module plfa.part2.chap15_bisimulation where

open import plfa.part2.More

-- NOTE: As the last exercise requires defining a second bisimulation,
-- I've split the solution to the exercises into modules. That way I
-- can import the code from the "Bisimulation" chapter only where
-- needed, and for the last exercise reuse the same names for
-- definitions and lemmas (like _~_).

--------------------------------------------------------------------------------

module Exercise1 where
  open import plfa.part2.Bisimulation

  -- #### Exercise `_†` (practice)

  -- Formalise the translation from source to target given in the introduction.
  -- Show that `M † ≡ N` implies `M ~ N`, and conversely.

  -- **Hint:** For simplicity, we focus on only a few constructs of the language,
  -- so `_†` should be defined only on relevant terms. One way to do this is
  -- to use a decidable predicate to pick out terms in the domain of `_†`, using
  -- [proof by reflection](/Decidable/#proof-by-reflection).

  -- SOLUTION:

  -- The exercise asks for defining `_†` using the reflection trick.
  -- However, I don't see the point in doing so, because the reflection trick
  -- only helps when `_†` is called with a statically known argument, which
  -- for the formalization of bisimilarity never happens: we would always talk
  -- about something like `∀ M → ... M †` instead of a statically known
  -- application, like `ƛ (` "x") †`, where the reflection trick is actually
  -- able to infer that the argument satisfies the decidable predicate.
  --
  -- For this reason we show the definition both with the reflection trick, and
  -- without.

  open import Data.Product using (_×_; proj₁; proj₂; Σ-syntax; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
  open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; cong₂)

  module WithReflectionTrick where
    open import Data.Unit
    open import Data.Empty
    open import Relation.Nullary using (Dec; yes; no; ¬_)
    open import Relation.Nullary.Decidable using (⌊_⌋; True; toWitness; fromWitness)

    Relevant : ∀ {Γ A} → (Γ ⊢ A) → Set
    Relevant (` x) = ⊤
    Relevant (ƛ M) = Relevant M
    Relevant (L · M) = Relevant L × Relevant M
    Relevant `zero = ⊥
    Relevant (`suc M) = ⊥
    Relevant (case M M₁ M₂) = ⊥
    Relevant (μ M) = ⊥
    Relevant (con x) = ⊥
    Relevant (M `* M₁) = ⊥
    Relevant (`let M N) = Relevant M × Relevant N
    Relevant `⟨ M , M₁ ⟩ = ⊥
    Relevant (`proj₁ M) = ⊥
    Relevant (`proj₂ M) = ⊥
    Relevant (case× M M₁) = ⊥

    Relevant? : ∀ {Γ A} → (M : Γ ⊢ A) → Dec (Relevant M)
    Relevant? (` x) = yes tt
    Relevant? (ƛ M) = Relevant? M
    Relevant? (L · M)
      with Relevant? L
    ... | no ¬l = no (λ x → ¬l (proj₁ x))
    ... | yes l
      with Relevant? M
    ... | no ¬m = no (λ x → ¬m (proj₂ x))
    ... | yes m = yes ⟨ l , m ⟩
    Relevant? `zero = no (λ x → x)
    Relevant? (`suc M) = no (λ x → x)
    Relevant? (case M M₁ M₂) = no (λ x → x)
    Relevant? (μ M) = no (λ x → x)
    Relevant? (con x) = no (λ x → x)
    Relevant? (M `* M₁) = no (λ x → x)
    Relevant? (`let L M)
      with Relevant? L
    ... | no ¬l = no (λ x → ¬l (proj₁ x))
    ... | yes l
      with Relevant? M
    ... | no ¬m = no (λ x → ¬m (proj₂ x))
    ... | yes m = yes ⟨ l , m ⟩
    Relevant? `⟨ M , M₁ ⟩ = no (λ x → x)
    Relevant? (`proj₁ M) = no (λ x → x)
    Relevant? (`proj₂ M) = no (λ x → x)
    Relevant? (case× M M₁) = no (λ x → x)

    translate :  ∀ {Γ A} → (M : Γ ⊢ A) → Relevant M → (Γ ⊢ A)
    translate (` x) rel = ` x
    translate (ƛ M) rel = ƛ (translate M rel)
    translate (L · M) ⟨ fst , snd ⟩ = (translate L fst) · (translate M snd)
    translate (`let L M) ⟨ fst , snd ⟩ = (ƛ (translate M snd)) · (translate L fst)

    _† : ∀ {Γ A} → (M : Γ ⊢ A) → {True (Relevant? M)} → (Γ ⊢ A)
    (M †) {ll?} = translate M (toWitness ll?)

  module WithoutReflectionTrick where
    data Relevant : ∀ {Γ A} → (Γ ⊢ A) → Set where
      rel-` : ∀ {Γ A} {x : Γ ∋ A}
        → Relevant (` x)
      rel-ƛ : ∀ {Γ A B} {M : Γ , A ⊢ B}
        → Relevant M 
        → Relevant (ƛ M) 
      rel-· : ∀ {Γ A B} {M : Γ ⊢ A ⇒ B} {N : Γ ⊢ A}
        → Relevant M 
        → Relevant N 
        → Relevant (M · N) 
      rel-let : ∀ {Γ A B} {M : Γ ⊢ A} {N : Γ , A ⊢ B}
        → Relevant M 
        → Relevant N 
        → Relevant (`let M N) 

    -- A relevant term `Γ ⊢ᵣ A` is a pair of a regular term `Γ ⊢ A` and
    -- a proof that that term is relevant.
    _⊢ᵣ_ : Context → Type → Set
    Γ ⊢ᵣ t = Σ[ M ∈ Γ ⊢ t ] Relevant M

    tm : ∀ {Γ A} → Γ ⊢ᵣ A → Γ ⊢ A
    tm ⟨ M , rel-M ⟩ = M

    _† : ∀ {Γ A} → Γ ⊢ᵣ A → Γ ⊢ A
    ⟨ ` x      , rel-M ⟩ †               = ` x
    ⟨ ƛ M      , rel-ƛ rel-M ⟩ †         = ƛ (⟨ M , rel-M ⟩ †)
    ⟨ M · N    , rel-· rel-M rel-N ⟩ †   = (⟨ M , rel-M ⟩ †) · (⟨ N  , rel-N ⟩ †)
    ⟨ `let M N , rel-let rel-M rel-N ⟩ † = (ƛ (⟨ N , rel-N ⟩ †)) · (⟨ M , rel-M ⟩ †)

  module Lemmas where
    open WithoutReflectionTrick

    -- First Lemma

    †→~' : ∀ {Γ A} (M : Γ ⊢ᵣ A)
      → tm M ~ M †
    †→~' ⟨ ` x      , rel-M ⟩               = ~`
    †→~' ⟨ ƛ M      , rel-ƛ rel-M ⟩         = ~ƛ (†→~' ⟨ M , rel-M ⟩)
    †→~' ⟨ M · N    , rel-· rel-M rel-N ⟩   = (†→~' ⟨ M , rel-M ⟩) ~· (†→~' ⟨ N , rel-N ⟩)
    †→~' ⟨ `let M N , rel-let rel-M rel-N ⟩ = ~let (†→~' ⟨ M , rel-M ⟩) (†→~' ⟨ N , rel-N ⟩)

    †→~ : ∀ {Γ A} (M : Γ ⊢ᵣ A) (N : Γ ⊢ A)
      → M † ≡ N
      → tm M ~ N
    †→~ M .(M †) refl = †→~' M

    -- Second Lemma

    ~→† : ∀ {Γ A} (M : Γ ⊢ᵣ A) (N : Γ ⊢ A)
      → tm M ~ N
      → M † ≡ N
    ~→† ⟨ ` x        , rel ⟩                   _ ~`                 = refl
    ~→† ⟨ ƛ M        , rel-ƛ rel-M₁ ⟩          _ (~ƛ M~N)           = cong ƛ_ (~→† _ _ M~N)
    ~→† ⟨ M₁ · M₂    , rel-· rel-M₁ rel-M₂ ⟩   _ (M₁~N₁ ~· M₂~N₂)   = cong₂ _·_ (~→† _ _ M₁~N₁) (~→† _ _ M₂~N₂)
    ~→† ⟨ `let M₁ M₂ , rel-let rel-M₁ rel-N₂ ⟩ _ (~let M₁~N₁ M₂~N₂) = cong₂ (λ ■₁ ■₂ → (ƛ ■₁) · ■₂) (~→† _ _ M₂~N₂) (~→† _ _ M₁~N₁)

--------------------------------------------------------------------------------

module Exercise2 where
  open import plfa.part2.Bisimulation

  -- #### Exercise `~val⁻¹` (practice)

  -- Show that this also holds in the reverse direction: if `M ~ M†`
  -- and `Value M†` then `Value M`.

  ~val⁻¹ : ∀ {Γ A} {M M† : Γ ⊢ A}
    → M ~ M† → Value M† → Value M
  ~val⁻¹ (~ƛ M~M†) val-M† = V-ƛ

--------------------------------------------------------------------------------

module Exercise3 where
  open import plfa.part2.Bisimulation
  open Exercise2 using (~val⁻¹)

  -- #### Exercise `sim⁻¹` (practice)

  -- Show that we also have a simulation in the other direction, and hence that we have
  -- a bisimulation.

  data Arm {Γ A} (M N† : Γ ⊢ A) : Set where
    arm : ∀ {N : Γ ⊢ A}
      → M —→ N
      → N ~ N†
        --------
      → Arm M N†

  sim⁻¹ : ∀ {Γ A} {M M† N† : Γ ⊢ A} → M ~ M† → M† —→ N† → Arm M N†
  sim⁻¹ (L~L† ~· M~M†) (ξ-·₁ L†→L†′)
    with sim⁻¹ L~L† L†→L†′
  ... | arm L→N N~L†′ = arm (ξ-·₁ L→N) (N~L†′ ~· M~M†)
  sim⁻¹ (L~L† ~· M~M†) (ξ-·₂ vL† M†→M†′)
    with sim⁻¹ M~M† M†→M†′
  ... | arm M→M′ N~M′ = arm (ξ-·₂ (~val⁻¹ L~L† vL†) M→M′) (L~L† ~· N~M′)
  sim⁻¹ ((~ƛ L~L†) ~· M~M†) (β-ƛ vM†) = arm (β-ƛ (~val⁻¹ M~M† vM†)) (~sub L~L† M~M†)
  sim⁻¹ (~let M~M† N~N†) (ξ-·₂ V-ƛ M†→M†′)
    with sim⁻¹ M~M† M†→M†′
  ... | arm M→M′ M′~M†′ = arm (ξ-let M→M′) (~let M′~M†′ N~N†)
  sim⁻¹ (~let M~M† N~N†) (β-ƛ vM†) = arm (β-let (~val⁻¹ M~M† vM†)) (~sub N~N† M~M†)

--------------------------------------------------------------------------------

module Exercise4 where
  open import Data.Product using (_×_; proj₁; proj₂; Σ-syntax; ∃-syntax) renaming (_,_ to ⟨_,_⟩)

  -- #### Exercise `products` (practice)

  -- Show that the two formulations of products in
  -- Chapter [More](/More/)
  -- are in bisimulation.  The only constructs you need to include are
  -- variables, and those connected to functions and products.
  -- In this case, the simulation is _not_ lock-step.

  -- SOLUTION:

  -- Note: The simulation is still lock-step. Not sure if they were
  -- thinking of a different encoding.

  -- proj₁ ⟨ a , b ⟩ = a
  -- proj₂ ⟨ a , b ⟩ = b

  -- let ⟨ x , y ⟩ = ⟨ a , b ⟩ in e₂

  -- proj₁ e   ==   let ⟨ x , y ⟩ = e in x
  -- proj₂ e   ==   let ⟨ x , y ⟩ = e in y

  -- let ⟨ x , y ⟩ = e1 in e2   ==   let x = proj₁ e1 in let y = proj₂ e1 in e2


  infix  4 _~_
  infix  5 ~ƛ_
  infix  7 _~·_

  data _~_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where

    ~` : ∀ {Γ A} {x : Γ ∋ A}
      ---------
      → ` x ~ ` x

    ~ƛ_ : ∀ {Γ A B} {N N† : Γ , A ⊢ B}
      → N ~ N†
        ----------
      → ƛ N ~ ƛ N†

    _~·_ : ∀ {Γ A B} {L L† : Γ ⊢ A ⇒ B} {M M† : Γ ⊢ A}
      → L ~ L†
      → M ~ M†
        ---------------
      → L · M ~ L† · M†

    -- Pairs are related if they components are related.
    ~⟨_,_⟩ : ∀ {Γ A B} {M M† : Γ ⊢ A} {N N† : Γ ⊢ B}
      → M ~ M†
      → N ~ N†
        -------------------------
      → `⟨ M , N ⟩ ~ `⟨ M† , N† ⟩

    -- NOTE: `proj₁ M` is equivalent to `let (x, y) = M in x`

    ~proj₁ : ∀ {Γ A B} {M M† : Γ ⊢ A `× B}
      → M ~ M†
        ----------------------------
      → `proj₁ M ~ case× M† (` (S Z))

    -- NOTE: `proj₂ M` is equivalent to `let (x, y) = M in y`
    ~proj₂ : ∀ {Γ A B} {M M† : Γ ⊢ A `× B}
      → M ~ M†
        ------------------------
      → `proj₂ M ~ case× M† (` Z)

  _⇒ᵣ_ : Context → Context → Set
  Γ ⇒ᵣ Δ = ∀ {A} → Γ ∋ A → Δ ∋ A

  _⇒ₛ_ : Context → Context → Set
  Γ ⇒ₛ Δ = ∀ {A} → Γ ∋ A → Δ ⊢ A

  _~ₛ_ : ∀ {Γ Δ} → Γ ⇒ₛ Δ → Γ ⇒ₛ Δ → Set
  σ ~ₛ σ† = ∀ {A} (x : _ ∋ A) → σ x ~ σ† x

  ~rename : ∀ {Γ Δ} {A} {M M† : Γ ⊢ A}
    → (ρ : Γ ⇒ᵣ Δ)
    → M ~ M†
      ------------------------
    → rename ρ M ~ rename ρ M†
  ~rename ρ ~`                 = ~`
  ~rename ρ (~ƛ M~M†)          = ~ƛ (~rename (ext ρ) M~M†)
  ~rename ρ (M₁~M₁† ~· M₂~M₂†) = ~rename ρ M₁~M₁† ~· ~rename ρ M₂~M₂†
  ~rename ρ ~⟨ M~M† , M~M†₁ ⟩  = ~⟨ ~rename ρ M~M† , ~rename ρ M~M†₁ ⟩
  ~rename ρ (~proj₁ M~M†)      = ~proj₁ (~rename ρ M~M†)
  ~rename ρ (~proj₂ M~M†)      = ~proj₂ (~rename ρ M~M†)

  ~exts : ∀ {Γ Δ A} {σ σ† : Γ ⇒ₛ Δ}
    → σ ~ₛ σ†
      -----------------
    → exts σ {A = A} ~ₛ exts σ† {A = A}
  ~exts σ~σ† Z     = ~`
  ~exts σ~σ† (S x) = ~rename S_ (σ~σ† x)

  ~subst : ∀ {Γ Δ A} {M M† : Γ ⊢ A} {σ σ† : Γ ⇒ₛ Δ}
    → σ ~ₛ σ†
    → M ~ M†
      ------------------------
    → subst σ M ~ subst σ† M†
  ~subst σ~σ† (~` {x = x})         = σ~σ† x
  ~subst σ~σ† (~ƛ M~M†)            = ~ƛ (~subst (~exts σ~σ†) M~M†)
  ~subst σ~σ† (M₁~M₁† ~· M₂~M₂†)   = ~subst σ~σ† M₁~M₁† ~· ~subst σ~σ† M₂~M₂†
  ~subst σ~σ† ~⟨ M₁~M₁† , M₂~M₂† ⟩ = ~⟨ ~subst σ~σ† M₁~M₁† , ~subst σ~σ† M₂~M₂† ⟩
  ~subst σ~σ† (~proj₁ M~M†)        = ~proj₁ (~subst σ~σ† M~M†)
  ~subst σ~σ† (~proj₂ M~M†)        = ~proj₂ (~subst σ~σ† M~M†)

  ~substZero : ∀ {Γ A} {M M† : Γ ⊢ A}
    → M ~ M†
    → substZero M ~ₛ substZero M†
  ~substZero M~M† Z     = M~M†
  ~substZero M~M† (S x) = ~`

  ~sub : ∀ {Γ A B} {N N† : Γ , B ⊢ A} {M M† : Γ ⊢ B}
    → N ~ N†
    → M ~ M†
      -----------------------
    → (N [ M ]) ~ (N† [ M† ])
  ~sub N~N† M~M† = ~subst (~substZero M~M†) N~N†

  -- Forwards-Direction

  ~val : ∀ {Γ A} {M M† : Γ ⊢ A}
    → M ~ M†
    → Value M
      --------
    → Value M†
  ~val (~ƛ M~M†)            val-M                 = V-ƛ
  ~val ~⟨ M₁~M₁† , M₂~M₂† ⟩ V-⟨ val-M₁ , val-M₂ ⟩ = V-⟨ ~val M₁~M₁† val-M₁ , ~val M₂~M₂† val-M₂ ⟩

  sim : ∀ {Γ A} {M M† M′ : Γ ⊢ A}
    → M ~ M†
    → M —→ M′
      -----------------------------
    → ∃[ M′† ] (M′ ~ M′†) × (M† —→ M′†)
  sim (M₁~M₁† ~· M₂~M₂†) (ξ-·₁ M₁—→M₁′)
   with sim M₁~M₁† M₁—→M₁′
  ... | ⟨ M₁′†       , ⟨ M₁′~M₁′†           ,       M₁†—→M₁′† ⟩ ⟩
      = ⟨ (M₁′† · _) , ⟨ M₁′~M₁′† ~· M₂~M₂† , (ξ-·₁ M₁†—→M₁′†) ⟩ ⟩
  sim (M₁~M₁† ~· M₂~M₂†) (ξ-·₂ val-M₁ M₂—→M₂′)
   with sim M₂~M₂† M₂—→M₂′
  ... | ⟨ M₂′†       , ⟨ M₂′~M₂′†           ,                            M₂†—→M₂′† ⟩ ⟩
      = ⟨ (_ · M₂′†) , ⟨ M₁~M₁† ~· M₂′~M₂′† , (ξ-·₂ (~val M₁~M₁† val-M₁) M₂†—→M₂′†) ⟩ ⟩
  sim ((~ƛ M₁~M₁†) ~· M₂~M₂†) (β-ƛ val-M₂)
      = ⟨ _ , ⟨ ~sub M₁~M₁† M₂~M₂† , β-ƛ (~val M₂~M₂† val-M₂) ⟩ ⟩
  sim ~⟨ M₁~M₁† , M₂~M₂† ⟩ (ξ-⟨,⟩₁ M₁—→M₁′)
   with sim M₁~M₁† M₁—→M₁′
  ... | ⟨ M₁′†          , ⟨ M₁′~M₁′†               ,        M₁†—→M₁′† ⟩ ⟩
      = ⟨ `⟨ M₁′† , _ ⟩ , ⟨ ~⟨ M₁′~M₁′† , M₂~M₂† ⟩ , ξ-⟨,⟩₁ M₁†—→M₁′† ⟩ ⟩
  sim ~⟨ M₁~M₁† , M₂~M₂† ⟩ (ξ-⟨,⟩₂ val-M₁ M₂—→M₂′)
   with sim M₂~M₂† M₂—→M₂′
  ... | ⟨ M₂′†          , ⟨ M₂′~M₂′†               ,                             M₂†—→M₂′† ⟩ ⟩
      = ⟨ `⟨ _ , M₂′† ⟩ , ⟨ ~⟨ M₁~M₁† , M₂′~M₂′† ⟩ , ξ-⟨,⟩₂ (~val M₁~M₁† val-M₁) M₂†—→M₂′† ⟩ ⟩
  sim (~proj₁ M~M†) (ξ-proj₁ M—→M′)
   with sim M~M† M—→M′
  ... | ⟨ M′†                 , ⟨ M′~M′†        ,         M†—→M′† ⟩ ⟩
      = ⟨ case× M′† (` (S Z)) , ⟨ ~proj₁ M′~M′† , ξ-case× M†—→M′† ⟩ ⟩
  sim (~proj₁ ~⟨ M₁~M₁† , M₂~M₂† ⟩) (β-proj₁ val-M₁ val-M₂)
      = ⟨ _ , ⟨ M₁~M₁† , β-case× (~val M₁~M₁† val-M₁) (~val M₂~M₂† val-M₂) ⟩ ⟩
  sim (~proj₂ M~M†) (ξ-proj₂ M—→M′)
   with sim M~M† M—→M′
  ... | ⟨ M′†             , ⟨ M′~M′†        ,         M†—→M′† ⟩ ⟩
      = ⟨ case× M′† (` Z) , ⟨ ~proj₂ M′~M′† , ξ-case× M†—→M′† ⟩ ⟩
  sim (~proj₂ ~⟨ M₁~M₁† , M₂~M₂† ⟩) (β-proj₂ val-M₁ val-M₂)
      = ⟨ _ , ⟨ M₂~M₂† , β-case× (~val M₁~M₁† val-M₁) (~val M₂~M₂† val-M₂) ⟩ ⟩

  -- Backwards-Direction

  ~val⁻¹ : ∀ {Γ A} {M M† : Γ ⊢ A}
    → M ~ M†
    → Value M†
      --------
    → Value M
  ~val⁻¹ (~ƛ M~M†)            val-M†                  = V-ƛ
  ~val⁻¹ ~⟨ M₁~M₁† , M₂~M₂† ⟩ V-⟨ val-M₁† , val-M₂† ⟩ = V-⟨ ~val⁻¹ M₁~M₁† val-M₁† , ~val⁻¹ M₂~M₂† val-M₂† ⟩

  sim⁻¹ : ∀ {Γ A} {M M† M′† : Γ ⊢ A}
    → M ~ M†
    → M† —→ M′†
    → ∃[ M′ ] (M′ ~ M′†) × (M —→ M′)
  sim⁻¹ (M₁~M₁† ~· M₂~M₂†) (ξ-·₁ M₁†—→M₁′†)
   with sim⁻¹ M₁~M₁† M₁†—→M₁′†
  ... | ⟨ M₁′     , ⟨ M₁′~M₁′†           ,      M₁—→M₁′ ⟩ ⟩
      = ⟨ M₁′ · _ , ⟨ M₁′~M₁′† ~· M₂~M₂† , ξ-·₁ M₁—→M₁′ ⟩ ⟩
  sim⁻¹ (M₁~M₁† ~· M₂~M₂†) (ξ-·₂ val-M₁† M₂†—→M₂′†)
   with sim⁻¹ M₂~M₂† M₂†—→M₂′†
  ... | ⟨ M₂′     , ⟨ M₂′~M₂′†           ,      M₂—→M₂′ ⟩ ⟩
      = ⟨ _ · M₂′ , ⟨ M₁~M₁† ~· M₂′~M₂′† , ξ-·₂ (~val⁻¹ M₁~M₁† val-M₁†) M₂—→M₂′ ⟩ ⟩
  sim⁻¹ ((~ƛ M₁~M₁†) ~· M₂~M₂†) (β-ƛ val-M₂†)
      = ⟨ _ , ⟨ (~sub M₁~M₁† M₂~M₂†) , (β-ƛ (~val⁻¹ M₂~M₂† val-M₂†)) ⟩ ⟩
  sim⁻¹ ~⟨ M₁~M₁† , M₂~M₂† ⟩ (ξ-⟨,⟩₁ M₁†—→M₁′†)
   with sim⁻¹ M₁~M₁† M₁†—→M₁′†
  ... | ⟨ M₁′     , ⟨ M₁′~M₁′†           ,      M₁—→M₁′ ⟩ ⟩
      = ⟨ `⟨ M₁′ , _ ⟩ , ⟨ ~⟨ M₁′~M₁′† , M₂~M₂† ⟩ , ξ-⟨,⟩₁ M₁—→M₁′ ⟩ ⟩
  sim⁻¹ ~⟨ M₁~M₁† , M₂~M₂† ⟩ (ξ-⟨,⟩₂ val-M₁† M₂†—→M₂′†)
   with sim⁻¹ M₂~M₂† M₂†—→M₂′†
  ... | ⟨ M₂′     , ⟨ M₂′~M₂′†           ,      M₂—→M₂′ ⟩ ⟩
      = ⟨ `⟨ _ , M₂′ ⟩ , ⟨ ~⟨ M₁~M₁† , M₂′~M₂′† ⟩ , ξ-⟨,⟩₂ (~val⁻¹ M₁~M₁† val-M₁†) M₂—→M₂′ ⟩ ⟩
  sim⁻¹ (~proj₁ M~M†) (ξ-case× M†—→M′†)
   with sim⁻¹ M~M† M†—→M′†
  ... | ⟨ M′        , ⟨        M′~M′† ,         M—→M′ ⟩ ⟩
      = ⟨ `proj₁ M′ , ⟨ ~proj₁ M′~M′† , ξ-proj₁ M—→M′ ⟩ ⟩
  sim⁻¹ (~proj₁ ~⟨ M₁~M₁† , M₂~M₂† ⟩) (β-case× val-M₁† val-M₂†)
      = ⟨ _ , ⟨ M₁~M₁† , β-proj₁ (~val⁻¹ M₁~M₁† val-M₁†) (~val⁻¹ M₂~M₂† val-M₂†) ⟩ ⟩
  sim⁻¹ (~proj₂ M~M†) (ξ-case× M†—→M′†)
   with sim⁻¹ M~M† M†—→M′†
  ... | ⟨ M′        , ⟨        M′~M′† ,         M—→M′ ⟩ ⟩
      = ⟨ `proj₂ M′ , ⟨ ~proj₂ M′~M′† , ξ-proj₂ M—→M′ ⟩ ⟩
  sim⁻¹ (~proj₂ ~⟨ M₁~M₁† , M₂~M₂† ⟩) (β-case× val-M₁† val-M₂†)
      = ⟨ _ , ⟨ M₂~M₂† , β-proj₂ (~val⁻¹ M₁~M₁† val-M₁†) (~val⁻¹ M₂~M₂† val-M₂†) ⟩ ⟩