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

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



Thanks Sam. That works.

(then (expand* formula1 formula2 ...) (all-typepreds) (grind))

One has to first expand formulas until the relevant expressions to which typepred is applied appear, and then one can apply all-typepreds.

Jonathan

On Jun 30, 2016, at 3:41 PM, Sam Owre <owre@xxxxxxxxxxx> wrote:

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