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

Re: Proof of override expressions



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