Hello!<div><br></div><div>I&#39;m a bit of an Agda newbie, so to learn it I started converting Pierce&#39;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&#39;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&#39;t be an (ANum zero) doesn&#39;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 -&gt; Set where</div><div>  refl : x == x</div><div><br></div><div>eq-subst : {A : Set} -&gt; (C : A -&gt; Set) -&gt; (a&#39; a&#39;&#39; : A) -&gt; a&#39; == a&#39;&#39; -&gt; C a&#39; -&gt; C a&#39;&#39;</div>
<div>eq-subst c .a&#39;&#39; a&#39;&#39; refl p = p</div><div><br></div><div>eq-subst&#39; : {A B : Set} {x x&#39; y y&#39; : A} (f : A -&gt; A -&gt; B) -&gt; x == x&#39; -&gt; y == y&#39; -&gt; f x y == f x&#39; y&#39;</div>
<div>eq-subst&#39; f refl refl = refl</div><div><br></div><div>data aexp : Set where</div><div>  ANum : ℕ -&gt; aexp</div><div>  APlus : aexp -&gt; aexp -&gt; aexp</div><div>  AMinus : aexp -&gt; aexp -&gt; aexp</div><div>
  AMult : aexp -&gt; aexp -&gt; aexp</div><div><br></div><div>aeval : aexp -&gt; ℕ </div><div>aeval (ANum y) = y</div><div>aeval (APlus y y&#39;) = aeval y + aeval y&#39;</div><div>aeval (AMinus y y&#39;) = aeval y ∸ aeval y&#39;</div>
<div>aeval (AMult y y&#39;) = aeval y * aeval y&#39;</div><div><br></div><div>optimize-0plus : aexp -&gt; aexp</div><div>optimize-0plus (ANum y) = ANum y</div><div>optimize-0plus (APlus (ANum zero) y&#39;) = optimize-0plus y&#39;</div>
<div>optimize-0plus (APlus y y&#39;) = APlus (optimize-0plus y) (optimize-0plus y&#39;)</div><div>optimize-0plus (AMinus y y&#39;) = AMinus (optimize-0plus y) (optimize-0plus y&#39;)</div><div>optimize-0plus (AMult y y&#39;) = AMult (optimize-0plus y) (optimize-0plus y&#39;)</div>
<div><br></div><div>optimize-0plus-sound : (e : aexp) -&gt; aeval (optimize-0plus e) == aeval e</div><div>optimize-0plus-sound (ANum y) = refl</div><div>optimize-0plus-sound (APlus (ANum zero) y&#39;) = optimize-0plus-sound y&#39;</div>
<div>optimize-0plus-sound (APlus y y&#39;) = {!!}</div><div>optimize-0plus-sound (AMinus y y&#39;) = eq-subst&#39; _∸_ (optimize-0plus-sound y) (optimize-0plus-sound y&#39;)</div><div>optimize-0plus-sound (AMult y y&#39;) = eq-subst&#39; (_*_) (optimize-0plus-sound y) (optimize-0plus-sound y&#39;)</div>
</div><div><br></div>