[Found a way to finish the equivalence proof.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080624151447
 + I reformulated the correctness statement using double negation.
 + The proof is not finished yet. In an attempt to reduce tedium in the
   remaining cases I plan to stop using evaluation contexts in the
   definition of the small-step reduction relation.
] adddir ./Semantics/Equivalence
hunk ./CompilerCorrectness.agda 46
-Sound₂ e i = start e i ⟶∞ -> e ⇑[ i ]
+Sound₂ e i = start e i ⟶∞ -> ¬ ¬ e ⇑[ i ]
hunk ./CompilerCorrectness/Soundness.agda 18
+open import Relation.Nullary
hunk ./CompilerCorrectness/Soundness.agda 44
-  ≡-subst (\x -> x ⇑[ i ]) (left-inverse e)
-          (small⇒big⟶∞ (sound₂' e e⟶∞))
+  ≡-subst (\x -> ¬ ¬ x ⇑[ i ]) (left-inverse e)
+          (small⇒big⟶∞ _ _ (sound₂' e e⟶∞))
hunk ./Everything.agda 27
-import Semantics.Equivalence           -- Currently does not pass the productivity checker.
+import Semantics.Equivalence
+import Semantics.Equivalence.Add
hunk ./Everything.agda 63
-import CompilerCorrectness.Soundness  -- Currently contains postulates.
+import CompilerCorrectness.Soundness  -- Currently contains postulate.
hunk ./Semantics/Equivalence.agda 16
+open import Data.Sum
+open import Data.Empty
+open import Relation.Nullary
+open import Data.Function
+open import Relation.Binary.PropositionalEquality
hunk ./Semantics/Equivalence.agda 38
-    ⟶∞ : forall {t} {e : Exprˢ t} {i} ->
-         e ⟶∞[ i ] -> e ˢ⁻¹ ⇑[ i ]
+    ⟶∞ : forall {t} (e : Exprˢ t) i ->
+         e ⟶∞[ i ] -> ¬ ¬ e ˢ⁻¹ ⇑[ i ]
hunk ./Semantics/Equivalence.agda 243
--- excluded middle to prove this result. I could follow them, but I
--- would prefer not to have to postulate any classical axioms, or
--- resort to double-negation translation. However, achieving this
--- seems to be difficult at best. The following is as far as I've
--- come:
+-- excluded middle to prove this result. Here I follow them, but I use
+-- double-negation instead of postulating anything (as suggested by
+-- Thorsten).
hunk ./Semantics/Equivalence.agda 247
--- First a function which calculates a "prefix" of the resulting
--- proof, without looking at the remainder.
-
-prefix : forall {t i j} (E : EvalCtxt t i j) {x} ->
-         x ˢ⁻¹ ⇑[ i ] -> E [ x ] ˢ⁻¹ ⇑[ j ]
-prefix •                  x⇑ = x⇑
-prefix (E •< |⊕| > y)     x⇑ = Add₁   (prefix E x⇑)
-prefix (E •< |>>| > y)    x⇑ = Seqn₁  (prefix E x⇑)
-prefix (E •< |catch| > y) x⇑ = Catch₁ (prefix E x⇑)
-prefix (val m ⊕• E)       x⇑ = Add₂ (m , Val) (prefix E x⇑)
-prefix (handler• E)       x⇑ = Catch₂ Throw (prefix E x⇑)
-prefix (block• E)         x⇑ = Block   (prefix E x⇑)
-prefix (unblock• E)       x⇑ = Unblock (prefix E x⇑)
-
--- Then a lemma which fills in the rest. Unfortunately this lemma is
--- not true.
+import Semantics.Equivalence.Add as Add
hunk ./Semantics/Equivalence.agda 249
-postulate
-
-  drop : forall {t i j} (E : EvalCtxt t i j) {x} ->
-         E [ x ] ˢ⁻¹ ⇑[ j ] -> x ˢ⁻¹ ⇑[ i ]
-
--- Finally we can define another variant of the proof. While this
--- proof is not guarded, it is conceivable that it is lazy enough to
--- be productive. Perhaps. (If the drop lemma were definable and it
--- only inspected the "prefix" of its argument.)
-
-small⇒big⟶∞ : forall {t} {e : Exprˢ t} {i} ->
-              e ⟶∞[ i ] -> e ˢ⁻¹ ⇑[ i ]
-small⇒big⟶∞ (Red E r ◅∞ rs) ~
-  prefix E (small⇒big⟶ʳ⇑ r (drop E (small⇒big⟶∞ rs)))
+small⇒big⟶∞ : forall {t} (e : Exprˢ t) i ->
+              e ⟶∞[ i ] -> ¬ ¬ e ˢ⁻¹ ⇑[ i ]
+small⇒big⟶∞ (run (val n))     i ⟶∞ ¬⇑ = {! !}
+small⇒big⟶∞ (run throw)       i ⟶∞ ¬⇑ = {! !}
+small⇒big⟶∞ (run loop)        i ⟶∞ ¬⇑ = ¬⇑ loop⇑
+small⇒big⟶∞ (run (x ⊕ y))     i ⟶∞ ¬⇑ = Add.lemma ⟶∞ helper
+  where
+  helper : x ⟶∞[ i ] ⊎ ∃ (\n -> (x ⟶⋆[ i ] done (val n)) × y ⟶∞[ i ]) -> ⊥
+  helper (inj₁ x⟶∞)              = small⇒big⟶∞ x i x⟶∞ (¬⇑ ∘ Add₁)
+  helper (inj₂ (n , x⟶⋆n , y⟶∞)) = small⇒big⟶∞ y i y⟶∞ (¬⇑ ∘ Add₂ (n , small⇒big⟶⋆ (val n) x⟶⋆n))
+small⇒big⟶∞ (run (x >> y))    i ⟶∞ ¬⇑ = {! !}
+small⇒big⟶∞ (run (x catch y)) i ⟶∞ ¬⇑ = {! !}
+small⇒big⟶∞ (run (block x))   i ⟶∞ ¬⇑ = {! !}
+small⇒big⟶∞ (run (unblock x)) i ⟶∞ ¬⇑ = {! !}
+small⇒big⟶∞ (done v)          i ⟶∞ ¬⇑ = ⊥-elim (done↛∞ ⟶∞)
addfile ./Semantics/Equivalence/Add.agda
hunk ./Semantics/Equivalence/Add.agda 1
+------------------------------------------------------------------------
+-- The ⊕ case of small⇒big⟶∞ uses the main lemma proved in this module
+------------------------------------------------------------------------
+
+module Semantics.Equivalence.Add where
+
+open import Syntax
+open import Infinite
+open import Semantics.SmallStep
+
+open import Data.Empty
+open import Data.Product
+open import Data.Sum
+open import Data.Function
+open import Relation.Nullary
+open import Relation.Binary.PropositionalEquality
+
+drop-run[•⊕-] : forall {t} {x x' y y' : Exprˢ t} ->
+                run (x ⊕ y) ≡ run (x' ⊕ y') -> x ≡ x'
+drop-run[•⊕-] ≡-refl ~ ≡-refl
+
+helper₁ : forall {t} {y z : Exprˢ t} {m i} ->
+          z ⟶∞[ i ] -> z ≡ run (done (val m) ⊕ y) -> y ⟶∞[ i ]
+helper₁ (Red • Val                ◅∞ ⟶∞) ()
+helper₁ (Red • Throw              ◅∞ ⟶∞) ()
+helper₁ (Red • Loop               ◅∞ ⟶∞) ()
+helper₁ (Red • Add₁               ◅∞ ⟶∞) ≡-refl ~ ⊥-elim (done↛∞ ⟶∞)
+helper₁ (Red • Add₂               ◅∞ ⟶∞) ()
+helper₁ (Red • Add₃               ◅∞ ⟶∞) ≡-refl ~ ⊥-elim (done↛∞ ⟶∞)
+helper₁ (Red • Seqn₁              ◅∞ ⟶∞) ()
+helper₁ (Red • Seqn₂              ◅∞ ⟶∞) ()
+helper₁ (Red • Catch₁             ◅∞ ⟶∞) ()
+helper₁ (Red • Catch₂             ◅∞ ⟶∞) ()
+helper₁ (Red • Block              ◅∞ ⟶∞) ()
+helper₁ (Red • Unblock            ◅∞ ⟶∞) ()
+helper₁ (Red • (Int int)          ◅∞ ⟶∞) ≡-refl ~ ⊥-elim (done↛∞ ⟶∞)
+helper₁ (Red {j = j} {y = z}
+             (E •< |⊕| >     y) r ◅∞ ⟶∞) eq     ~ ⊥-elim (done↛ $ ≡-subst (\x -> x ⟶[ j ] E [ z ])
+                                                                          (drop-run[•⊕-] eq)
+                                                                          (Red E r))
+helper₁ (Red (E •< |>>| >    y) r ◅∞ ⟶∞) ()
+helper₁ (Red (E •< |catch| > y) r ◅∞ ⟶∞) ()
+helper₁ (Red (val m ⊕• E)       r ◅∞ ⟶∞) ≡-refl ~ Red E r ◅∞ helper₁ ⟶∞ ≡-refl
+helper₁ (Red (handler• E)       r ◅∞ ⟶∞) ()
+helper₁ (Red (block•   E)       r ◅∞ ⟶∞) ()
+helper₁ (Red (unblock• E)       r ◅∞ ⟶∞) ()
+
+Pred : forall {t} -> Exprˢ t -> Status -> Exprˢ t -> Set
+Pred y i = \x -> ∃ \n -> x ≡ done (val n) × y ⟶∞[ i ]
+
+helper₂ : forall {t} {x y u : Exprˢ t} {i} ->
+          u ⟶∞[ i ] -> u ≡ run (x ⊕ y) -> x ⟶⋆∞[ i ] Pred y i
+helper₂ (Red • Val                ◅∞ ⟶∞) ()
+helper₂ (Red • Throw              ◅∞ ⟶∞) ()
+helper₂ (Red • Loop               ◅∞ ⟶∞) ()
+helper₂ (Red • Add₁               ◅∞ ⟶∞) ≡-refl ~ ⊥-elim (done↛∞ ⟶∞)
+helper₂ (Red • Add₂               ◅∞ ⟶∞) ≡-refl ~ ⊥-elim (done↛∞ ⟶∞)
+helper₂ (Red • Add₃               ◅∞ ⟶∞) ≡-refl ~ ⊥-elim (done↛∞ ⟶∞)
+helper₂ (Red • Seqn₁              ◅∞ ⟶∞) ()
+helper₂ (Red • Seqn₂              ◅∞ ⟶∞) ()
+helper₂ (Red • Catch₁             ◅∞ ⟶∞) ()
+helper₂ (Red • Catch₂             ◅∞ ⟶∞) ()
+helper₂ (Red • Block              ◅∞ ⟶∞) ()
+helper₂ (Red • Unblock            ◅∞ ⟶∞) ()
+helper₂ (Red • (Int int)          ◅∞ ⟶∞) ≡-refl ~ ⊥-elim (done↛∞ ⟶∞)
+helper₂ (Red (E •< |⊕| >     y) r ◅∞ ⟶∞) ≡-refl ~ Red E r ◅∞ helper₂ ⟶∞ ≡-refl
+helper₂ (Red (E •< |>>| >    y) r ◅∞ ⟶∞) ()
+helper₂ (Red (E •< |catch| > y) r ◅∞ ⟶∞) ()
+helper₂ (Red (val m ⊕• E)       r ◅∞ ⟶∞) ≡-refl ~ ε (m , ≡-refl , Red E r ◅∞ helper₁ ⟶∞ ≡-refl)
+helper₂ (Red (handler• E)       r ◅∞ ⟶∞) ()
+helper₂ (Red (block• E)         r ◅∞ ⟶∞) ()
+helper₂ (Red (unblock• E)       r ◅∞ ⟶∞) ()
+
+lemma : forall {t} {x y : Exprˢ t} {i} ->
+        run (x ⊕ y) ⟶∞[ i ] ->
+        ¬ ¬ (x ⟶∞[ i ] ⊎
+             (∃ \n -> (x ⟶⋆[ i ] done (val n)) × y ⟶∞[ i ]))
+lemma {x = x} {y} {i} x⊕y⟶∞ =
+  map-¬¬ helper $ reductio-ad-absurdum-⊎ (⋆∞⇒∞ (helper₂ x⊕y⟶∞ ≡-refl))
+  where
+  helper : ∃ (\z -> (x ⟶⋆[ i ] z) × Pred y i z) ⊎ x ⟶∞[ i ] -> _
+  helper (inj₁ (.(done (val n)) , x⟶⋆n , n , ≡-refl , y⟶∞)) = inj₂ (n , x⟶⋆n , y⟶∞)
+  helper (inj₂ x⟶∞)                                         = inj₁ x⟶∞