[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [PVS-Help] Using a finite subtype of nat and auto proving



Hi Ostroff,

 once you get x!1*x!1 >= x!1 use (div-by 1 "x!1" ) then use (grind).

Here is the proof steps:

 (skosimp*) (typepred "x!1") (div-by 1 "x!1") (grind)


Thanks

On Tue, Aug 23, 2016 at 8:35 AM, Jonathan Ostroff <jonathan@xxxxxxxx> wrote:
——
logic : THEORY
BEGIN
D: TYPE = {i: nat | 1 <= i AND i <= 5}

D2: TYPE = {i: nat | i = 1 OR i= 2 OR i=3 OR i=4 OR i=5}

conj1: CONJECTURE (FORALL (x:D2) : x*x >= x)

END logic
————

(grind) works on conj1 with type D2.

But if we replace D2 with D, then (grind) will not work. In fact, I did not see how to prove it.

Is there a simple way to use D rather than D2 and to prove the conjecture?

Thanks

Jonathan




--
Amer Tahat

PhD. Computational Sciences and Engineering,

Department of Computer Science,
Michigan Tech University,
Houghton, MI, 49931, U.S.A