[Finished the equivalence proof.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080624193150] addfile ./Semantics/Equivalence/Lemmas.agda
hunk ./Everything.agda 29
-import Semantics.Equivalence.Add
+import Semantics.Equivalence.Lemmas
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
-
-helper₁ : forall {t} {y : Exprˢ t} {m i} ->
-          run (done (val m) ⊕ y) ⟶∞[ i ] -> y ⟶∞[ i ]
-helper₁ (Red Add₁      ◅∞ ⟶∞) ~ ⊥-elim (done↛∞ ⟶∞)
-helper₁ (Red Add₃      ◅∞ ⟶∞) ~ ⊥-elim (done↛∞ ⟶∞)
-helper₁ (Red (Int int) ◅∞ ⟶∞) ~ ⊥-elim (done↛∞ ⟶∞)
-helper₁ (Addˡ ⟶        ◅∞ ⟶∞) ~ ⊥-elim (done↛ ⟶)
-helper₁ (Addʳ ⟶        ◅∞ ⟶∞) ~ ⟶ ◅∞ helper₁ ⟶∞
-
-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 : Exprˢ t} {i} ->
-          run (x ⊕ y) ⟶∞[ i ] -> x ⟶⋆∞[ i ] Pred y i
-helper₂ (Red Add₁      ◅∞ ⟶∞) ~ ⊥-elim (done↛∞ ⟶∞)
-helper₂ (Red Add₂      ◅∞ ⟶∞) ~ ⊥-elim (done↛∞ ⟶∞)
-helper₂ (Red Add₃      ◅∞ ⟶∞) ~ ⊥-elim (done↛∞ ⟶∞)
-helper₂ (Red (Int int) ◅∞ ⟶∞) ~ ⊥-elim (done↛∞ ⟶∞)
-helper₂ (Addˡ ⟶        ◅∞ ⟶∞) ~ ⟶ ◅∞ helper₂ ⟶∞
-helper₂ (Addʳ ⟶        ◅∞ ⟶∞) ~ ε (_ , ≡-refl , ⟶ ◅∞ helper₁ ⟶∞)
-
-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⟶∞))
-  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⟶∞
rmfile ./Semantics/Equivalence/Add.agda
hunk ./Semantics/Equivalence/Lemmas.agda 1
+------------------------------------------------------------------------
+-- The proof of small⇒big⟶∞ uses the lemmas proved here
+------------------------------------------------------------------------
+
+module Semantics.Equivalence.Lemmas 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
+
+module Add where
+
+  helper₂ : forall {t} {y : Exprˢ t} {m i} ->
+            run (done (val m) ⊕ y) ⟶∞[ i ] -> y ⟶∞[ i ]
+  helper₂ (Red Add₁      ◅∞ ⟶∞) ~ ⊥-elim (done↛∞ ⟶∞)
+  helper₂ (Red Add₃      ◅∞ ⟶∞) ~ ⊥-elim (done↛∞ ⟶∞)
+  helper₂ (Red (Int int) ◅∞ ⟶∞) ~ ⊥-elim (done↛∞ ⟶∞)
+  helper₂ (Addˡ ⟶        ◅∞ ⟶∞) ~ ⊥-elim (done↛ ⟶)
+  helper₂ (Addʳ ⟶        ◅∞ ⟶∞) ~ ⟶ ◅∞ helper₂ ⟶∞
+
+  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 : Exprˢ t} {i} ->
+            run (x ⊕ y) ⟶∞[ i ] -> x ⟶⋆∞[ i ] Pred y i
+  helper₁ (Red Add₁      ◅∞ ⟶∞) ~ ⊥-elim (done↛∞ ⟶∞)
+  helper₁ (Red Add₂      ◅∞ ⟶∞) ~ ⊥-elim (done↛∞ ⟶∞)
+  helper₁ (Red Add₃      ◅∞ ⟶∞) ~ ⊥-elim (done↛∞ ⟶∞)
+  helper₁ (Red (Int int) ◅∞ ⟶∞) ~ ⊥-elim (done↛∞ ⟶∞)
+  helper₁ (Addˡ ⟶        ◅∞ ⟶∞) ~ ⟶ ◅∞ helper₁ ⟶∞
+  helper₁ (Addʳ ⟶        ◅∞ ⟶∞) ~ ε (_ , ≡-refl , ⟶ ◅∞ helper₂ ⟶∞)
+
+  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⟶∞))
+    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⟶∞
+
+module Seqn where
+
+  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 : Exprˢ t} {i} ->
+            run (x >> y) ⟶∞[ i ] -> x ⟶⋆∞[ i ] Pred y i
+  helper₁ (Red Seqn₁     ◅∞ ⟶∞) ~ ε (_ , ≡-refl , ⟶∞)
+  helper₁ (Red Seqn₂     ◅∞ ⟶∞) ~ ⊥-elim (done↛∞ ⟶∞)
+  helper₁ (Red (Int int) ◅∞ ⟶∞) ~ ⊥-elim (done↛∞ ⟶∞)
+  helper₁ (Seqnˡ ⟶       ◅∞ ⟶∞) ~ ⟶ ◅∞ helper₁ ⟶∞
+
+  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⟶∞))
+    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⟶∞
+
+module Catch where
+
+  helper₂ : forall {t} {y : Exprˢ t} {i} ->
+            run (done throw catch y) ⟶∞[ i ] -> y ⟶∞[ B ]
+  helper₂ (Red Catch₂    ◅∞ ⟶∞) ~ ⊥-elim (done↛∞ ⟶∞)
+  helper₂ (Red (Int int) ◅∞ ⟶∞) ~ ⊥-elim (done↛∞ ⟶∞)
+  helper₂ (Catchˡ ⟶      ◅∞ ⟶∞) ~ ⊥-elim (done↛ ⟶)
+  helper₂ (Catchʳ ⟶      ◅∞ ⟶∞) ~ ⟶ ◅∞ helper₂ ⟶∞
+
+  Pred : forall {t} -> Exprˢ t -> Status -> Exprˢ t -> Set
+  Pred y i = \x -> x ≡ done throw × y ⟶∞[ B ]
+
+  helper₁ : forall {t} {x y : Exprˢ t} {i} ->
+            run (x catch y) ⟶∞[ i ] -> x ⟶⋆∞[ i ] Pred y i
+  helper₁ (Red Catch₁    ◅∞ ⟶∞) ~ ⊥-elim (done↛∞ ⟶∞)
+  helper₁ (Red Catch₂    ◅∞ ⟶∞) ~ ⊥-elim (done↛∞ ⟶∞)
+  helper₁ (Red (Int int) ◅∞ ⟶∞) ~ ⊥-elim (done↛∞ ⟶∞)
+  helper₁ (Catchˡ ⟶      ◅∞ ⟶∞) ~ ⟶ ◅∞ helper₁ ⟶∞
+  helper₁ (Catchʳ ⟶      ◅∞ ⟶∞) ~ ε (≡-refl , ⟶ ◅∞ helper₂ ⟶∞)
+
+  lemma : forall {t} {x y : Exprˢ t} {i} ->
+          run (x catch y) ⟶∞[ i ] ->
+          ¬ ¬ (x ⟶∞[ i ] ⊎ ((x ⟶⋆[ i ] done throw) × y ⟶∞[ B ]))
+  lemma {x = x} {y} {i} x⊕y⟶∞ =
+    map-¬¬ helper $ reductio-ad-absurdum-⊎ (⋆∞⇒∞ (helper₁ x⊕y⟶∞))
+    where
+    helper : ∃ (\z -> (x ⟶⋆[ i ] z) × Pred y i z) ⊎ x ⟶∞[ i ] -> _
+    helper (inj₁ (.(done throw) , x⟶⋆↯ , ≡-refl , y⟶∞)) = inj₂ (x⟶⋆↯ , y⟶∞)
+    helper (inj₂ x⟶∞)                                   = inj₁ x⟶∞
+
+module Block where
+
+  lemma : forall {t} {x : Exprˢ t} {i} ->
+          run (block x) ⟶∞[ i ] -> x ⟶∞[ B ]
+  lemma (Red Block     ◅∞ ⟶∞) ~ ⊥-elim (done↛∞ ⟶∞)
+  lemma (Red (Int int) ◅∞ ⟶∞) ~ ⊥-elim (done↛∞ ⟶∞)
+  lemma (Blockˡ ⟶      ◅∞ ⟶∞) ~ ⟶ ◅∞ lemma ⟶∞
+
+module Unblock where
+
+  lemma : forall {t} {x : Exprˢ t} {i} ->
+          run (unblock x) ⟶∞[ i ] -> x ⟶∞[ U ]
+  lemma (Red Unblock   ◅∞ ⟶∞) ~ ⊥-elim (done↛∞ ⟶∞)
+  lemma (Red (Int int) ◅∞ ⟶∞) ~ ⊥-elim (done↛∞ ⟶∞)
+  lemma (Unblockˡ ⟶    ◅∞ ⟶∞) ~ ⟶ ◅∞ lemma ⟶∞
hunk ./Semantics/Equivalence.agda 248
--- Thorsten).
+-- Thorsten Altenkirch).
hunk ./Semantics/Equivalence.agda 250
-import Semantics.Equivalence.Add as Add
+open import Semantics.Equivalence.Lemmas
hunk ./Semantics/Equivalence.agda 254
-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
+small⇒big⟶∞ (run (val n)) i  (Red Val       ◅∞ ⟶∞) ¬⇑ = ⊥-elim (done↛∞ ⟶∞)
+small⇒big⟶∞ (run (val n)) .U (Red (Int int) ◅∞ ⟶∞) ¬⇑ = ⊥-elim (done↛∞ ⟶∞)
+small⇒big⟶∞ (run throw)   i  (Red Throw     ◅∞ ⟶∞) ¬⇑ = ⊥-elim (done↛∞ ⟶∞)
+small⇒big⟶∞ (run throw)   .U (Red (Int int) ◅∞ ⟶∞) ¬⇑ = ⊥-elim (done↛∞ ⟶∞)
+small⇒big⟶∞ (run loop)    i  ⟶∞                    ¬⇑ = ¬⇑ loop⇑
+small⇒big⟶∞ (run (x ⊕ y)) i  ⟶∞                    ¬⇑ = Add.lemma ⟶∞ helper
hunk ./Semantics/Equivalence.agda 264
-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⟶∞ (run (x >> y)) i ⟶∞ ¬⇑ = Seqn.lemma ⟶∞ helper
+  where
+  helper : x ⟶∞[ i ] ⊎ ∃ (\n -> (x ⟶⋆[ i ] done (val n)) × y ⟶∞[ i ]) -> ⊥
+  helper (inj₁ x⟶∞)              = small⇒big⟶∞ x i x⟶∞ (¬⇑ ∘ Seqn₁)
+  helper (inj₂ (n , x⟶⋆n , y⟶∞)) = small⇒big⟶∞ y i y⟶∞ (¬⇑ ∘ Seqn₂ (n , small⇒big⟶⋆ (val n) x⟶⋆n))
+small⇒big⟶∞ (run (x catch y)) i ⟶∞ ¬⇑ = Catch.lemma ⟶∞ helper
+  where
+  helper : x ⟶∞[ i ] ⊎ (x ⟶⋆[ i ] done throw) × y ⟶∞[ B ] -> ⊥
+  helper (inj₁ x⟶∞)          = small⇒big⟶∞ x i x⟶∞ (¬⇑ ∘ Catch₁)
+  helper (inj₂ (x⟶⋆↯ , y⟶∞)) = small⇒big⟶∞ y B y⟶∞ (¬⇑ ∘ Catch₂ (small⇒big⟶⋆ throw x⟶⋆↯))
+small⇒big⟶∞ (run (block x))   i ⟶∞ ¬⇑ = small⇒big⟶∞ x B (Block.lemma   ⟶∞) (¬⇑ ∘ Block)
+small⇒big⟶∞ (run (unblock x)) i ⟶∞ ¬⇑ = small⇒big⟶∞ x U (Unblock.lemma ⟶∞) (¬⇑ ∘ Unblock)