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

*To*: Bin Chen <chenb3@cas.mcmaster.ca>*Subject*: Re: Proof of override expressions*From*: Bruno Dutertre <bruno@sdl.sri.com>*Date*: Thu, 20 Feb 2003 19:26:46 -0800*CC*: pvs-help@csl.sri.com*References*: <Pine.GSO.4.44.0302201615380.14240-100000@birkhoff.cas.mcmaster.ca>*Sender*: pvs-help-owner@csl.sri.com*User-Agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.0.0) Gecko/20020529

Bin Chen wrote: > Hi, > > Could anyone please tell me how to prove the following sequent? > > s_correct1: > > |-------- > [1] x > WITH [r(1) := x(r(2)) + x(r(3)), r(0):= x(r(2)) + x(r(3))] > (r(1)) > = > x > WITH [r(1) := x(r(2)) + x(r(3)), r(0):= x(r(2)) + x(r(3))] > (r(2)) > + > x > WITH [r(1) := x(r(2)) + x(r(3)), r(0):= x(r(2)) + x(r(3))] > (r(3)) > Hi, If r(0), r(1), r(2), and r(3) are distinct then (assert) should do it. (There are also other cases where (assert) will work). If that does not work, you can repeatedly apply (lift-if) until all the WITH disappear, and prove the resulting sequent. > Usually how to prove sequents with override expressions? > The main point is that "x WITH [(i) := a](j)" is the same "IF i=j THEN a ELSE x(j) ENDIF". So the decision procedures can simplify it if they can determine that "i=j" is true or that it is false. Otherwise, (lift-if) treats "x WITH [(i) := a](j)" like "IF i=j THEN a ELSE x(j) ENDIF". Proof strategies like (reduce), (smash), and (grind) will do that too since they apply (lift-if) internally. For multiple updates, "x WITH [(i) := a, (j) := b]" is the same as "x WITH [(i) := a] WITH [(j) := b]". > Thank you very much! > > Ken. > Bruno -- Bruno Dutertre | bruno@sdl.sri.com SDL, SRI International | fax: 650 859-2844 333 Ravenswood Avenue, Menlo Park CA 94025 | tel: 650 859-2717

**References**:**Proof of override expressions***From:*Bin Chen <chenb3@cas.mcmaster.ca>

- Prev by Date:
**Proof of override expressions** - Next by Date:
**existskwantor problem** - Prev by thread:
**Proof of override expressions** - Next by thread:
**Dependent types lost in reduce combinators** - Index(es):