[A failed attempt at proving small⇒big⟶∞ without using excluded middle.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080618144219] hunk ./Semantics/Equivalence.agda 232
-small⇒big⟶∞ : forall {t} {e : Exprˢ t} {i} ->
-              e ⟶∞[ i ] -> e ˢ⁻¹ ⇑[ i ]
-small⇒big⟶∞ (Red E r ◅∞ rs) ~
-  map⇑ E (small⇒big⟶ʳ⇓ r) (small⇒big⟶ʳ⇑ r) (small⇒big⟶∞ rs)
+-- small⇒big⟶∞ : forall {t} {e : Exprˢ t} {i} ->
+--               e ⟶∞[ i ] -> e ˢ⁻¹ ⇑[ i ]
+-- small⇒big⟶∞ (Red E r ◅∞ rs) ~
+--   map⇑ E (small⇒big⟶ʳ⇓ r) (small⇒big⟶ʳ⇑ r) (small⇒big⟶∞ rs)
hunk ./Semantics/Equivalence.agda 239
--- would prefer not to have to postulate any classical axioms.
+-- 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:
+
+-- 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.
+
+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)))