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

Re: [PVS-Help] Typred with grind/ground



Hi Jonathan,

Look into all-typepreds - it should do what you want.

Regards,
Sam Owre

Jonathan Ostroff <jonathan@xxxxxxxx> wrote:

> I used predicate subtyping to define a type DIGIT.
> 
> DIGIT: TYPE = {i: nat | i = 0 OR i = 1} CONTAINING 0
> a,b,c,z: DIGIT
> 
> Then, in the middle of a proof I was given the following sequent, which should have discharged automatically.
> 
> [-1] (a + b + c >= 2)
> {-2} IF a = 1 AND b = 1 THEN 1 = d ELSE 0 = d ENDIF
> {-3} IF b = 1 AND c = 1 THEN 1 = e ELSE 0 = e ENDIF
> {-4} IF c = 1 AND a = 1 THEN 1 = f ELSE 0 = f ENDIF
> {-5} IF d = 1 OR e = 1 THEN 1 = g ELSE 0 = g ENDIF
> {-6} IF g = 1 OR f = 1 THEN 1 = z ELSE 0 = z ENDIF
> |-------
> [1] z = 1
> 
> However, without using (typepred a b c), the above would not prove.
> 
> In fact, if I had done (typepred a b c) and then (grind) at a higher level, all would have proven automatically. We also could do
> (typepred a b c)(ground) in the above case. 
> 
> Is there some way to say (a) introduce all relevant type predicates whatever they are, and then (2) grind?
> 
> (In this case, I knew that I needed a, b and c, but in many cases it is not obvious when ons starts out).
> 
> Thanks,
> 
> Jonathan
>