[Agda] Problem with a simple proof

[Caylee Hogg]

Hello!

I'm a bit of an Agda newbie, so to learn it I started converting Pierce's
Software Foundations book. I hit a bit of a roadblock when I needed to prove
that an optimization preserves the semantics of a simple expression
language. I'm including the relevant code below - the problem is that while
I was able to define the optimization using the overlapping patterns, but
when trying to write the proof the fact that y in the overlapping case can't
be an (ANum zero) doesn't seem obvious to the type checker.

How should I actually finish the proof? Please feel free to critique any of
it.

Cheers,
Caylee Hogg

open import Data.Nat

data _==_ {A : Set}(x : A) : A -> Set where
  refl : x == x

eq-subst : {A : Set} -> (C : A -> Set) -> (a' a'' : A) -> a' == a'' -> C a'
-> C a''
eq-subst c .a'' a'' refl p = p

eq-subst' : {A B : Set} {x x' y y' : A} (f : A -> A -> B) -> x == x' -> y ==
y' -> f x y == f x' y'
eq-subst' f refl refl = refl

data aexp : Set where
  ANum : ℕ -> aexp
  APlus : aexp -> aexp -> aexp
  AMinus : aexp -> aexp -> aexp
  AMult : aexp -> aexp -> aexp

aeval : aexp -> ℕ
aeval (ANum y) = y
aeval (APlus y y') = aeval y + aeval y'
aeval (AMinus y y') = aeval y ∸ aeval y'
aeval (AMult y y') = aeval y * aeval y'

optimize-0plus : aexp -> aexp
optimize-0plus (ANum y) = ANum y
optimize-0plus (APlus (ANum zero) y') = optimize-0plus y'
optimize-0plus (APlus y y') = APlus (optimize-0plus y) (optimize-0plus y')
optimize-0plus (AMinus y y') = AMinus (optimize-0plus y) (optimize-0plus y')
optimize-0plus (AMult y y') = AMult (optimize-0plus y) (optimize-0plus y')

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 y y') = {!!}
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')
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20110504/232c291b/attachment.html