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

*To*: Malcolm Dowse <dowsem@tcd.ie>*Subject*: Re: Record-type equality bug??*From*: Holger Pfeifer <pfeifer@ares.informatik.uni-ulm.de>*Date*: Wed, 28 Mar 2001 11:54:25 +0200*CC*: pvs-help@csl.sri.com*References*: <20010327224827.A181946@alf2.tcd.ie>*Sender*: pvs-help-owner@csl.sri.com

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

**References**:**Record-type equality bug??***From:*Malcolm Dowse <dowsem@tcd.ie>

- Prev by Date:
**Record-type equality bug??** - Next by Date:
**Re: PVS batch mode** - Prev by thread:
**Record-type equality bug??** - Next by thread:
**Enumeration types** - Index(es):