From 8aa70272568b3a829e129425dda1df68c81e6cd9 Mon Sep 17 00:00:00 2001 From: Jeremy Siek Date: Sun, 19 May 2019 16:45:27 -0400 Subject: [PATCH] more cleanup --- src/plfa/CallByName.lagda | 121 ++++++++++++++------------- src/plfa/Confluence.lagda | 6 +- src/plfa/Substitution.lagda | 159 ++++++++++++++++++------------------ 3 files changed, 144 insertions(+), 142 deletions(-) diff --git a/src/plfa/CallByName.lagda b/src/plfa/CallByName.lagda index 730dac11..0c53d896 100644 --- a/src/plfa/CallByName.lagda +++ b/src/plfa/CallByName.lagda @@ -20,7 +20,7 @@ open import plfa.LambdaReduction using (β; ξ₁; ξ₂; ζ; _—→_; _—↠_; _—→⟨_⟩_; _[]; —↠-trans; appL-cong) open import plfa.Soundness using (Subst) open import plfa.Substitution - using (⧼_⧽; _•_; _⨟_; ids; sub-id; sub-sub; subst-zero-exts-cons) + using (⟪_⟫; _•_; _⨟_; ids; sub-id; sub-sub; subst-zero-exts-cons) import Relation.Binary.PropositionalEquality as Eq open Eq using (_≡_; refl; trans; sym) open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎) @@ -166,21 +166,21 @@ expand the conclusion of the statement, stating that the results are equivalent. We make the two notions of equivalence precise by defining the -following two mutually-recursive predicates `c ≈ M` and `γ ≃ σ`. +following two mutually-recursive predicates `c ≈ M` and `γ ≈ₑ σ`. \begin{code} _≈_ : Clos → (∅ ⊢ ★) → Set -_≃_ : ∀{Γ} → ClosEnv Γ → Subst Γ ∅ → Set +_≈ₑ_ : ∀{Γ} → ClosEnv Γ → Subst Γ ∅ → Set -(clos {Γ} M γ) ≈ N = Σ[ σ ∈ Subst Γ ∅ ] γ ≃ σ × (N ≡ ⧼ σ ⧽ M) +(clos {Γ} M γ) ≈ N = Σ[ σ ∈ Subst Γ ∅ ] γ ≈ₑ σ × (N ≡ ⟪ σ ⟫ M) -γ ≃ σ = ∀{x} → (γ x) ≈ (σ x) +γ ≈ₑ σ = ∀{x} → (γ x) ≈ (σ x) \end{code} We can now state the main lemma: - If γ ⊢ M ⇓ c and γ ≃ σ, - then ⧼ σ ⧽ M —↠ N and c ≈ N for some N. + If γ ⊢ M ⇓ c and γ ≈ₑ σ, + then ⟪ σ ⟫ M —↠ N and c ≈ N for some N. Before starting the proof, we establish a couple lemmas about equivalent environments and substitutions. @@ -188,33 +188,33 @@ about equivalent environments and substitutions. The empty environment is equivalent to the identity substitution. \begin{code} -≃-id : ∅' ≃ ids -≃-id {()} +≈ₑ-id : ∅' ≈ₑ ids +≈ₑ-id {()} \end{code} We define an auxilliary function for extending a substitution. \begin{code} ext-subst : ∀{Γ Δ} → Subst Γ Δ → Δ ⊢ ★ → Subst (Γ , ★) Δ -ext-subst{Γ}{Δ} σ N {A} = ⧼ subst-zero N ⧽ ∘ exts σ +ext-subst{Γ}{Δ} σ N {A} = ⟪ subst-zero N ⟫ ∘ exts σ \end{code} The next lemma states that if you start with an equivalent -environment and substitution `γ ≃ σ`, extending them with +environment and substitution `γ ≈ₑ σ`, extending them with an equivalent closure and term `c ≈ N` produces an equivalent environment and substitution: -`(γ ,' c) ≃ (ext-subst σ N)`. +`(γ ,' c) ≈ₑ (ext-subst σ N)`. \begin{code} -≃-ext : ∀ {Γ} {γ : ClosEnv Γ} {σ : Subst Γ ∅} {c} {N : ∅ ⊢ ★} - → γ ≃ σ → c ≈ N +≈ₑ-ext : ∀ {Γ} {γ : ClosEnv Γ} {σ : Subst Γ ∅} {c} {N : ∅ ⊢ ★} + → γ ≈ₑ σ → c ≈ N -------------------------- - → (γ ,' c) ≃ (ext-subst σ N) -≃-ext {Γ} {γ} {σ} {c} {N} γ≃σ c≈N {x} = goal + → (γ ,' c) ≈ₑ (ext-subst σ N) +≈ₑ-ext {Γ} {γ} {σ} {c} {N} γ≈ₑσ c≈N {x} = goal where - ext-cons : (γ ,' c) ≃ (N • σ) + ext-cons : (γ ,' c) ≈ₑ (N • σ) ext-cons {Z} = c≈N - ext-cons {S x} = γ≃σ + ext-cons {S x} = γ≈ₑσ goal : (γ ,' c) x ≈ ext-subst σ N x goal @@ -222,45 +222,45 @@ an equivalent environment and substitution: ... | a rewrite sym (subst-zero-exts-cons{Γ}{∅}{σ}{★}{N}{★}) = a \end{code} -To prove `≃-ext`, we make use of the fact that `ext-subst σ N` is +To prove `≈ₑ-ext`, we make use of the fact that `ext-subst σ N` is equivalent to `N • σ` (by `subst-zero-exts-cons`). So we just -need to prove that `(γ ,' c) ≃ (N • σ)`, which is easy. +need to prove that `(γ ,' c) ≈ₑ (N • σ)`, which is easy. We proceed by cases on the input variable. * If it is `Z`, then we immediately conclude using the premise `c ≈ N`. * If it is `S x`, then we immediately conclude using - premise `γ ≃ σ`. + premise `γ ≈ₑ σ`. We arive at the main lemma: if `M` big steps to a -closure `c` in environment `γ`, and if `γ ≃ σ`, then `⧼ σ ⧽ M` reduces +closure `c` in environment `γ`, and if `γ ≈ₑ σ`, then `⟪ σ ⟫ M` reduces to some term `N` that is equivalent to `c`. We describe the proof below. \begin{code} ⇓→—↠×𝔹 : ∀{Γ}{γ : ClosEnv Γ}{σ : Subst Γ ∅}{M : Γ ⊢ ★}{c : Clos} - → γ ⊢ M ⇓ c → γ ≃ σ + → γ ⊢ M ⇓ c → γ ≈ₑ σ --------------------------------------- - → Σ[ N ∈ ∅ ⊢ ★ ] (⧼ σ ⧽ M —↠ N) × c ≈ N -⇓→—↠×𝔹 {γ = γ} (⇓-var{x = x} γx≡Lδ δ⊢L⇓c) γ≃σ - with γ x | γ≃σ {x} | γx≡Lδ -... | clos L δ | ⟨ τ , ⟨ δ≃τ , σx≡τL ⟩ ⟩ | refl - with ⇓→—↠×𝔹{σ = τ} δ⊢L⇓c δ≃τ + → Σ[ N ∈ ∅ ⊢ ★ ] (⟪ σ ⟫ M —↠ N) × c ≈ N +⇓→—↠×𝔹 {γ = γ} (⇓-var{x = x} γx≡Lδ δ⊢L⇓c) γ≈ₑσ + with γ x | γ≈ₑσ {x} | γx≡Lδ +... | clos L δ | ⟨ τ , ⟨ δ≈ₑτ , σx≡τL ⟩ ⟩ | refl + with ⇓→—↠×𝔹{σ = τ} δ⊢L⇓c δ≈ₑτ ... | ⟨ N , ⟨ τL—↠N , c≈N ⟩ ⟩ rewrite σx≡τL = ⟨ N , ⟨ τL—↠N , c≈N ⟩ ⟩ -⇓→—↠×𝔹 {σ = σ} {c = clos (ƛ N) γ} ⇓-lam γ≃σ = - ⟨ ⧼ σ ⧽ (ƛ N) , ⟨ ⧼ σ ⧽ (ƛ N) [] , ⟨ σ , ⟨ γ≃σ , refl ⟩ ⟩ ⟩ ⟩ -⇓→—↠×𝔹{Γ}{γ} {σ = σ} {L · M} {c} (⇓-app {N = N} L⇓ƛNδ N⇓c) γ≃σ - with ⇓→—↠×𝔹{σ = σ} L⇓ƛNδ γ≃σ -... | ⟨ _ , ⟨ σL—↠ƛτN , ⟨ τ , ⟨ δ≃τ , ≡ƛτN ⟩ ⟩ ⟩ ⟩ rewrite ≡ƛτN - with ⇓→—↠×𝔹 {σ = ext-subst τ (⧼ σ ⧽ M)} N⇓c - (λ {x} → ≃-ext{σ = τ} δ≃τ ⟨ σ , ⟨ γ≃σ , refl ⟩ ⟩ {x}) - | β{∅}{⧼ exts τ ⧽ N}{⧼ σ ⧽ M} +⇓→—↠×𝔹 {σ = σ} {c = clos (ƛ N) γ} ⇓-lam γ≈ₑσ = + ⟨ ⟪ σ ⟫ (ƛ N) , ⟨ ⟪ σ ⟫ (ƛ N) [] , ⟨ σ , ⟨ γ≈ₑσ , refl ⟩ ⟩ ⟩ ⟩ +⇓→—↠×𝔹{Γ}{γ} {σ = σ} {L · M} {c} (⇓-app {N = N} L⇓ƛNδ N⇓c) γ≈ₑσ + with ⇓→—↠×𝔹{σ = σ} L⇓ƛNδ γ≈ₑσ +... | ⟨ _ , ⟨ σL—↠ƛτN , ⟨ τ , ⟨ δ≈ₑτ , ≡ƛτN ⟩ ⟩ ⟩ ⟩ rewrite ≡ƛτN + with ⇓→—↠×𝔹 {σ = ext-subst τ (⟪ σ ⟫ M)} N⇓c + (λ {x} → ≈ₑ-ext{σ = τ} δ≈ₑτ ⟨ σ , ⟨ γ≈ₑσ , refl ⟩ ⟩ {x}) + | β{∅}{⟪ exts τ ⟫ N}{⟪ σ ⟫ M} ... | ⟨ N' , ⟨ —↠N' , c≈N' ⟩ ⟩ | ƛτN·σM—→ - rewrite sub-sub{M = N}{σ₁ = exts τ}{σ₂ = subst-zero (⧼ σ ⧽ M)} = - let rs = (ƛ ⧼ exts τ ⧽ N) · ⧼ σ ⧽ M —→⟨ ƛτN·σM—→ ⟩ —↠N' in + rewrite sub-sub{M = N}{σ₁ = exts τ}{σ₂ = subst-zero (⟪ σ ⟫ M)} = + let rs = (ƛ ⟪ exts τ ⟫ N) · ⟪ σ ⟫ M —→⟨ ƛτN·σM—→ ⟩ —↠N' in let g = —↠-trans (appL-cong σL—↠ƛτN) rs in ⟨ N' , ⟨ g , c≈N' ⟩ ⟩ \end{code} @@ -270,51 +270,51 @@ to consider. * Case `⇓-var`. So we have `γ x ≡ clos L δ` and `δ ⊢ L ⇓ c`. - We need to show that `⧼ σ ⧽ x —↠ N` and `c ≈ N` for some `N`. - The premise `γ ≃ σ` tells us that `γ x ≈ σ x`, so `clos L δ ≈ σ x`. + We need to show that `⟪ σ ⟫ x —↠ N` and `c ≈ N` for some `N`. + The premise `γ ≈ₑ σ` tells us that `γ x ≈ σ x`, so `clos L δ ≈ σ x`. By the definition of `≈`, there exists a `τ` such that - `δ ≃ τ` and `σ x ≡ ⧼ τ ⧽ L `. - Using `δ ⊢ L ⇓ c` and `δ ≃ τ`, + `δ ≈ₑ τ` and `σ x ≡ ⟪ τ ⟫ L `. + Using `δ ⊢ L ⇓ c` and `δ ≈ₑ τ`, the induction hypothesis gives us - `⧼ τ ⧽ L —↠ N` and `c ≈ N` for some `N`. - So we have shown that `⧼ σ ⧽ x —↠ N` and `c ≈ N` for some `N`. + `⟪ τ ⟫ L —↠ N` and `c ≈ N` for some `N`. + So we have shown that `⟪ σ ⟫ x —↠ N` and `c ≈ N` for some `N`. * Case `⇓-lam`. - We immediately have `⧼ σ ⧽ (ƛ N) —↠ ⧼ σ ⧽ (ƛ N)` - and `clos (⧼ σ ⧽ (ƛ N)) γ ≈ ⧼ σ ⧽ (ƛ N)`. + We immediately have `⟪ σ ⟫ (ƛ N) —↠ ⟪ σ ⟫ (ƛ N)` + and `clos (⟪ σ ⟫ (ƛ N)) γ ≈ ⟪ σ ⟫ (ƛ N)`. * Case `⇓-app`. - Using `γ ⊢ L ⇓ clos N δ` and `γ ≃ σ`, + Using `γ ⊢ L ⇓ clos N δ` and `γ ≈ₑ σ`, the induction hypothesis gives us - ⧼ σ ⧽ L —↠ ƛ ⧼ exts τ ⧽ N (1) + ⟪ σ ⟫ L —↠ ƛ ⟪ exts τ ⟫ N (1) - and `δ ≃ τ` for some `τ`. - From `γ≃σ` we have `clos M γ ≈ ⧼ σ ⧽ M`. + and `δ ≈ₑ τ` for some `τ`. + From `γ≈ₑσ` we have `clos M γ ≈ ⟪ σ ⟫ M`. Then with `(δ ,' clos M γ) ⊢ N ⇓ c`, the induction hypothesis gives us `c ≈ N'` and - ⧼ exts τ ⨟ subst-zero (⧼ σ ⧽ M) ⧽ N —↠ N' (2) + ⟪ exts τ ⨟ subst-zero (⟪ σ ⟫ M) ⟫ N —↠ N' (2) Meanwhile, by `β`, we have - (ƛ ⧼ exts τ ⧽ N) · ⧼ σ ⧽ M —→ ⧼ subst-zero (⧼ σ ⧽ M) ⧽ (⧼ exts τ ⧽ N) + (ƛ ⟪ exts τ ⟫ N) · ⟪ σ ⟫ M —→ ⟪ subst-zero (⟪ σ ⟫ M) ⟫ (⟪ exts τ ⟫ N) which is the same as the following, by `sub-sub`. - (ƛ ⧼ exts τ ⧽ N) · ⧼ σ ⧽ M —→ ⧼ exts τ ⨟ subst-zero (⧼ σ ⧽ M) ⧽ N (3) + (ƛ ⟪ exts τ ⟫ N) · ⟪ σ ⟫ M —→ ⟪ exts τ ⨟ subst-zero (⟪ σ ⟫ M) ⟫ N (3) Using (3) and (2) we have - (ƛ ⧼ exts τ ⧽ N) · ⧼ σ ⧽ M —↠ N' (4) + (ƛ ⟪ exts τ ⟫ N) · ⟪ σ ⟫ M —↠ N' (4) From (1) we have - ⧼ σ ⧽ L · ⧼ σ ⧽ M —↠ (ƛ ⧼ exts τ ⧽ N) · ⧼ σ ⧽ M + ⟪ σ ⟫ L · ⟪ σ ⟫ M —↠ (ƛ ⟪ exts τ ⟫ N) · ⟪ σ ⟫ M which we combine with (4) to conclude that - ⧼ σ ⧽ L · ⧼ σ ⧽ M —↠ N' + ⟪ σ ⟫ L · ⟪ σ ⟫ M —↠ N' With the main lemma complete, we establish the forward direction @@ -326,10 +326,10 @@ cbn→reduce : ∀{M : ∅ ⊢ ★}{Δ}{δ : ClosEnv Δ}{N′ : Δ , ★ ⊢ ----------------------------- → Σ[ N ∈ ∅ , ★ ⊢ ★ ] (M —↠ ƛ N) cbn→reduce {M}{Δ}{δ}{N′} M⇓c - with ⇓→—↠×𝔹{σ = ids} M⇓c ≃-id + with ⇓→—↠×𝔹{σ = ids} M⇓c ≈ₑ-id ... | ⟨ N , ⟨ rs , ⟨ σ , ⟨ h , eq2 ⟩ ⟩ ⟩ ⟩ rewrite sub-id{M = M} | eq2 = - ⟨ ⧼ exts σ ⧽ N′ , rs ⟩ + ⟨ ⟪ exts σ ⟫ N′ , rs ⟩ \end{code} The proof of the backward direction, that beta reduction to a lambda @@ -359,5 +359,10 @@ reduction. Finally, Corollary 2 combines these results to show that ## Unicode +This chapter uses the following unicode: + + ≈ U+2248 ALMOST EQUAL TO (\~~ or \approx) + ₑ U+2091 LATIN SUBSCRIPT SMALL LETTER E (\_e) + ⊢ U+22A2 RIGHT TACK (\|- or \vdash) ⇓ U+21DB DOWNWARDS DOUBLE ARROW (\d= or \Downarrow) diff --git a/src/plfa/Confluence.lagda b/src/plfa/Confluence.lagda index 74049ac2..e9cc9d81 100644 --- a/src/plfa/Confluence.lagda +++ b/src/plfa/Confluence.lagda @@ -13,12 +13,10 @@ module plfa.Confluence where ## Imports \begin{code} -open import plfa.Substitution - using (subst-commute; rename-subst-commute) +open import plfa.Substitution using (subst-commute; rename-subst-commute) open import plfa.LambdaReduction using (_—→_; β; ξ₁; ξ₂; ζ; _—↠_; _—→⟨_⟩_; _[]; - abs-cong; appL-cong; appR-cong; - —↠-trans) + abs-cong; appL-cong; appR-cong; —↠-trans) open import plfa.Denotational using (Rename) open import plfa.Soundness using (Subst) open import plfa.Untyped diff --git a/src/plfa/Substitution.lagda b/src/plfa/Substitution.lagda index bd8ed008..e04e3bee 100644 --- a/src/plfa/Substitution.lagda +++ b/src/plfa/Substitution.lagda @@ -61,8 +61,8 @@ system that _decides_ whether any two substitutions are equal. We use the following more succinct notation the `subst` function. \begin{code} -⧼_⧽ : ∀{Γ Δ A} → Subst Γ Δ → Γ ⊢ A → Δ ⊢ A -⧼ σ ⧽ = λ M → subst σ M +⟪_⟫ : ∀{Γ Δ A} → Subst Γ Δ → Γ ⊢ A → Δ ⊢ A +⟪ σ ⟫ = λ M → subst σ M \end{code} @@ -109,7 +109,7 @@ _•_ : ∀{Γ Δ A} → (Δ ⊢ A) → Subst Γ Δ → Subst (Γ , A) Δ Given two substitutions `σ` and `τ`, the sequencing operation `σ ⨟ τ` produces the sequence - ⧼τ⧽(σ 0), ⧼τ⧽(σ 1), ⧼τ⧽(σ 2), ... + ⟪τ⟫(σ 0), ⟪τ⟫(σ 1), ⟪τ⟫(σ 2), ... That is, it composes the two substitutions by first applying `σ` and then applying `τ`. @@ -118,7 +118,7 @@ That is, it composes the two substitutions by first applying infixr 5 _⨟_ _⨟_ : ∀{Γ Δ Σ} → Subst Γ Δ → Subst Δ Σ → Subst Γ Σ -σ ⨟ τ = ⧼ τ ⧽ ∘ σ +σ ⨟ τ = ⟪ τ ⟫ ∘ σ \end{code} For the sequencing operation, Abadi et al. use the notation of @@ -131,20 +131,20 @@ the standard notation for forward function composition. The σ algebra includes the following equations. - (sub-head) ⧼ M • σ ⧽ (` Z) ≡ M + (sub-head) ⟪ M • σ ⟫ (` Z) ≡ M (sub-tail) ↑ ⨟ (M • σ) ≡ σ - (sub-η) (⧼ σ ⧽ (` Z)) • (↑ ⨟ σ) ≡ σ + (sub-η) (⟪ σ ⟫ (` Z)) • (↑ ⨟ σ) ≡ σ (Z-shift) (` Z) • ↑ ≡ ids - (sub-id) ⧼ ids ⧽ M ≡ M - (sub-app) ⧼ σ ⧽ (L · M) ≡ (⧼ σ ⧽ L) · (⧼ σ ⧽ M) - (sub-abs) ⧼ σ ⧽ (ƛ N) ≡ ƛ ⧼ σ ⧽ N - (sub-sub) ⧼ τ ⧽ ⧼ σ ⧽ M ≡ ⧼ σ ⨟ τ ⧽ M + (sub-id) ⟪ ids ⟫ M ≡ M + (sub-app) ⟪ σ ⟫ (L · M) ≡ (⟪ σ ⟫ L) · (⟪ σ ⟫ M) + (sub-abs) ⟪ σ ⟫ (ƛ N) ≡ ƛ ⟪ σ ⟫ N + (sub-sub) ⟪ τ ⟫ ⟪ σ ⟫ M ≡ ⟪ σ ⨟ τ ⟫ M (sub-idL) ids ⨟ σ ≡ σ (sub-idR) σ ⨟ ids ≡ σ (sub-assoc) (σ ⨟ τ) ⨟ θ ≡ σ ⨟ (τ ⨟ θ) - (sub-dist) (M • σ) ⨟ τ ≡ (⧼ τ ⧽ M) • (σ ⨟ τ) + (sub-dist) (M • σ) ⨟ τ ≡ (⟪ τ ⟫ M) • (σ ⨟ τ) The first group of equations describe how the `•` operator acts like cons. The equation `sub-head` says that the variable zero `Z` returns the @@ -179,7 +179,7 @@ the σ algebra. To begin with, renaming can be expressed in terms of substitution. We have - rename ρ M ≡ ⧼ ren ρ ⧽ M (rename-subst-ren) + rename ρ M ≡ ⟪ ren ρ ⟫ M (rename-subst-ren) where `ren` turns a renaming `ρ` into a substitution by post-composing `ρ` with the identity substitution. @@ -194,7 +194,7 @@ shift. ren S_ ≡ ↑ (ren-shift) - rename S_ M ≡ ⧼ ↑ ⧽ M (rename-shift) + rename S_ M ≡ ⟪ ↑ ⟫ M (rename-shift) Next we relate the `exts` function to the σ algebra. Recall that the `exts` function extends a substitution as follows: @@ -220,7 +220,7 @@ renamings. It is also useful to specialize the `sub-sub` equation of the σ algebra to the situation where the first substitution is a renaming. - ⧼ σ ⧽ (rename ρ M) ≡ ⧼ σ ∘ ρ ⧽ M (rename-subst) + ⟪ σ ⟫ (rename ρ M) ≡ ⟪ σ ∘ ρ ⟫ M (rename-subst) The `subst-zero M` substitution is equivalent to cons'ing `M` onto the identity substitution. @@ -241,7 +241,7 @@ the operators. \begin{code} sub-head : ∀ {Γ Δ} {A} {M : Δ ⊢ A}{σ : Subst Γ Δ} - → ⧼ M • σ ⧽ (` Z) ≡ M + → ⟪ M • σ ⟫ (` Z) ≡ M sub-head = refl \end{code} @@ -253,10 +253,10 @@ sub-tail = extensionality λ x → refl \begin{code} sub-η : ∀{Γ Δ} {A B} {σ : Subst (Γ , A) Δ} - → (⧼ σ ⧽ (` Z) • (↑ ⨟ σ)) {A = B} ≡ σ + → (⟪ σ ⟫ (` Z) • (↑ ⨟ σ)) {A = B} ≡ σ sub-η {Γ}{Δ}{A}{B}{σ} = extensionality λ x → lemma where - lemma : ∀ {x} → ((⧼ σ ⧽ (` Z)) • (↑ ⨟ σ)) x ≡ σ x + lemma : ∀ {x} → ((⟪ σ ⟫ (` Z)) • (↑ ⨟ σ)) x ≡ σ x lemma {x = Z} = refl lemma {x = S x} = refl \end{code} @@ -290,7 +290,7 @@ sub-dist {Γ}{Δ}{Σ}{A}{B}{σ}{τ}{M} = extensionality λ x → lemma {x = x} \begin{code} sub-app : ∀{Γ Δ} {σ : Subst Γ Δ} {L : Γ ⊢ ★}{M : Γ ⊢ ★} - → ⧼ σ ⧽ (L · M) ≡ (⧼ σ ⧽ L) · (⧼ σ ⧽ M) + → ⟪ σ ⟫ (L · M) ≡ (⟪ σ ⟫ L) · (⟪ σ ⟫ M) sub-app = refl \end{code} @@ -405,7 +405,7 @@ in the σ algebra. The first equation we prove is - rename ρ M ≡ ⧼ ren ρ ⧽ M (rename-subst-ren) + rename ρ M ≡ ⟪ ren ρ ⟫ M (rename-subst-ren) Because `subst` uses the `exts` function, we need the following lemma which says that `exts` and `ext` do the same thing except that `ext` @@ -426,7 +426,7 @@ the term `M`. \begin{code} rename-subst-ren : ∀ {Γ Δ}{A} {ρ : Rename Γ Δ}{M : Γ ⊢ A} - → rename ρ M ≡ ⧼ ren ρ ⧽ M + → rename ρ M ≡ ⟪ ren ρ ⟫ M rename-subst-ren {M = ` x} = refl rename-subst-ren {ρ = ρ}{M = ƛ N} = begin @@ -434,11 +434,11 @@ rename-subst-ren {ρ = ρ}{M = ƛ N} = ≡⟨⟩ ƛ rename (ext ρ) N ≡⟨ cong ƛ_ (rename-subst-ren {ρ = ext ρ}{M = N}) ⟩ - ƛ ⧼ ren (ext ρ) ⧽ N + ƛ ⟪ ren (ext ρ) ⟫ N ≡⟨ cong ƛ_ (cong-sub {M = N} ren-ext refl) ⟩ - ƛ ⧼ exts (ren ρ) ⧽ N + ƛ ⟪ exts (ren ρ) ⟫ N ≡⟨⟩ - ⧼ ren ρ ⧽ (ƛ N) + ⟪ ren ρ ⟫ (ƛ N) ∎ rename-subst-ren {M = L · M} = cong₂ _·_ rename-subst-ren rename-subst-ren \end{code} @@ -455,18 +455,18 @@ ren-shift {Γ}{A}{B} = extensionality λ x → lemma {x = x} lemma {x = S x} = refl \end{code} -The substitution `rename S_ M` is equivalent to shifting: `⧼ ↑ ⧽ M`. +The substitution `rename S_ M` is equivalent to shifting: `⟪ ↑ ⟫ M`. \begin{code} rename-shift : ∀{Γ} {A} {B} {M : Γ ⊢ A} - → rename (S_{B = B}) M ≡ ⧼ ↑ ⧽ M + → rename (S_{B = B}) M ≡ ⟪ ↑ ⟫ M rename-shift{Γ}{A}{B}{M} = begin rename S_ M ≡⟨ rename-subst-ren ⟩ - ⧼ ren S_ ⧽ M + ⟪ ren S_ ⟫ M ≡⟨ cong-sub{M = M} ren-shift refl ⟩ - ⧼ ↑ ⧽ M + ⟪ ↑ ⟫ M ∎ \end{code} @@ -523,14 +523,14 @@ The equation `sub-abs` follows immediately from the equation \begin{code} sub-abs : ∀{Γ Δ} {σ : Subst Γ Δ} {N : Γ , ★ ⊢ ★} - → ⧼ σ ⧽ (ƛ N) ≡ ƛ ⧼ (` Z) • (σ ⨟ ↑) ⧽ N + → ⟪ σ ⟫ (ƛ N) ≡ ƛ ⟪ (` Z) • (σ ⨟ ↑) ⟫ N sub-abs {σ = σ}{N = N} = begin - ⧼ σ ⧽ (ƛ N) + ⟪ σ ⟫ (ƛ N) ≡⟨⟩ - ƛ ⧼ exts σ ⧽ N + ƛ ⟪ exts σ ⟫ N ≡⟨ cong ƛ_ (cong-sub{M = N} exts-cons-shift refl) ⟩ - ƛ ⧼ (` Z) • (σ ⨟ ↑) ⧽ N + ƛ ⟪ (` Z) • (σ ⨟ ↑) ⟫ N ∎ \end{code} @@ -547,20 +547,20 @@ exts-ids {Γ}{A}{B} = extensionality lemma lemma (S x) = refl \end{code} -The proof of `⧼ ids ⧽ M ≡ M` now follows easily by induction on `M`, +The proof of `⟪ ids ⟫ M ≡ M` now follows easily by induction on `M`, using `exts-ids` in the case for `M ≡ ƛ N`. \begin{code} sub-id : ∀{Γ} {A} {M : Γ ⊢ A} - → ⧼ ids ⧽ M ≡ M + → ⟪ ids ⟫ M ≡ M sub-id {M = ` x} = refl sub-id {M = ƛ N} = begin - ⧼ ids ⧽ (ƛ N) + ⟪ ids ⟫ (ƛ N) ≡⟨⟩ - ƛ ⧼ exts ids ⧽ N + ƛ ⟪ exts ids ⟫ N ≡⟨ cong ƛ_ (cong-sub{M = N} exts-ids refl) ⟩ - ƛ ⧼ ids ⧽ N + ƛ ⟪ ids ⟫ N ≡⟨ cong ƛ_ sub-id ⟩ ƛ N ∎ @@ -591,7 +591,7 @@ sub-idR {Γ}{σ = σ}{A} = The `sub-sub` equation states that sequenced substitutions `σ ⨟ τ` are equivalent to first applying `σ` then applying `τ`. - ⧼ τ ⧽ ⧼ σ ⧽ M ≡ ⧼ σ ⨟ τ ⧽ M + ⟪ τ ⟫ ⟪ σ ⟫ M ≡ ⟪ σ ⨟ τ ⟫ M The proof requires several lemmas. First, we need to prove the specialization for renaming. @@ -718,9 +718,9 @@ exts-seq = extensionality λ x → lemma {x = x} begin (exts σ₁ ⨟ exts σ₂) (S x) ≡⟨⟩ - ⧼ exts σ₂ ⧽ (rename S_ (σ₁ x)) + ⟪ exts σ₂ ⟫ (rename S_ (σ₁ x)) ≡⟨ commute-subst-rename{M = σ₁ x}{σ = σ₂}{ρ = S_} refl ⟩ - rename S_ (⧼ σ₂ ⧽ (σ₁ x)) + rename S_ (⟪ σ₂ ⟫ (σ₁ x)) ≡⟨⟩ rename S_ ((σ₁ ⨟ σ₂) x) ∎ @@ -740,17 +740,17 @@ Now we come to the proof of `sub-sub`, which we explain below. \begin{code} sub-sub : ∀{Γ Δ Σ}{A}{M : Γ ⊢ A} {σ₁ : Subst Γ Δ}{σ₂ : Subst Δ Σ} - → ⧼ σ₂ ⧽ (⧼ σ₁ ⧽ M) ≡ ⧼ σ₁ ⨟ σ₂ ⧽ M + → ⟪ σ₂ ⟫ (⟪ σ₁ ⟫ M) ≡ ⟪ σ₁ ⨟ σ₂ ⟫ M sub-sub {M = ` x} = refl sub-sub {Γ}{Δ}{Σ}{A}{ƛ N}{σ₁}{σ₂} = begin - ⧼ σ₂ ⧽ (⧼ σ₁ ⧽ (ƛ N)) + ⟪ σ₂ ⟫ (⟪ σ₁ ⟫ (ƛ N)) ≡⟨⟩ - ƛ ⧼ exts σ₂ ⧽ (⧼ exts σ₁ ⧽ N) + ƛ ⟪ exts σ₂ ⟫ (⟪ exts σ₁ ⟫ N) ≡⟨ cong ƛ_ (sub-sub{M = N}{σ₁ = exts σ₁}{σ₂ = exts σ₂}) ⟩ - ƛ ⧼ exts σ₁ ⨟ exts σ₂ ⧽ N + ƛ ⟪ exts σ₁ ⨟ exts σ₂ ⟫ N ≡⟨ cong ƛ_ (cong-sub{M = N} (λ {A} → exts-seq) refl) ⟩ - ƛ ⧼ exts ( σ₁ ⨟ σ₂) ⧽ N + ƛ ⟪ exts ( σ₁ ⨟ σ₂) ⟫ N ∎ sub-sub {M = L · M} = cong₂ _·_ (sub-sub{M = L}) (sub-sub{M = M}) \end{code} @@ -761,11 +761,11 @@ We proceed by induction on the term `M`. * If `M = ƛ N`, we first use the induction hypothesis to show that - ƛ ⧼ exts σ₂ ⧽ (⧼ exts σ₁ ⧽ N) ≡ ƛ ⧼ exts σ₁ ⨟ exts σ₂ ⧽ N + ƛ ⟪ exts σ₂ ⟫ (⟪ exts σ₁ ⟫ N) ≡ ƛ ⟪ exts σ₁ ⨟ exts σ₂ ⟫ N and then use the lemma `exts-seq` to show - ƛ ⧼ exts σ₁ ⨟ exts σ₂ ⧽ N ≡ ƛ ⧼ exts ( σ₁ ⨟ σ₂) ⧽ N + ƛ ⟪ exts σ₁ ⨟ exts σ₂ ⟫ N ≡ ƛ ⟪ exts ( σ₁ ⨟ σ₂) ⟫ N * If `M` is an application, we use the induction hypothesis for both subterms. @@ -776,16 +776,16 @@ substitution to a renaming. \begin{code} rename-subst : ∀{Γ Δ Δ′}{M : Γ ⊢ ★}{ρ : Rename Γ Δ}{σ : Subst Δ Δ′} - → ⧼ σ ⧽ (rename ρ M) ≡ ⧼ σ ∘ ρ ⧽ M + → ⟪ σ ⟫ (rename ρ M) ≡ ⟪ σ ∘ ρ ⟫ M rename-subst {Γ}{Δ}{Δ′}{M}{ρ}{σ} = begin - ⧼ σ ⧽ (rename ρ M) - ≡⟨ cong ⧼ σ ⧽ (rename-subst-ren{M = M}) ⟩ - ⧼ σ ⧽ (⧼ ren ρ ⧽ M) + ⟪ σ ⟫ (rename ρ M) + ≡⟨ cong ⟪ σ ⟫ (rename-subst-ren{M = M}) ⟩ + ⟪ σ ⟫ (⟪ ren ρ ⟫ M) ≡⟨ sub-sub{M = M} ⟩ - ⧼ ren ρ ⨟ σ ⧽ M + ⟪ ren ρ ⨟ σ ⟫ M ≡⟨⟩ - ⧼ σ ∘ ρ ⧽ M + ⟪ σ ∘ ρ ⟫ M ∎ \end{code} @@ -806,9 +806,9 @@ sub-assoc {Γ}{Δ}{Σ}{Ψ}{σ}{τ}{θ}{A} = extensionality λ x → lemma{x = x} begin ((σ ⨟ τ) ⨟ θ) x ≡⟨⟩ - ⧼ θ ⧽ (⧼ τ ⧽ (σ x)) + ⟪ θ ⟫ (⟪ τ ⟫ (σ x)) ≡⟨ sub-sub{M = σ x} ⟩ - ⧼ τ ⨟ θ ⧽ (σ x) + ⟪ τ ⨟ θ ⟫ (σ x) ≡⟨⟩ (σ ⨟ τ ⨟ θ) x ∎ @@ -830,7 +830,7 @@ subst-zero-exts-cons {Γ}{Δ}{σ}{B}{M}{A} = ≡⟨ cong-seq exts-cons-shift subst-Z-cons-ids ⟩ (` Z • (σ ⨟ ↑)) ⨟ (M • ids) ≡⟨ sub-dist ⟩ - (⧼ M • ids ⧽ (` Z)) • ((σ ⨟ ↑) ⨟ (M • ids)) + (⟪ M • ids ⟫ (` Z)) • ((σ ⨟ ↑) ⨟ (M • ids)) ≡⟨ cong-cons (sub-head{σ = ids}) refl ⟩ M • ((σ ⨟ ↑) ⨟ (M • ids)) ≡⟨ cong-cons refl (sub-assoc{σ = σ}) ⟩ @@ -849,56 +849,56 @@ We first prove the generalized form of the substitution lemma, showing that a substitution `σ` commutes with the subusitution of `M` into `N`. - ⧼ exts σ ⧽ N [ ⧼ σ ⧽ M ] ≡ ⧼ σ ⧽ (N [ M ]) + ⟪ exts σ ⟫ N [ ⟪ σ ⟫ M ] ≡ ⟪ σ ⟫ (N [ M ]) This proof is where the σ algebra pays off. The proof is by direct equational reasoning. Starting with the left-hand side, we apply σ algebra equations, oriented left-to-right, until we arive at the normal form - ⧼ ⧼ σ ⧽ M • σ ⧽ N + ⟪ ⟪ σ ⟫ M • σ ⟫ N We then do the same with the right-hand side, arriving at the same normal form. \begin{code} subst-commute : ∀{Γ Δ}{N : Γ , ★ ⊢ ★}{M : Γ ⊢ ★}{σ : Subst Γ Δ } - → ⧼ exts σ ⧽ N [ ⧼ σ ⧽ M ] ≡ ⧼ σ ⧽ (N [ M ]) + → ⟪ exts σ ⟫ N [ ⟪ σ ⟫ M ] ≡ ⟪ σ ⟫ (N [ M ]) subst-commute {Γ}{Δ}{N}{M}{σ} = begin - ⧼ exts σ ⧽ N [ ⧼ σ ⧽ M ] + ⟪ exts σ ⟫ N [ ⟪ σ ⟫ M ] ≡⟨⟩ - ⧼ subst-zero (⧼ σ ⧽ M) ⧽ (⧼ exts σ ⧽ N) - ≡⟨ cong-sub {M = ⧼ exts σ ⧽ N} subst-Z-cons-ids refl ⟩ - ⧼ ⧼ σ ⧽ M • ids ⧽ (⧼ exts σ ⧽ N) + ⟪ subst-zero (⟪ σ ⟫ M) ⟫ (⟪ exts σ ⟫ N) + ≡⟨ cong-sub {M = ⟪ exts σ ⟫ N} subst-Z-cons-ids refl ⟩ + ⟪ ⟪ σ ⟫ M • ids ⟫ (⟪ exts σ ⟫ N) ≡⟨ sub-sub {M = N} ⟩ - ⧼ (exts σ) ⨟ ((⧼ σ ⧽ M) • ids) ⧽ N + ⟪ (exts σ) ⨟ ((⟪ σ ⟫ M) • ids) ⟫ N ≡⟨ cong-sub {M = N} (cong-seq exts-cons-shift refl) refl ⟩ - ⧼ (` Z • (σ ⨟ ↑)) ⨟ (⧼ σ ⧽ M • ids) ⧽ N + ⟪ (` Z • (σ ⨟ ↑)) ⨟ (⟪ σ ⟫ M • ids) ⟫ N ≡⟨ cong-sub {M = N} (sub-dist {M = ` Z}) refl ⟩ - ⧼ ⧼ ⧼ σ ⧽ M • ids ⧽ (` Z) • ((σ ⨟ ↑) ⨟ (⧼ σ ⧽ M • ids)) ⧽ N + ⟪ ⟪ ⟪ σ ⟫ M • ids ⟫ (` Z) • ((σ ⨟ ↑) ⨟ (⟪ σ ⟫ M • ids)) ⟫ N ≡⟨⟩ - ⧼ ⧼ σ ⧽ M • ((σ ⨟ ↑) ⨟ (⧼ σ ⧽ M • ids)) ⧽ N + ⟪ ⟪ σ ⟫ M • ((σ ⨟ ↑) ⨟ (⟪ σ ⟫ M • ids)) ⟫ N ≡⟨ cong-sub{M = N} (cong-cons refl (sub-assoc{σ = σ})) refl ⟩ - ⧼ ⧼ σ ⧽ M • (σ ⨟ ↑ ⨟ ⧼ σ ⧽ M • ids) ⧽ N + ⟪ ⟪ σ ⟫ M • (σ ⨟ ↑ ⨟ ⟪ σ ⟫ M • ids) ⟫ N ≡⟨ cong-sub{M = N} refl refl ⟩ - ⧼ ⧼ σ ⧽ M • (σ ⨟ ids) ⧽ N + ⟪ ⟪ σ ⟫ M • (σ ⨟ ids) ⟫ N ≡⟨ cong-sub{M = N} (cong-cons refl (sub-idR{σ = σ})) refl ⟩ - ⧼ ⧼ σ ⧽ M • σ ⧽ N + ⟪ ⟪ σ ⟫ M • σ ⟫ N ≡⟨ cong-sub{M = N} (cong-cons refl (sub-idL{σ = σ})) refl ⟩ - ⧼ ⧼ σ ⧽ M • (ids ⨟ σ) ⧽ N + ⟪ ⟪ σ ⟫ M • (ids ⨟ σ) ⟫ N ≡⟨ cong-sub{M = N} (sym sub-dist) refl ⟩ - ⧼ M • ids ⨟ σ ⧽ N + ⟪ M • ids ⨟ σ ⟫ N ≡⟨ sym (sub-sub{M = N}) ⟩ - ⧼ σ ⧽ (⧼ M • ids ⧽ N) - ≡⟨ cong ⧼ σ ⧽ (sym (cong-sub{M = N} subst-Z-cons-ids refl)) ⟩ - ⧼ σ ⧽ (N [ M ]) + ⟪ σ ⟫ (⟪ M • ids ⟫ N) + ≡⟨ cong ⟪ σ ⟫ (sym (cong-sub{M = N} subst-Z-cons-ids refl)) ⟩ + ⟪ σ ⟫ (N [ M ]) ∎ \end{code} A corollary of `subst-commute` is that `rename` also commutes with substitution. In the proof below, we first exchange `rename ρ` for -the substitution `⧼ ren ρ ⧽`, and apply `subst-commute`, and +the substitution `⟪ ren ρ ⟫`, and apply `subst-commute`, and then convert back to `rename ρ`. \begin{code} @@ -909,9 +909,9 @@ rename-subst-commute {Γ}{Δ}{N}{M}{ρ} = (rename (ext ρ) N) [ rename ρ M ] ≡⟨ cong-sub (cong-sub-zero (rename-subst-ren{M = M})) (rename-subst-ren{M = N}) ⟩ - (⧼ ren (ext ρ) ⧽ N) [ ⧼ ren ρ ⧽ M ] + (⟪ ren (ext ρ) ⟫ N) [ ⟪ ren ρ ⟫ M ] ≡⟨ cong-sub refl (cong-sub{M = N} ren-ext refl) ⟩ - (⧼ exts (ren ρ) ⧽ N) [ ⧼ ren ρ ⧽ M ] + (⟪ exts (ren ρ) ⟫ N) [ ⟪ ren ρ ⟫ M ] ≡⟨ subst-commute{N = N} ⟩ subst (ren ρ) (N [ M ]) ≡⟨ sym (rename-subst-ren) ⟩ @@ -955,9 +955,8 @@ defines the σ algebra. ## Unicode This chapter uses the following unicode: - - ⧼ U+29FC LEFT-POINTING CURVED ANGLE BRACKET (C-x 8 RET LEFT-POINTING CURVED ANGLE BRACKET) - ⧽ U+29FD RIGHT-POINTING CURVED ANGLE BRACKET (C-x 8 RET RIGHT-POINTING CURVED ANGLE BRACKET) + ⟪ U+27EA MATHEMATICAL LEFT DOUBLE ANGLE BRACKET (\<<) + ⟫ U+27EA MATHEMATICAL RIGHT DOUBLE ANGLE BRACKET (\>>) ↑ U+2191 UPWARDS ARROW (\u) • U+2022 BULLET (\bub) ⨟ U+2A1F Z NOTATION SCHEMA COMPOSITION (C-x 8 RET Z NOTATION SCHEMA COMPOSITION)