moved Bisimulation to separate chapter

index.md

@@ -43,7 +43,8 @@ are encouraged.
   - [Lambda: Lambda: Introduction to Lambda Calculus]({{ site.baseurl }}{% link out/plta/Lambda.md %})
   - [Properties: Progress and Preservation]({{ site.baseurl }}{% link out/plta/Properties.md %})
   - [DeBruijn: Inherently typed De Bruijn representation]({{ site.baseurl }}{% link out/plta/DeBruijn.md %})
-  - [Extensions: Extensions to simply-typed lambda calculus]({{ site.baseurl }}{% link out/plta/Extensions.md %})
+  - [More: More constructs of simply-typed lambda calculus]({{ site.baseurl }}{% link out/plta/More.md %}) 
+  - [Bisimulation: Relating reductions systems]({{ site.baseurl }}{% link out/plta/Bisimulation.md %}) 
   - [Inference: Bidirectional type inference]({{ site.baseurl }}{% link out/plta/Inference.md %})
   - [Untyped: Untyped lambda calculus with full normalisation]({{ site.baseurl }}{% link out/plta/Untyped.md %})
 

src/plta/More.lagda

@@ -627,126 +627,3 @@ eval (gas (suc m)) L with progress L
 ...    | steps M—↠N fin                  =  steps (L —→⟨ L—→M ⟩ M—↠N) fin
 \end{code}
 
