<br><br><div class="gmail_quote">On Wed, May 4, 2011 at 10:09 PM, Caylee Hogg <span dir="ltr"><<a href="mailto:caylee.hogg@gmail.com">caylee.hogg@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
<br><br><div class="gmail_quote"><div class="im">On Wed, May 4, 2011 at 12:39 PM, gallais @ <a href="http://ensl.org" target="_blank">ensl.org</a> <span dir="ltr"><<a href="mailto:guillaume.allais@ens-lyon.org" target="_blank">guillaume.allais@ens-lyon.org</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Caylee,<br>
<br>
When you are doing a proof by induction (which is what's underlying<br>
here), you have to take care of each case in a separate clause. Here<br>
is the skeleton of a proof that should work:<br>
<div><br>
optimize-0plus-sound : (e : aexp) -> aeval (optimize-0plus e) == aeval e<br>
</div>optimize-0plus-sound (ANum y) = ?<br>
{- APlus y y' -> Is y equal to ANum zero ? -> Pattern matching on y -}<br>
{- Aplus (ANum n) y') -> Is n equal to zero ? -> Pattern matching on n -}<br>
<div>optimize-0plus-sound (APlus (ANum zero) y') = {!!}<br>
</div>optimize-0plus-sound (APlus (ANum (suc n)) y')= {!!}<br>
{- Other cases -}<br>
optimize-0plus-sound (APlus (APlus y y') y0) = {!!}<br>
optimize-0plus-sound (APlus (AMinus y y') y0) = {!!}<br>
optimize-0plus-sound (APlus (AMult y y') y0) = {!!}<br>
optimize-0plus-sound (AMinus y y') = ?<br>
optimize-0plus-sound (AMult y y') = ?<br></blockquote><div><br></div></div><div>Okay! So it wasn't bad style, though, to define the original optimize-0plus function with the overlapping patterns? It just doesn't work for the actual inductive proof?</div>
<div><br></div><div>Now I've hit another issue...this time with trying to make the termination checker happy. </div><div><br></div><div><div class="im"><div>optimize-0plus-sound : (e : aexp) -> aeval (optimize-0plus e) == aeval e</div>
<div>optimize-0plus-sound (ANum y) = refl</div><div>optimize-0plus-sound (APlus (ANum zero) y') = optimize-0plus-sound y'</div></div><div>optimize-0plus-sound (APlus (ANum (suc n)) y') = eq-subst' _+_ (optimize-0plus-sound (ANum (suc n))) (optimize-0plus-sound y')</div>
<div class="im">
<div>optimize-0plus-sound (APlus (APlus y y') y0) = {!!}</div></div><div>optimize-0plus-sound (APlus (AMinus y y') y0) = eq-subst' _+_</div><div> (eq-subst' _∸_ (optimize-0plus-sound y) (optimize-0plus-sound y'))</div>
<div> (optimize-0plus-sound y0)</div><div>optimize-0plus-sound (APlus (AMult y y') y0) = eq-subst' _+_ (eq-subst' _*_ (optimize-0plus-sound y) (optimize-0plus-sound y')) (optimize-0plus-sound y0)</div>
<div class="im">
<div>optimize-0plus-sound (AMinus y y') = eq-subst' _∸_ (optimize-0plus-sound y) (optimize-0plus-sound y')</div><div>optimize-0plus-sound (AMult y y') = eq-subst' (_*_) (optimize-0plus-sound y) (optimize-0plus-sound y')</div>
</div></div><div><br></div><div>So...what I morally want to do, and is basically what the Coq proof looks like in tactic form, is to use (optimize-0plus-sound (APlus y y')) within the remaining shed; however, while this type checks it makes the termination checker highlight everything in red to let me know that I'm a bad person. It seems like totally reasonable induction since I'm getting smaller with each step, I'm just not getting as small as Agda would seem to like.</div>
</div></blockquote><div><br></div><div>That's a bug in the termination checker that has been fixed in the development version. If you don't want to upgrade you can work around it by introducing a helper function for the plus case (unchecked code):</div>
<div><br></div><div>mutual</div><div> plus-helper : (a b : aexp) -> aeval (optimize-0plus (APlus a b)) == aeval (APlus a b)</div><div> ...</div><div> plus-helper (APlus a b) c = eq-subst' _+_ (plus-helper a b) (optimize-0plus-sound c)</div>
<div> ...</div><div><br></div><div> optimize-0plus-sound (APlus a b) = plus-helper a b</div><div> ...</div><div><br></div><div>You might also want to check out the "rewrite" feature that let's you get away without all the eq-subst's. To use it you need the equality from the standard library:</div>
<div><br></div><div> open import Relation.Binary.PropositionalEquality renaming (_≡_ to _==_)</div><div><br></div><div>Now instead of (for instance):</div><div><br></div><div><meta charset="utf-8"><div><div class="im"><div>
optimize-0plus-sound (AMult y y') = eq-subst' (_*_) (optimize-0plus-sound y) (optimize-0plus-sound y')</div><div><br></div><div>you can write</div><div><br></div><div> optimize-0plus-sound (AMult y y') rewrite optimize-0plus-sound y | optimize-0plus-sound y' = refl</div>
<div><br></div><div>Rewrite takes a bunch of equality proofs (lhs1 == rhs1, lhs2 == rhs2, ..) separated by bars and rewrites any occurrences of the left hand sides in the current goal (and context) to the corresponding right hand side.</div>
<div><br></div><div>/ Ulf</div></div></div></div></div>