[Agda] Problem with a simple proof

[Ulf Norell]

On Wed, May 4, 2011 at 10:09 PM, Caylee Hogg <caylee.hogg at gmail.com> wrote:

>
>
> 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.
>

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):

mutual
  plus-helper : (a b : aexp) -> aeval (optimize-0plus (APlus a b)) == aeval
(APlus a b)
  ...
  plus-helper (APlus a b) c = eq-subst' _+_ (plus-helper a b)
(optimize-0plus-sound c)
  ...

  optimize-0plus-sound (APlus a b) = plus-helper a b
  ...

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:

  open import Relation.Binary.PropositionalEquality renaming (_≡_ to _==_)

Now instead of (for instance):

  optimize-0plus-sound (AMult y y') = eq-subst' (_*_) (optimize-0plus-sound
y) (optimize-0plus-sound y')

you can write

  optimize-0plus-sound (AMult y y') rewrite optimize-0plus-sound y |
optimize-0plus-sound y' = refl

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.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20110505/fda44db6/attachment.html