<br><br><div class="gmail_quote">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>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>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>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>optimize-0plus-sound (APlus (APlus y y&#39;) y0) = {!!}</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>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><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><br></div><div>Thanks for the help,</div><div>Caylee</div></div>