<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"><<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>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>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>optimize-0plus-sound (APlus (ANum (suc n)) y') = eq-subst' _+_ (optimize-0plus-sound (ANum (suc n))) (optimize-0plus-sound y')</div>
<div>optimize-0plus-sound (APlus (APlus y y') y0) = {!!}</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>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><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><br></div><div>Thanks for the help,</div><div>Caylee</div></div>