[Agda] Problem with a simple proof

[gallais at ensl.org]

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') = ?

Cheers,
--
guillaume



On 4 May 2011 21:03, Caylee Hogg <caylee.hogg at gmail.com> wrote:
> 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')
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>