<br><br><div class="gmail_quote">On Wed, May 4, 2011 at 10:09 PM, Caylee Hogg <span dir="ltr">&lt;<a href="mailto:caylee.hogg@gmail.com">caylee.hogg@gmail.com</a>&gt;</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">&lt;<a href="mailto:guillaume.allais@ens-lyon.org" target="_blank">guillaume.allais@ens-lyon.org</a>&gt;</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&#39;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) -&gt; aeval (optimize-0plus e) == aeval e<br>
</div>optimize-0plus-sound (ANum y) = ?<br>
{- APlus y y&#39; -&gt; Is y equal to ANum zero ? -&gt; Pattern matching on y -}<br>
{- Aplus (ANum n) y&#39;) -&gt; Is n equal to zero ? -&gt; Pattern matching on n -}<br>
<div>optimize-0plus-sound (APlus (ANum zero) y&#39;) = {!!}<br>
</div>optimize-0plus-sound (APlus (ANum (suc n)) y&#39;)= {!!}<br>
{- Other cases -}<br>
optimize-0plus-sound (APlus (APlus y y&#39;) y0) = {!!}<br>
optimize-0plus-sound (APlus (AMinus y y&#39;) y0) = {!!}<br>
optimize-0plus-sound (APlus (AMult y y&#39;) y0) = {!!}<br>
optimize-0plus-sound (AMinus y y&#39;) = ?<br>
optimize-0plus-sound (AMult y y&#39;) = ?<br></blockquote><div><br></div></div><div>Okay! So it wasn&#39;t bad style, though, to define the original optimize-0plus function with the overlapping patterns? It just doesn&#39;t work for the actual inductive proof?</div>



<div><br></div><div>Now I&#39;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) -&gt; aeval (optimize-0plus e) == aeval e</div>


<div>optimize-0plus-sound (ANum y) = refl</div><div>optimize-0plus-sound (APlus (ANum zero) y&#39;) = optimize-0plus-sound y&#39;</div></div><div>optimize-0plus-sound (APlus (ANum (suc n)) y&#39;) = eq-subst&#39; _+_ (optimize-0plus-sound (ANum (suc n))) (optimize-0plus-sound y&#39;)</div>

<div class="im">
<div>optimize-0plus-sound (APlus (APlus y y&#39;) y0) = {!!}</div></div><div>optimize-0plus-sound (APlus (AMinus y y&#39;) y0) = eq-subst&#39; _+_</div><div>                                                  (eq-subst&#39; _∸_ (optimize-0plus-sound y) (optimize-0plus-sound y&#39;))</div>


<div>                                                  (optimize-0plus-sound y0)</div><div>optimize-0plus-sound (APlus (AMult y y&#39;) y0) = eq-subst&#39; _+_ (eq-subst&#39; _*_ (optimize-0plus-sound y) (optimize-0plus-sound y&#39;)) (optimize-0plus-sound y0)</div>

<div class="im">
<div>optimize-0plus-sound (AMinus y y&#39;) = eq-subst&#39; _∸_ (optimize-0plus-sound y) (optimize-0plus-sound y&#39;)</div><div>optimize-0plus-sound (AMult y y&#39;) = eq-subst&#39; (_*_) (optimize-0plus-sound y) (optimize-0plus-sound y&#39;)</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&#39;)) within the remaining shed; however, while this type checks it makes the termination checker highlight everything in red to let me know that I&#39;m a bad person. It seems like totally reasonable induction since I&#39;m getting smaller with each step, I&#39;m just not getting as small as Agda would seem to like.</div>

</div></blockquote><div><br></div><div>That&#39;s a bug in the termination checker that has been fixed in the development version. If you don&#39;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) -&gt; aeval (optimize-0plus (APlus a b)) == aeval (APlus a b)</div><div>  ...</div><div>  plus-helper (APlus a b) c = eq-subst&#39; _+_ (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 &quot;rewrite&quot; feature that let&#39;s you get away without all the eq-subst&#39;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&#39;) = eq-subst&#39; (_*_) (optimize-0plus-sound y) (optimize-0plus-sound y&#39;)</div><div><br></div><div>you can write</div><div><br></div><div>  optimize-0plus-sound (AMult y y&#39;) rewrite optimize-0plus-sound y | optimize-0plus-sound y&#39; = 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>