------------------------------------------------------------------------
-- 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.Function

module Add where

  helper :  {t} {y : Exprˢ t} {m i} 
           run (done (nat m)  y) ⟶∞[ i ]  y ⟶∞[ i ]
  helper (Red Add₁           ◅∞ ⟶∞) = ⊥-elim (done↛∞ ⟶∞)
  helper (Red Add₃           ◅∞ ⟶∞) = ⊥-elim (done↛∞ ⟶∞)
  helper (Red (Int int)      ◅∞ ⟶∞) = ⊥-elim (done↛∞ ⟶∞)
  helper (Addʳ              ◅∞ ⟶∞) ~  ◅∞ helper ⟶∞
  helper (Addˡ (Red (Int _)) ◅∞ Red (Int ())        ◅∞ ⟶∞)
  helper (Addˡ (Red (Int _)) ◅∞ Addˡ (Red (Int ())) ◅∞ ⟶∞)
  helper (Addˡ (Red (Int _)) ◅∞ Red Add₂            ◅∞ ⟶∞) =
    ⊥-elim (done↛∞ ⟶∞)

  data Pred {t} (y : Exprˢ t) i : Exprˢ t  Set where
     :  n (y⟶∞ : y ⟶∞[ i ])  Pred y i (done (nat n))

  lemma :  {t} {x y : Exprˢ t} {i} 
          run (x  y) ⟶∞[ i ]  x ⟶⋆∞[ i ] Pred y i
  lemma (Red Add₁      ◅∞ ⟶∞) = ⊥-elim (done↛∞ ⟶∞)
  lemma (Red Add₂      ◅∞ ⟶∞) = ⊥-elim (done↛∞ ⟶∞)
  lemma (Red Add₃      ◅∞ ⟶∞) = ⊥-elim (done↛∞ ⟶∞)
  lemma (Red (Int int) ◅∞ ⟶∞) = ⊥-elim (done↛∞ ⟶∞)
  lemma (Addˡ         ◅∞ ⟶∞) ~  ◅∞ lemma ⟶∞
  lemma (Addʳ         ◅∞ ⟶∞) = ε ( _ ( ◅∞ helper ⟶∞))

module Seqn where

  open Add public using (Pred;)

  lemma :  {t} {x y : Exprˢ t} {i} 
          run (x >> y) ⟶∞[ i ]  x ⟶⋆∞[ i ] Pred y i
  lemma (Red Seqn₁     ◅∞ ⟶∞) = ε ( _ ⟶∞)
  lemma (Red Seqn₂     ◅∞ ⟶∞) = ⊥-elim (done↛∞ ⟶∞)
  lemma (Red (Int int) ◅∞ ⟶∞) = ⊥-elim (done↛∞ ⟶∞)
  lemma (Seqnˡ        ◅∞ ⟶∞) ~  ◅∞ lemma ⟶∞

module Catch where

  helper :  {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ˡ (Red (Int ())) ◅∞ ⟶∞)
  helper (Catchʳ               ◅∞ ⟶∞) ~  ◅∞ helper ⟶∞

  data Pred {t} (y : Exprˢ t) i : Exprˢ t  Set where
     : (y⟶∞ : y ⟶∞[ B ])  Pred y i (done throw)

  lemma :  {t} {x y : Exprˢ t} {i} 
          run (x catch y) ⟶∞[ i ]  x ⟶⋆∞[ i ] Pred y i
  lemma (Red Catch₁    ◅∞ ⟶∞) = ⊥-elim (done↛∞ ⟶∞)
  lemma (Red Catch₂    ◅∞ ⟶∞) = ⊥-elim (done↛∞ ⟶∞)
  lemma (Red (Int int) ◅∞ ⟶∞) = ⊥-elim (done↛∞ ⟶∞)
  lemma (Catchˡ       ◅∞ ⟶∞) ~  ◅∞ lemma ⟶∞
  lemma (Catchʳ       ◅∞ ⟶∞) = ε ( ( ◅∞ helper ⟶∞))

module Block where

  lemma :  {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 :  {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 ⟶∞

module Loop where

  data Pred i : Exprˢ partial  Set where
     :  n  Pred i (done (nat n))

  helper :  {y i x}  Seqn.Pred y i x  Pred i x
  helper (Seqn. n _) =  n

  lemma :  {x i}  run (loop x) ⟶∞[ i ]  x ⟶⋆∞[ i ] Pred i
  lemma (Red Loop      ◅∞ ⟶∞) = map⋆∞ id id helper (Seqn.lemma ⟶∞)
  lemma (Red (Int int) ◅∞ ⟶∞) = ⊥-elim (done↛∞ ⟶∞)