[Changed to a possibly correct correctness statement.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080307033740] hunk ./Wand.agda 396
-  exec : forall {n f} -> LinearExp n f -> Stack n -> C
-  exec (add ○ c)     (x ∷ y ∷ s) σ = exec c (x + y ∷ s) σ
-  exec (fetch I ○ c) s           σ = exec c (σ I ∷ s) σ
-  exec halt          (x ∷ [])    σ = x
-
-  -- Correctness.
-
+  ⟦_⟧' : forall {n} -> (V ^ n → C) -> Stack n -> C
+  ⟦ f ⟧' []      = f
+  ⟦ f ⟧' (x ∷ s) = ⟦ f x ⟧' s
+
hunk ./Wand.agda 401
-  ⟦ f ⟧ []      = f
-  ⟦ f ⟧ (x ∷ s) = ⟦ f x ⟧ s
+  ⟦ f ⟧ s = ⟦ f ⟧' (reverse s)
hunk ./Wand.agda 403
-  -- Note: These lemmas are not true. I think the stack should be
-  -- reversed, but this is bound to complicate the proofs... Perhaps
-  -- it's a good idea to derive the interpreter.
-
hunk ./Wand.agda 404
-           ⟦ B″ 2 n Step₁.add g x y ⟧ s σ ≡ ⟦ g (x + y) ⟧ s σ
+           ⟦ B″ 2 n Step₁.add g ⟧ (x ∷ y ∷ s) σ ≡ ⟦ g ⟧ (y + x ∷ s) σ
hunk ./Wand.agda 406
-  lemma₁ g x y (z ∷ s) σ = {!  !}
+  lemma₁ g x y (z ∷ s) σ = {! !}
hunk ./Wand.agda 409
-           ⟦ B″ 0 n (Step₁.fetch I) g ⟧ s σ ≡ ⟦ g (σ I) ⟧ s σ
+           ⟦ B″ 0 n (Step₁.fetch I) g ⟧ s σ ≡ ⟦ g ⟧ (σ I ∷ s) σ
hunk ./Wand.agda 411
-  lemma₂ g I (_ ∷ _ ∷ _ ∷ [])      σ = {! !}
-  lemma₂ g I (z ∷ s) σ = {!lemma₂ (\x -> g x z) I s σ !}
+  lemma₂ g I (z ∷ s) σ = {! !}
+
+  -- Note: I have not derived the implementation of exec, I have just
+  -- combined it with the correctness proof.
+
+  mutual
+
+    exec : forall {n f} -> LinearExp n f -> Stack n -> C
+    exec e s σ = witness (execP e s σ)
hunk ./Wand.agda 421
-  exec-correct : forall {n f}
-                        (e : LinearExp n f) (s : Stack n) (σ : S) ->
-                 ⟦ f ⟧ s σ ≡ exec e s σ
-  exec-correct (_○_ add {n = n} {g = g} c) (x ∷ y ∷ s) σ = begin
-    ⟦ B″ 2 n Step₁.add g x y ⟧ s σ
-      ≡⟨ lemma₁ g x y s σ ⟩
-    ⟦ g (x + y) ⟧ s σ
-      ≡⟨ exec-correct c (x + y ∷ s) σ ⟩
-    exec c (x + y ∷ s) σ
-      ∎
-  exec-correct (_○_ (fetch I) {n = n} {g = g} c) s σ = begin
-    ⟦ B″ 0 n (Step₁.fetch I) g ⟧ s σ
-      ≡⟨ lemma₂ g I s σ ⟩
-    ⟦ g (σ I) ⟧ s σ
-      ≡⟨ exec-correct c (σ I ∷ s) σ ⟩
-    exec c (σ I ∷ s) σ
-      ∎
-  exec-correct halt (x ∷ []) σ = ≡-refl
+    execP : forall {n f} (e : LinearExp n f) (s : Stack n) (σ : S) ->
+            EqualTo (⟦ f ⟧ s σ)
+    execP (_○_ add {n} {g} c) (x ∷ y ∷ s) σ = ▷ begin
+      ⟦ B″ 2 n Step₁.add g ⟧ (x ∷ y ∷ s) σ
+        ≡⟨ lemma₁ g x y s σ ⟩
+      ⟦ g ⟧ (y + x ∷ s) σ
+        ≡⟨ proof (execP c (y + x ∷ s) σ) ⟩
+      exec c (y + x ∷ s) σ
+        ∎
+    execP (_○_ (fetch I) {n} {g} c) s σ = ▷ begin
+      ⟦ B″ 0 n (Step₁.fetch I) g ⟧ s σ
+        ≡⟨ lemma₂ g I s σ ⟩
+      ⟦ g ⟧ (σ I ∷ s) σ
+        ≡⟨ proof (execP c (σ I ∷ s) σ) ⟩
+      exec c (σ I ∷ s) σ
+        ∎
+    execP halt (x ∷ []) σ = ▷ begin x ∎
hunk ./Wand.agda 459
-      ≡⟨ Step₄.exec-correct (comp e) [] σ ⟩
+      ≡⟨ proof (Step₄.execP (comp e) [] σ) ⟩