Hello!<div><br></div><div>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.</div>
<div><br></div><div>How should I actually finish the proof? Please feel free to critique any of it.</div><div><br></div><div>Cheers,</div><div>Caylee Hogg</div><div><br></div><div><div>open import Data.Nat</div><div><br></div>
<div>data _==_ {A : Set}(x : A) : A -> Set where</div><div> refl : x == x</div><div><br></div><div>eq-subst : {A : Set} -> (C : A -> Set) -> (a' a'' : A) -> a' == a'' -> C a' -> C a''</div>
<div>eq-subst c .a'' a'' refl p = p</div><div><br></div><div>eq-subst' : {A B : Set} {x x' y y' : A} (f : A -> A -> B) -> x == x' -> y == y' -> f x y == f x' y'</div>
<div>eq-subst' f refl refl = refl</div><div><br></div><div>data aexp : Set where</div><div> ANum : ℕ -> aexp</div><div> APlus : aexp -> aexp -> aexp</div><div> AMinus : aexp -> aexp -> aexp</div><div>
AMult : aexp -> aexp -> aexp</div><div><br></div><div>aeval : aexp -> ℕ </div><div>aeval (ANum y) = y</div><div>aeval (APlus y y') = aeval y + aeval y'</div><div>aeval (AMinus y y') = aeval y ∸ aeval y'</div>
<div>aeval (AMult y y') = aeval y * aeval y'</div><div><br></div><div>optimize-0plus : aexp -> aexp</div><div>optimize-0plus (ANum y) = ANum y</div><div>optimize-0plus (APlus (ANum zero) y') = optimize-0plus y'</div>
<div>optimize-0plus (APlus y y') = APlus (optimize-0plus y) (optimize-0plus y')</div><div>optimize-0plus (AMinus y y') = AMinus (optimize-0plus y) (optimize-0plus y')</div><div>optimize-0plus (AMult y y') = AMult (optimize-0plus y) (optimize-0plus y')</div>
<div><br></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 y y') = {!!}</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>