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

Re: Record-type equality bug??



Malcolm,

> headc3.2 :
> 
> [-1]  (# un := 1, id := 1 #) = di!1
> [-2]  (# un := 1, id := 0 #) = di!1
>   |-------
> [1]   (di!1`un = 0)
> 
> Shouldn't this be trivially proveable?

Of course it should, and in fact it is: the commands

(REPLACE -1 :dir rl)
(ASSERT)

do the job.

But I suppose you wanted to have some of PVS's higher-level stategies
such as (GRIND) prove the formula and they failed. The reason for this
is that the default direction of rewriting equalities is from the left
to the right, whereas in your case you need the opposite direction.
Unfortunately, (GRIND) and its friends don't provide a way to change
the default behaviour. 

Maybe you can try to state your original conjecture in a way that the
formulae [-1] and [-2] above would appear as 
	di!1 = (# ... #)
in the proof. The (GRIND) would definitely work.

Hope this helps,

	- Holger