From 57ca84d211edfd52a44ad3a0fa2ecdd551dece0e Mon Sep 17 00:00:00 2001 From: Jeremy Siek Date: Sun, 19 May 2019 15:19:33 -0400 Subject: [PATCH] more apostrophes and unicode --- src/plfa/Adequacy.lagda | 9 ++ src/plfa/Compositional.lagda | 150 ++++++++++++++------------- src/plfa/ContextualEquivalence.lagda | 7 ++ src/plfa/Soundness.lagda | 102 +++++++++--------- 4 files changed, 149 insertions(+), 119 deletions(-) diff --git a/src/plfa/Adequacy.lagda b/src/plfa/Adequacy.lagda index fb28a2ca..b47f2214 100644 --- a/src/plfa/Adequacy.lagda +++ b/src/plfa/Adequacy.lagda @@ -635,3 +635,12 @@ cbn↔reduce {M} = ⟨ (λ x → reduce→cbn (proj₂ x)) , (λ x → cbn→reduce (proj₂ (proj₂ (proj₂ x)))) ⟩ \end{code} + +## Unicode + +This chapter uses the following unicode: + + 𝔼 U+1D53C MATHEMATICAL DOUBLE-STRUCK CAPITAL E (\bE) + 𝔾 U+1D53E MATHEMATICAL DOUBLE-STRUCK CAPITAL G (\bG) + 𝕍 U+1D53E MATHEMATICAL DOUBLE-STRUCK CAPITAL V (\bV) + diff --git a/src/plfa/Compositional.lagda b/src/plfa/Compositional.lagda index 3e90a435..5cc31cf9 100644 --- a/src/plfa/Compositional.lagda +++ b/src/plfa/Compositional.lagda @@ -63,7 +63,7 @@ sub-ℱ : ∀{Γ}{N : Γ , ★ ⊢ ★}{γ v u} ------------ → ℱ (ℰ N) γ u sub-ℱ d Bot⊑ = tt -sub-ℱ d (Fun⊑ lt lt') = sub (up-env d lt) lt' +sub-ℱ d (Fun⊑ lt lt′) = sub (up-env d lt) lt′ sub-ℱ d (ConjL⊑ lt lt₁) = ⟨ sub-ℱ d lt , sub-ℱ d lt₁ ⟩ sub-ℱ d (ConjR1⊑ lt) = sub-ℱ (proj₁ d) lt sub-ℱ d (ConjR2⊑ lt) = sub-ℱ (proj₂ d) lt @@ -159,23 +159,23 @@ describe the proof below. → ℰ (L · M) γ v ---------------- → (ℰ L ● ℰ M) γ v -ℰ·→●ℰ (↦-elim{v = v'} d₁ d₂) = inj₂ ⟨ v' , ⟨ d₁ , d₂ ⟩ ⟩ +ℰ·→●ℰ (↦-elim{v = v′} d₁ d₂) = inj₂ ⟨ v′ , ⟨ d₁ , d₂ ⟩ ⟩ ℰ·→●ℰ {v = ⊥} ⊥-intro = inj₁ Bot⊑ ℰ·→●ℰ {Γ}{γ}{L}{M}{v} (⊔-intro{v = v₁}{w = v₂} d₁ d₂) with ℰ·→●ℰ d₁ | ℰ·→●ℰ d₂ ... | inj₁ lt1 | inj₁ lt2 = inj₁ (ConjL⊑ lt1 lt2) -... | inj₁ lt1 | inj₂ ⟨ v₁' , ⟨ L↓v12 , M↓v3 ⟩ ⟩ = - inj₂ ⟨ v₁' , ⟨ sub L↓v12 lt , M↓v3 ⟩ ⟩ - where lt : v₁' ↦ (v₁ ⊔ v₂) ⊑ v₁' ↦ v₂ +... | inj₁ lt1 | inj₂ ⟨ v₁′ , ⟨ L↓v12 , M↓v3 ⟩ ⟩ = + inj₂ ⟨ v₁′ , ⟨ sub L↓v12 lt , M↓v3 ⟩ ⟩ + where lt : v₁′ ↦ (v₁ ⊔ v₂) ⊑ v₁′ ↦ v₂ lt = (Fun⊑ Refl⊑ (ConjL⊑ (Trans⊑ lt1 Bot⊑) Refl⊑)) -... | inj₂ ⟨ v₁' , ⟨ L↓v12 , M↓v3 ⟩ ⟩ | inj₁ lt2 = - inj₂ ⟨ v₁' , ⟨ sub L↓v12 lt , M↓v3 ⟩ ⟩ - where lt : v₁' ↦ (v₁ ⊔ v₂) ⊑ v₁' ↦ v₁ +... | inj₂ ⟨ v₁′ , ⟨ L↓v12 , M↓v3 ⟩ ⟩ | inj₁ lt2 = + inj₂ ⟨ v₁′ , ⟨ sub L↓v12 lt , M↓v3 ⟩ ⟩ + where lt : v₁′ ↦ (v₁ ⊔ v₂) ⊑ v₁′ ↦ v₁ lt = (Fun⊑ Refl⊑ (ConjL⊑ Refl⊑ (Trans⊑ lt2 Bot⊑))) -... | inj₂ ⟨ v₁' , ⟨ L↓v12 , M↓v3 ⟩ ⟩ | inj₂ ⟨ v₁'' , ⟨ L↓v12' , M↓v3' ⟩ ⟩ = - let L↓⊔ = ⊔-intro L↓v12 L↓v12' in - let M↓⊔ = ⊔-intro M↓v3 M↓v3' in - let x = inj₂ ⟨ v₁' ⊔ v₁'' , ⟨ sub L↓⊔ Dist⊔↦⊔ , M↓⊔ ⟩ ⟩ in +... | inj₂ ⟨ v₁′ , ⟨ L↓v12 , M↓v3 ⟩ ⟩ | inj₂ ⟨ v₁′′ , ⟨ L↓v12′ , M↓v3′ ⟩ ⟩ = + let L↓⊔ = ⊔-intro L↓v12 L↓v12′ in + let M↓⊔ = ⊔-intro M↓v3 M↓v3′ in + let x = inj₂ ⟨ v₁′ ⊔ v₁′′ , ⟨ sub L↓⊔ Dist⊔↦⊔ , M↓⊔ ⟩ ⟩ in x ℰ·→●ℰ {Γ}{γ}{L}{M}{v} (sub d lt) with ℰ·→●ℰ d @@ -186,7 +186,7 @@ describe the proof below. We proceed by induction on the semantics. -* In case `↦-elim` we have `γ ⊢ L ↓ (v' ↦ v)` and `γ ⊢ M ↓ v'`, +* In case `↦-elim` we have `γ ⊢ L ↓ (v′ ↦ v)` and `γ ⊢ M ↓ v′`, which is all we need to show `(ℰ L ● ℰ M) γ v`. * In case `⊥-intro` we have `v = ⊥`. We conclude that `v ⊑ ⊥`. @@ -197,26 +197,26 @@ We proceed by induction on the semantics. We have four subcases to consider. * Suppose `v₁ ⊑ ⊥` and `v₂ ⊑ ⊥`. Then `v₁ ⊔ v₂ ⊑ ⊥`. - * Suppose `v₁ ⊑ ⊥`, `γ ⊢ L ↓ v₁' ↦ v₂`, and `γ ⊢ M ↓ v₁'`. - We have `γ ⊢ L ↓ v₁' ↦ (v₁ ⊔ v₂)` by rule `sub` - because `v₁' ↦ (v₁ ⊔ v₂) ⊑ v₁' ↦ v₂`. - * Suppose `γ ⊢ L ↓ v₁' ↦ v₁`, `γ ⊢ M ↓ v₁'`, and `v₂ ⊑ ⊥`. - We have `γ ⊢ L ↓ v₁' ↦ (v₁ ⊔ v₂)` by rule `sub` - because `v₁' ↦ (v₁ ⊔ v₂) ⊑ v₁' ↦ v₁`. - * Suppose `γ ⊢ L ↓ v₁'' ↦ v₁, γ ⊢ M ↓ v₁''`, - `γ ⊢ L ↓ v₁' ↦ v₂`, and `γ ⊢ M ↓ v₁'`. + * Suppose `v₁ ⊑ ⊥`, `γ ⊢ L ↓ v₁′ ↦ v₂`, and `γ ⊢ M ↓ v₁′`. + We have `γ ⊢ L ↓ v₁′ ↦ (v₁ ⊔ v₂)` by rule `sub` + because `v₁′ ↦ (v₁ ⊔ v₂) ⊑ v₁′ ↦ v₂`. + * Suppose `γ ⊢ L ↓ v₁′ ↦ v₁`, `γ ⊢ M ↓ v₁′`, and `v₂ ⊑ ⊥`. + We have `γ ⊢ L ↓ v₁′ ↦ (v₁ ⊔ v₂)` by rule `sub` + because `v₁′ ↦ (v₁ ⊔ v₂) ⊑ v₁′ ↦ v₁`. + * Suppose `γ ⊢ L ↓ v₁′′ ↦ v₁, γ ⊢ M ↓ v₁′′`, + `γ ⊢ L ↓ v₁′ ↦ v₂`, and `γ ⊢ M ↓ v₁′`. This case is the most interesting. By two uses of the rule `⊔-intro` we have - `γ ⊢ L ↓ (v₁' ↦ v₂) ⊔ (v₁'' ↦ v₁)` and - `γ ⊢ M ↓ (v₁' ⊔ v₁'')`. But this does not yet match + `γ ⊢ L ↓ (v₁′ ↦ v₂) ⊔ (v₁′′ ↦ v₁)` and + `γ ⊢ M ↓ (v₁′ ⊔ v₁′′)`. But this does not yet match what we need for `ℰ L ● ℰ M` because the result of - `L` must be an `↦` whose input entry is `v₁' ⊔ v₁''`. + `L` must be an `↦` whose input entry is `v₁′ ⊔ v₁′′`. So we use the `sub` rule to obtain - `γ ⊢ L ↓ (v₁' ⊔ v₁'') ↦ (v₁ ⊔ v₂)`, + `γ ⊢ L ↓ (v₁′ ⊔ v₁′′) ↦ (v₁ ⊔ v₂)`, using the `Dist⊔→⊔` lemma (thanks to the `Dist⊑` rule) to show that - (v₁' ⊔ v₁'') ↦ (v₁ ⊔ v₂) ⊑ (v₁' ↦ v₂) ⊔ (v₁'' ↦ v₁) + (v₁′ ⊔ v₁′′) ↦ (v₁ ⊔ v₂) ⊑ (v₁′ ↦ v₂) ⊔ (v₁′′ ↦ v₁) So we have proved what is needed for this case. @@ -225,9 +225,9 @@ We proceed by induction on the semantics. We have two subcases to consider. * Suppose `v₁ ⊑ ⊥`. We conclude that `v ⊑ ⊥`. - * Suppose `Γ ⊢ L ↓ v' → v₁` and `Γ ⊢ M ↓ v'`. - We conclude with `Γ ⊢ L ↓ v' → v` by rule `sub`, because - `v' → v ⊑ v' → v₁`. + * Suppose `Γ ⊢ L ↓ v′ → v₁` and `Γ ⊢ M ↓ v′`. + We conclude with `Γ ⊢ L ↓ v′ → v` by rule `sub`, because + `v′ → v ⊑ v′ → v₁`. The forward direction is proved by cases on the premise `(ℰ L ● ℰ M) γ v`. @@ -288,23 +288,23 @@ that surrounding two denotationally-equal terms in the same context produces two programs that are denotationally equal. We begin by showing that denotational equality is a congruence with -respect to lambda abstraction: that `ℰ N ≃ ℰ N'` implies `ℰ (ƛ N) ≃ ℰ -(ƛ N')`. We shall use the `lam-equiv` equation to reduce this question to +respect to lambda abstraction: that `ℰ N ≃ ℰ N′` implies `ℰ (ƛ N) ≃ ℰ +(ƛ N′)`. We shall use the `lam-equiv` equation to reduce this question to whether `ℱ` is a congruence. \begin{code} -ℱ-cong : ∀{Γ}{D D' : Denotation (Γ , ★)} - → D ≃ D' +ℱ-cong : ∀{Γ}{D D′ : Denotation (Γ , ★)} + → D ≃ D′ ----------- - → ℱ D ≃ ℱ D' -ℱ-cong{Γ} D≃D' γ v = - ⟨ (λ x → ℱ≃{γ}{v} x D≃D') , (λ x → ℱ≃{γ}{v} x (≃-sym D≃D')) ⟩ + → ℱ D ≃ ℱ D′ +ℱ-cong{Γ} D≃D′ γ v = + ⟨ (λ x → ℱ≃{γ}{v} x D≃D′) , (λ x → ℱ≃{γ}{v} x (≃-sym D≃D′)) ⟩ where - ℱ≃ : ∀{γ : Env Γ}{v}{D D' : Denotation (Γ , ★)} - → ℱ D γ v → D ≃ D' → ℱ D' γ v - ℱ≃ {v = ⊥} fd dd' = tt - ℱ≃ {γ}{v ↦ w} fd dd' = proj₁ (dd' (γ `, v) w) fd - ℱ≃ {γ}{u ⊔ w} fd dd' = ⟨ ℱ≃{γ}{u} (proj₁ fd) dd' , ℱ≃{γ}{w} (proj₂ fd) dd' ⟩ + ℱ≃ : ∀{γ : Env Γ}{v}{D D′ : Denotation (Γ , ★)} + → ℱ D γ v → D ≃ D′ → ℱ D′ γ v + ℱ≃ {v = ⊥} fd dd′ = tt + ℱ≃ {γ}{v ↦ w} fd dd′ = proj₁ (dd′ (γ `, v) w) fd + ℱ≃ {γ}{u ⊔ w} fd dd′ = ⟨ ℱ≃{γ}{u} (proj₁ fd) dd′ , ℱ≃{γ}{w} (proj₂ fd) dd′ ⟩ \end{code} The proof of `ℱ-cong` uses the lemma `ℱ≃` to handle both directions of @@ -315,38 +315,38 @@ We now prove that lambda abstraction is a congruence by direct equational reasoning. \begin{code} -lam-cong : ∀{Γ}{N N' : Γ , ★ ⊢ ★} - → ℰ N ≃ ℰ N' +lam-cong : ∀{Γ}{N N′ : Γ , ★ ⊢ ★} + → ℰ N ≃ ℰ N′ ----------------- - → ℰ (ƛ N) ≃ ℰ (ƛ N') -lam-cong {Γ}{N}{N'} N≃N' = + → ℰ (ƛ N) ≃ ℰ (ƛ N′) +lam-cong {Γ}{N}{N′} N≃N′ = start ℰ (ƛ N) ≃⟨ lam-equiv ⟩ ℱ (ℰ N) - ≃⟨ ℱ-cong N≃N' ⟩ - ℱ (ℰ N') + ≃⟨ ℱ-cong N≃N′ ⟩ + ℱ (ℰ N′) ≃⟨ ≃-sym lam-equiv ⟩ - ℰ (ƛ N') + ℰ (ƛ N′) ☐ \end{code} Next we prove that denotational equality is a congruence for -application: that `ℰ L ≃ ℰ L'` and `ℰ M ≃ ℰ M'` imply -`ℰ (L · M) ≃ ℰ (L' · M')`. The `app-equiv` equation +application: that `ℰ L ≃ ℰ L′` and `ℰ M ≃ ℰ M′` imply +`ℰ (L · M) ≃ ℰ (L′ · M′)`. The `app-equiv` equation reduces this to the question of whether the `●` operator is a congruence. \begin{code} -●-cong : ∀{Γ}{D₁ D₁' D₂ D₂' : Denotation Γ} - → D₁ ≃ D₁' → D₂ ≃ D₂' - → (D₁ ● D₂) ≃ (D₁' ● D₂') +●-cong : ∀{Γ}{D₁ D₁′ D₂ D₂′ : Denotation Γ} + → D₁ ≃ D₁′ → D₂ ≃ D₂′ + → (D₁ ● D₂) ≃ (D₁′ ● D₂′) ●-cong {Γ} d1 d2 γ v = ⟨ (λ x → ●≃ x d1 d2) , (λ x → ●≃ x (≃-sym d1) (≃-sym d2)) ⟩ where - ●≃ : ∀{γ : Env Γ}{v}{D₁ D₁' D₂ D₂' : Denotation Γ} - → (D₁ ● D₂) γ v → D₁ ≃ D₁' → D₂ ≃ D₂' - → (D₁' ● D₂') γ v + ●≃ : ∀{γ : Env Γ}{v}{D₁ D₁′ D₂ D₂′ : Denotation Γ} + → (D₁ ● D₂) γ v → D₁ ≃ D₁′ → D₂ ≃ D₂′ + → (D₁′ ● D₂′) γ v ●≃ (inj₁ v⊑⊥) eq₁ eq₂ = inj₁ v⊑⊥ ●≃ {γ} {w} (inj₂ ⟨ v , ⟨ Dv↦w , Dv ⟩ ⟩) eq₁ eq₂ = inj₂ ⟨ v , ⟨ proj₁ (eq₁ γ (v ↦ w)) Dv↦w , proj₁ (eq₂ γ v) Dv ⟩ ⟩ @@ -359,20 +359,20 @@ With the congruence of `●`, we can prove that application is a congruence by direct equational reasoning. \begin{code} -app-cong : ∀{Γ}{L L' M M' : Γ ⊢ ★} - → ℰ L ≃ ℰ L' - → ℰ M ≃ ℰ M' +app-cong : ∀{Γ}{L L′ M M′ : Γ ⊢ ★} + → ℰ L ≃ ℰ L′ + → ℰ M ≃ ℰ M′ ------------------------- - → ℰ (L · M) ≃ ℰ (L' · M') -app-cong {Γ}{L}{L'}{M}{M'} L≅L' M≅M' = + → ℰ (L · M) ≃ ℰ (L′ · M′) +app-cong {Γ}{L}{L′}{M}{M′} L≅L′ M≅M′ = start ℰ (L · M) ≃⟨ app-equiv ⟩ ℰ L ● ℰ M - ≃⟨ ●-cong L≅L' M≅M' ⟩ - ℰ L' ● ℰ M' + ≃⟨ ●-cong L≅L′ M≅M′ ⟩ + ℰ L′ ● ℰ M′ ≃⟨ ≃-sym app-equiv ⟩ - ℰ (L' · M') + ℰ (L′ · M′) ☐ \end{code} @@ -434,15 +434,23 @@ compositionality : ∀{Γ Δ}{C : Ctx Γ Δ} {M N : Γ ⊢ ★} --------------------------- → ℰ (plug C M) ≃ ℰ (plug C N) compositionality {C = CHole} M≃N = - M≃N -compositionality {C = CLam C'} M≃N = - lam-cong (compositionality {C = C'} M≃N) -compositionality {C = CAppL C' L} M≃N = - app-cong (compositionality {C = C'} M≃N) λ γ v → ⟨ (λ x → x) , (λ x → x) ⟩ -compositionality {C = CAppR L C'} M≃N = - app-cong (λ γ v → ⟨ (λ x → x) , (λ x → x) ⟩) (compositionality {C = C'} M≃N) + M≃N +compositionality {C = CLam C′} M≃N = + lam-cong (compositionality {C = C′} M≃N) +compositionality {C = CAppL C′ L} M≃N = + app-cong (compositionality {C = C′} M≃N) λ γ v → ⟨ (λ x → x) , (λ x → x) ⟩ +compositionality {C = CAppR L C′} M≃N = + app-cong (λ γ v → ⟨ (λ x → x) , (λ x → x) ⟩) (compositionality {C = C′} M≃N) \end{code} The proof is a straightforward induction on the context `C`, using the congruence properties `lam-cong` and `app-cong` that we established above. + +## Unicode + +This chapter uses the following unicode: + + ℱ U+2131 SCRIPT CAPITAL F (\McF) + ● U+2131 BLACK CIRCLE (\cib) + diff --git a/src/plfa/ContextualEquivalence.lagda b/src/plfa/ContextualEquivalence.lagda index 08aa2857..ec0d88de 100644 --- a/src/plfa/ContextualEquivalence.lagda +++ b/src/plfa/ContextualEquivalence.lagda @@ -115,3 +115,10 @@ denot-equal-contex-equal{Γ}{M}{N} eq {C} = ⟨ (λ tm → denot-equal-terminates eq tm) , (λ tn → denot-equal-terminates (≃-sym eq) tn) ⟩ \end{code} + + +## Unicode + +This chapter uses the following unicode: + + ≅ U+2245 APPROXIMATELY EQUAL TO (\~= or \cong) diff --git a/src/plfa/Soundness.lagda b/src/plfa/Soundness.lagda index b3ae0a5c..a8e66680 100644 --- a/src/plfa/Soundness.lagda +++ b/src/plfa/Soundness.lagda @@ -102,7 +102,7 @@ subst-ext : ∀ {Γ Δ v} {γ : Env Γ} {δ : Env Δ} -------------------------- → δ `, v `⊢ exts σ ↓ γ `, v subst-ext σ d Z = var -subst-ext σ d (S x) = rename-pres S_ (λ _ → Refl⊑) (d x) +subst-ext σ d (S x′) = rename-pres S_ (λ _ → Refl⊑) (d x′) \end{code} The proof is by cases on the de Bruijn index `x`. @@ -110,8 +110,8 @@ The proof is by cases on the de Bruijn index `x`. * If it is `Z`, then we need to show that `δ , v ⊢ # 0 ↓ v`, which we have by rule `var`. -* If it is `S x'`,then we need to show that - `δ , v ⊢ rename S_ (σ x') ↓ nth x' γ`, +* If it is `S x′`,then we need to show that + `δ , v ⊢ rename S_ (σ x′) ↓ nth x′ γ`, which we obtain by the `rename-pres` lemma. With the extension lemma in hand, the proof that simultaneous @@ -312,8 +312,8 @@ In the upcoming uses of `rename-reflect`, the renaming will always be the increment function. So we prove a corollary for that special case. \begin{code} -rename-inc-reflect : ∀ {Γ v' v} {γ : Env Γ} { M : Γ ⊢ ★} - → (γ `, v') ⊢ rename S_ M ↓ v +rename-inc-reflect : ∀ {Γ v′ v} {γ : Env Γ} { M : Γ ⊢ ★} + → (γ `, v′) ⊢ rename S_ M ↓ v ---------------------------- → γ ⊢ M ↓ v rename-inc-reflect d = rename-reflect `Refl⊑ d @@ -376,7 +376,7 @@ nth-const-env : ∀{Γ} {x : Γ ∋ ★} {v} → (const-env x v) x ≡ v nth-const-env {x = x} rewrite var≟-refl x = refl \end{code} -The nth element of `const-env n' v` is the value `⊥, so long as `n ≢ n'`. +The nth element of `const-env n′ v` is the value `⊥, so long as `n ≢ n′`. \begin{code} diff-nth-const-env : ∀{Γ} {x y : Γ ∋ ★} {v} @@ -482,13 +482,13 @@ subst-reflect {M = M}{σ = σ} (var {x = y}) eqL with M ... | ` x with var {x = y} ... | yv rewrite sym eqL = subst-reflect-var {σ = σ} yv subst-reflect {M = M} (var {x = y}) () | M₁ · M₂ -subst-reflect {M = M} (var {x = y}) () | ƛ M' +subst-reflect {M = M} (var {x = y}) () | ƛ M′ subst-reflect {M = M}{σ = σ} (↦-elim d₁ d₂) eqL with M ... | ` x with ↦-elim d₁ d₂ -... | d' rewrite sym eqL = subst-reflect-var {σ = σ} d' -subst-reflect (↦-elim d₁ d₂) () | ƛ M' +... | d′ rewrite sym eqL = subst-reflect-var {σ = σ} d′ +subst-reflect (↦-elim d₁ d₂) () | ƛ M′ subst-reflect{Γ}{Δ}{γ}{σ = σ} (↦-elim d₁ d₂) refl | M₁ · M₂ with subst-reflect {M = M₁} d₁ refl | subst-reflect {M = M₂} d₂ refl @@ -499,8 +499,8 @@ subst-reflect{Γ}{Δ}{γ}{σ = σ} (↦-elim d₁ d₂) subst-reflect {M = M}{σ = σ} (↦-intro d) eqL with M ... | ` x with (↦-intro d) -... | d' rewrite sym eqL = subst-reflect-var {σ = σ} d' -subst-reflect {σ = σ} (↦-intro d) eq | ƛ M' +... | d′ rewrite sym eqL = subst-reflect-var {σ = σ} d′ +subst-reflect {σ = σ} (↦-intro d) eq | ƛ M′ with subst-reflect {σ = exts σ} d (lambda-inj eq) ... | ⟨ δ′ , ⟨ exts-σ-δ′ , m′ ⟩ ⟩ = ⟨ init δ′ , ⟨ ((λ x → rename-inc-reflect (exts-σ-δ′ (S x)))) , @@ -536,17 +536,17 @@ subst-reflect (sub d lt) eq We conclude this case by obtaining `γ ⊢ σ ↓ δ₁ ⊔ δ₂` by the `subst-⊔` lemma. -* Case `↦-intro`: We have `subst σ M ≡ ƛ L'`. We proceed by cases on `M`. +* Case `↦-intro`: We have `subst σ M ≡ ƛ L′`. We proceed by cases on `M`. * Case `M ≡ x`: We apply the `subst-reflect-var` lemma. - * Case `M ≡ ƛ M'`: By the induction hypothesis, we have - `(δ' , v') ⊢ M' ↓ v₂` and `(δ , v₁) ⊢ exts σ ↓ (δ' , v')`. - From the later we have `(δ , v₁) ⊢ # 0 ↓ v'`. - By the lemma `var-inv` we have `v' ⊑ v₁`, so by the `up-env` lemma we - have `(δ' , v₁) ⊢ M' ↓ v₂` and therefore `δ' ⊢ ƛ M' ↓ v₁ → v₂`. We - also need to show that `δ `⊢ σ ↓ δ'`. Fix `k`. We have - `(δ , v₁) ⊢ rename S_ σ k ↓ nth k δ'`. We then apply the lemma - `rename-inc-reflect` to obtain `δ ⊢ σ k ↓ nth k δ'`, so this case is + * Case `M ≡ ƛ M′`: By the induction hypothesis, we have + `(δ′ , v′) ⊢ M′ ↓ v₂` and `(δ , v₁) ⊢ exts σ ↓ (δ′ , v′)`. + From the later we have `(δ , v₁) ⊢ # 0 ↓ v′`. + By the lemma `var-inv` we have `v′ ⊑ v₁`, so by the `up-env` lemma we + have `(δ′ , v₁) ⊢ M′ ↓ v₂` and therefore `δ′ ⊢ ƛ M′ ↓ v₁ → v₂`. We + also need to show that `δ `⊢ σ ↓ δ′`. Fix `k`. We have + `(δ , v₁) ⊢ rename S_ σ k ↓ nth k δ′`. We then apply the lemma + `rename-inc-reflect` to obtain `δ ⊢ σ k ↓ nth k δ′`, so this case is complete. * Case `⊥-intro`: We choose `⊥` for `δ`. @@ -571,45 +571,45 @@ give terms `N : (Γ , ★ ⊢ ★)` and `M : (Γ ⊢ ★)`, if `γ ⊢ N [ M ] ↓ w`, then `γ ⊢ M ↓ v` and `(γ , v) ⊢ N ↓ w` for some value `v`. We have `N [ M ] = subst (subst-zero M) N`. We apply the `subst-reflect` lemma to obtain -`γ ⊢ subst-zero M ↓ (δ' , v')` and `(δ' , v') ⊢ N ↓ w` -for some `δ'` and `v'`. +`γ ⊢ subst-zero M ↓ (δ′ , v′)` and `(δ′ , v′) ⊢ N ↓ w` +for some `δ′` and `v′`. -Instantiating `γ ⊢ subst-zero M ↓ (δ' , v')` at `k = 0` -gives us `γ ⊢ M ↓ v'`. We choose `w = v'`, so the first +Instantiating `γ ⊢ subst-zero M ↓ (δ′ , v′)` at `k = 0` +gives us `γ ⊢ M ↓ v′`. We choose `w = v′`, so the first part of our conclusion is complete. -It remains to prove `(γ , v') ⊢ N ↓ v`. First, we obtain -`(γ , v') ⊢ rename var-id N ↓ v` by the `rename-pres` lemma -applied to `(δ' , v') ⊢ N ↓ v`, with the `var-id` renaming, -`γ = (δ' , v')`, and `δ = (γ , v')`. To apply this lemma, +It remains to prove `(γ , v′) ⊢ N ↓ v`. First, we obtain +`(γ , v′) ⊢ rename var-id N ↓ v` by the `rename-pres` lemma +applied to `(δ′ , v′) ⊢ N ↓ v`, with the `var-id` renaming, +`γ = (δ′ , v′)`, and `δ = (γ , v′)`. To apply this lemma, we need to show that -`nth n (δ' , v') ⊑ nth (var-id n) (γ , v')` for any `n`. +`nth n (δ′ , v′) ⊑ nth (var-id n) (γ , v′)` for any `n`. This is accomplished by the following lemma, which -makes use of `γ ⊢ subst-zero M ↓ (δ' , v')`. +makes use of `γ ⊢ subst-zero M ↓ (δ′ , v′)`. \begin{code} -nth-id-le : ∀{Γ}{δ'}{v'}{γ}{M} - → γ `⊢ subst-zero M ↓ (δ' `, v') +nth-id-le : ∀{Γ}{δ′}{v′}{γ}{M} + → γ `⊢ subst-zero M ↓ (δ′ `, v′) ----------------------------------------------------- - → (x : Γ , ★ ∋ ★) → (δ' `, v') x ⊑ (γ `, v') (var-id x) -nth-id-le γ-sz-δ'v' Z = Refl⊑ -nth-id-le γ-sz-δ'v' (S n') = var-inv (γ-sz-δ'v' (S n')) + → (x : Γ , ★ ∋ ★) → (δ′ `, v′) x ⊑ (γ `, v′) (var-id x) +nth-id-le γ-sz-δ′v′ Z = Refl⊑ +nth-id-le γ-sz-δ′v′ (S n′) = var-inv (γ-sz-δ′v′ (S n′)) \end{code} The above lemma proceeds by induction on `n`. -* If it is `Z`, then we show that `v' ⊑ v'` by `Refl⊑`. -* If it is `S n'`, then from the premise we obtain - `γ ⊢ # n' ↓ nth n' δ'`. By `var-inv` we have - `nth n' δ' ⊑ nth n' γ` from which we conclude that - `nth (S n') (δ' , v') ⊑ nth (var-id (S n')) (γ , v')`. +* If it is `Z`, then we show that `v′ ⊑ v′` by `Refl⊑`. +* If it is `S n′`, then from the premise we obtain + `γ ⊢ # n′ ↓ nth n′ δ′`. By `var-inv` we have + `nth n′ δ′ ⊑ nth n′ γ` from which we conclude that + `nth (S n′) (δ′ , v′) ⊑ nth (var-id (S n′)) (γ , v′)`. Returning to the proof that single substitution reflects denotations, we have just proved that - (γ `, v') ⊢ rename var-id N ↓ v + (γ `, v′) ⊢ rename var-id N ↓ v -but we need to show `(γ `, v') ⊢ N ↓ v`. +but we need to show `(γ `, v′) ⊢ N ↓ v`. So we apply the `rename-id` lemma to obtain `rename var-id N ≡ N`. @@ -647,30 +647,30 @@ reflect-beta : ∀{Γ}{γ : Env Γ}{M N}{v} → γ ⊢ (ƛ N) · M ↓ v reflect-beta d with substitution-reflect d -... | ⟨ v₂' , ⟨ d₁' , d₂' ⟩ ⟩ = ↦-elim (↦-intro d₂') d₁' +... | ⟨ v₂′ , ⟨ d₁′ , d₂′ ⟩ ⟩ = ↦-elim (↦-intro d₂′) d₁′ -reflect : ∀ {Γ} {γ : Env Γ} {M M' N v} - → γ ⊢ N ↓ v → M —→ M' → M' ≡ N +reflect : ∀ {Γ} {γ : Env Γ} {M M′ N v} + → γ ⊢ N ↓ v → M —→ M′ → M′ ≡ N --------------------------------- → γ ⊢ M ↓ v reflect var (ξ₁ r) () reflect var (ξ₂ r) () reflect{γ = γ} (var{x = x}) β mn with var{γ = γ}{x = x} -... | d' rewrite sym mn = reflect-beta d' +... | d′ rewrite sym mn = reflect-beta d′ reflect var (ζ r) () reflect (↦-elim d₁ d₂) (ξ₁ r) refl = ↦-elim (reflect d₁ r refl) d₂ reflect (↦-elim d₁ d₂) (ξ₂ r) refl = ↦-elim d₁ (reflect d₂ r refl) reflect (↦-elim d₁ d₂) β mn with ↦-elim d₁ d₂ -... | d' rewrite sym mn = reflect-beta d' +... | d′ rewrite sym mn = reflect-beta d′ reflect (↦-elim d₁ d₂) (ζ r) () reflect (↦-intro d) (ξ₁ r) () reflect (↦-intro d) (ξ₂ r) () reflect (↦-intro d) β mn with ↦-intro d -... | d' rewrite sym mn = reflect-beta d' +... | d′ rewrite sym mn = reflect-beta d′ reflect (↦-intro d) (ζ r) refl = ↦-intro (reflect d r refl) reflect ⊥-intro r mn = ⊥-intro reflect (⊔-intro d₁ d₂) r mn rewrite sym mn = @@ -708,3 +708,9 @@ soundness {Γ} (L —→⟨ r ⟩ M—↠N) γ v = ≃-trans {Γ} e ih γ v \end{code} + +## Unicode + +This chapter uses the following unicode: + + ≟ U+225F QUESTIONED EQUAL TO (\?=)