-
-## Bisimulation
-
-\begin{code}
-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ₜ)
-
-  ~let : ∀ {Γ A B} {Mₛ Mₜ : Γ ⊢ A} {Nₛ Nₜ : Γ , A ⊢ B}
-    → Mₛ ~ Mₜ
-    → Nₛ ~ Nₜ
-      ----------------------------
-    → (`let Mₛ Nₛ) ~ ((ƛ Nₜ) · Mₜ)
-\end{code}
-
-\begin{code}
-data BiVal {Γ A} (Vₛ Vₜ : Γ ⊢ A) : Set where
-
-  val :
-      Value Vₜ
-      ----------
-    → BiVal Vₛ Vₜ
-
-bival : ∀ {Γ A} {Vₛ Vₜ : Γ ⊢ A} 
-  → Vₛ ~ Vₜ
-  → Value Vₛ
-    -----------
-  → BiVal Vₛ Vₜ
-bival ~` ()
-bival (~ƛ Vₛ~Vₜ) V-ƛ = val V-ƛ
-bival (~· Vₛ~Vₜ Vₛ~Vₜ₁) ()
-bival (~let Vₛ~Vₜ Vₛ~Vₜ₁) ()
-
-bivar : ∀ {Γ A B} {x : Γ , B ∋ A} {Vₛ Vₜ : Γ ⊢ B} 
-  → Vₛ ~ Vₜ
-    -------------------------------
-  → ((` x) [ Vₛ ]) ~ ((` x) [ Vₜ ])
-bivar {x = Z} Vₛ~Vₜ = Vₛ~Vₜ
-bivar {x = S x} Vₛ~Vₜ = ~`
-
-biren : ∀ {Γ Δ}
-  → (ρ : ∀ {A} → Γ ∋ A → Δ ∋ A)
-    ---------------------------
-  → (∀ {A} {Mₛ Mₜ : Γ ⊢ A}
-     → Mₛ ~ Mₜ
-     → rename ρ Mₛ ~ rename ρ Mₜ)
-biren ρ (~` {x = x}) = ~`
-biren ρ (~ƛ ~N) = ~ƛ (biren (ext ρ) ~N)
-biren ρ (~· ~L ~M) = ~· (biren ρ ~L) (biren ρ ~M)
-biren ρ (~let ~M ~N) = ~let (biren ρ ~M) (biren (ext ρ) ~N)
-
-biexts : ∀ {Γ Δ}
-  → {σₛ : ∀ {A} → Γ ∋ A → Δ ⊢ A}
-  → {σₜ : ∀ {A} → Γ ∋ A → Δ ⊢ A}
-  → (∀ {A} → (x : Γ ∋ A) → σₛ x ~ σₜ x)
-    -----------------------------------
-  → (∀ {A B} → (x : Γ , B ∋ A) → exts σₛ x ~ exts σₜ x)
-biexts ~σ Z =  ~`
-biexts ~σ (S x) =  biren S_ (~σ x)
-
-bisubst : ∀ {Γ Δ}
-  → {σₛ : ∀ {A} → Γ ∋ A → Δ ⊢ A}
-  → {σₜ : ∀ {A} → Γ ∋ A → Δ ⊢ A}
-  → (∀ {A} → (x : Γ ∋ A) → σₛ x ~ σₜ x)
-    -----------------------------------
-  → (∀ {A} {Mₛ Mₜ : Γ ⊢ A}
-     → Mₛ ~ Mₜ
-     → subst σₛ Mₛ ~ subst σₜ Mₜ)
-bisubst ~σ (~` {x = x}) = ~σ x
-bisubst ~σ (~ƛ ~N) = ~ƛ (bisubst (biexts ~σ) ~N)
-bisubst ~σ (~· ~L ~M) = ~· (bisubst ~σ ~L) (bisubst ~σ ~M)
-bisubst ~σ (~let ~M ~N) = ~let (bisubst ~σ ~M) (bisubst (biexts ~σ) ~N)
-
-bisub : ∀ {Γ A B} {Nₛ Nₜ : Γ , B ⊢ A} {Vₛ Vₜ : Γ ⊢ B} 
-  → Nₛ ~ Nₜ
-  → Vₛ ~ Vₜ
-    -------------------------
-  → (Nₛ [ Vₛ ]) ~ (Nₜ [ Vₜ ])
-bisub {Γ} {A} {B} ~N ~V = bisubst {Γ , B} {Γ} ~σ {A} ~N
-  where
-  ~σ : ∀ {A} → (x : Γ , B ∋ A) → _ ~ _
-  ~σ Z      =  ~V
-  ~σ (S x)  =  ~`
-
-data Bisim {Γ A} (Mₛ Mₜ Mₛ′ : Γ ⊢ A) : Set where
-
-  bi : ∀ {Mₜ′ : Γ ⊢ A}
-    → (Mₛ′ ~ Mₜ′)
-    → (Mₜ —→ Mₜ′)
-      ---------------
-    → Bisim Mₛ Mₜ Mₛ′
-
-bisim : ∀ {Γ A} {Mₛ Mₜ Mₛ′ : Γ ⊢ A}
-  → Mₛ ~ Mₜ
-  → Mₛ —→ Mₛ′
-    ---------------
-  → Bisim Mₛ Mₜ Mₛ′
-bisim ~` ()
-bisim (~ƛ Nₛ~Nₜ) ()
-bisim (~· Lₛ~Lₜ Mₛ~Mₜ) (ξ-·₁ Lₛ—→Lₛ′) with bisim Lₛ~Lₜ Lₛ—→Lₛ′
-... | bi Lₛ′~Lₜ′ Lₜ—→Lₜ′ =  bi (~· Lₛ′~Lₜ′ Mₛ~Mₜ) (ξ-·₁ Lₜ—→Lₜ′)
-bisim (~· Lₛ~Lₜ Mₛ~Mₜ) (ξ-·₂ VLₛ Mₛ—→Mₛ′) with bival Lₛ~Lₜ VLₛ | bisim Mₛ~Mₜ Mₛ—→Mₛ′ 
-... | val VLₜ | bi Mₛ′~Mₜ′ Mₜ—→Mₜ′ =  bi (~· Lₛ~Lₜ Mₛ′~Mₜ′) (ξ-·₂ VLₜ Mₜ—→Mₜ′)
-bisim (~· (~ƛ Nₛ~Nₜ) Mₛ~Mₜ) (β-ƛ VMₛ) with bival Mₛ~Mₜ VMₛ
-... | val VMₜ  =  bi (bisub Nₛ~Nₜ Mₛ~Mₜ) (β-ƛ VMₜ)
-bisim (~let Mₛ~Mₜ Nₛ~Nₜ) (ξ-let Mₛ—→Mₛ′) with bisim Mₛ~Mₜ Mₛ—→Mₛ′
-... | bi Mₛ′~Mₜ′ Mₜ—→Mₜ′ =  bi (~let Mₛ′~Mₜ′ Nₛ~Nₜ) (ξ-·₂ V-ƛ Mₜ—→Mₜ′)
-bisim (~let Mₛ~Mₜ Nₛ~Nₜ) (β-let VMₛ) with bival Mₛ~Mₜ VMₛ
-... | val VMₜ  =  bi (bisub Nₛ~Nₜ Mₛ~Mₜ) (β-ƛ VMₜ)
-\end{code}