[Agda] Problem with a simple proof

[Caylee Hogg]

On Wed, May 4, 2011 at 12:39 PM, gallais @ ensl.org <
guillaume.allais at ens-lyon.org> wrote:

> Hi Caylee,
>
> When you are doing a proof by induction (which is what's underlying
> here), you have to take care of each case in a separate clause. Here
> is the skeleton of a proof that should work:
>
> optimize-0plus-sound : (e : aexp) -> aeval (optimize-0plus e) == aeval e
> optimize-0plus-sound (ANum y) = ?
> {- APlus y y' -> Is y equal to ANum zero ? -> Pattern matching on y -}
> {- Aplus (ANum n) y') -> Is n equal to zero ? -> Pattern matching on n -}
> optimize-0plus-sound (APlus (ANum zero) y') = {!!}
> optimize-0plus-sound (APlus (ANum (suc n)) y')= {!!}
> {- Other cases -}
> optimize-0plus-sound (APlus (APlus y y') y0) = {!!}
> optimize-0plus-sound (APlus (AMinus y y') y0) = {!!}
> optimize-0plus-sound (APlus (AMult y y') y0) = {!!}
> optimize-0plus-sound (AMinus y y') = ?
> optimize-0plus-sound (AMult y y') = ?
>

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?

Now I've hit another issue...this time with trying to make the termination
checker happy.

optimize-0plus-sound : (e : aexp) -> aeval (optimize-0plus e) == aeval e
optimize-0plus-sound (ANum y) = refl
optimize-0plus-sound (APlus (ANum zero) y') = optimize-0plus-sound y'
optimize-0plus-sound (APlus (ANum (suc n)) y') = eq-subst' _+_
(optimize-0plus-sound (ANum (suc n))) (optimize-0plus-sound y')
optimize-0plus-sound (APlus (APlus y y') y0) = {!!}
optimize-0plus-sound (APlus (AMinus y y') y0) = eq-subst' _+_
                                                  (eq-subst' _∸_
(optimize-0plus-sound y) (optimize-0plus-sound y'))
                                                  (optimize-0plus-sound y0)
optimize-0plus-sound (APlus (AMult y y') y0) = eq-subst' _+_ (eq-subst' _*_
(optimize-0plus-sound y) (optimize-0plus-sound y')) (optimize-0plus-sound
y0)
optimize-0plus-sound (AMinus y y') = eq-subst' _∸_ (optimize-0plus-sound y)
(optimize-0plus-sound y')
optimize-0plus-sound (AMult y y') = eq-subst' (_*_) (optimize-0plus-sound y)
(optimize-0plus-sound y')

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.

Thanks for the help,
Caylee
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20110504/ebe9f04b/attachment.html