From 3f9f9c3c000b367bbf2d49910553585d9d919e72 Mon Sep 17 00:00:00 2001 From: Jeremy Siek Date: Mon, 19 Aug 2019 17:14:07 -0400 Subject: [PATCH] lowercase constructors --- src/plfa/part2/Confluence.lagda.md | 8 +- src/plfa/part3/Adequacy.lagda.md | 174 +++++++++++----------- src/plfa/part3/Compositional.lagda.md | 87 +++++------ src/plfa/part3/Denotational.lagda.md | 202 +++++++++++++------------- src/plfa/part3/Soundness.lagda.md | 30 ++-- 5 files changed, 253 insertions(+), 248 deletions(-) diff --git a/src/plfa/part2/Confluence.lagda.md b/src/plfa/part2/Confluence.lagda.md index a7e0a76e..17faee5a 100644 --- a/src/plfa/part2/Confluence.lagda.md +++ b/src/plfa/part2/Confluence.lagda.md @@ -13,8 +13,8 @@ module plfa.part2.Confluence where ## Introduction In this chapter we prove that beta reduction is _confluent_, a -property also known as _Church-Rosser_. That is, if there is a -reduction sequence from any term `L` to two different terms `M₁` and +property also known as _Church-Rosser_. That is, if there are +reduction sequences from any term `L` to two different terms `M₁` and `M₂`, then there exist reduction sequences from those two terms to some common term `N`. In pictures: @@ -315,8 +315,8 @@ par-subst-exts s {x = Z} = pvar par-subst-exts s {x = S x} = par-rename s ``` -The next lemma that we need to prove that substitution respects -parallel reduction is the following one, which states that +The next lemma that we need for proving that substitution respects +parallel reduction is the following which states that simultaneoous substitution commutes with single substitution. We import this lemma from Chapter [Substitution]({{ site.baseurl }}/Substitution/) and restate it below. diff --git a/src/plfa/part3/Adequacy.lagda.md b/src/plfa/part3/Adequacy.lagda.md index b186be0d..21300022 100644 --- a/src/plfa/part3/Adequacy.lagda.md +++ b/src/plfa/part3/Adequacy.lagda.md @@ -90,9 +90,9 @@ open import plfa.part2.BigStep using (Clos; clos; ClosEnv; ∅'; _,'_; _⊢_⇓_; ⇓-var; ⇓-lam; ⇓-app; ⇓-determ; cbn→reduce) open import plfa.part3.Denotational - using (Value; Env; `∅; _`,_; _↦_; _⊑_; _⊢_↓_; ⊥; Funs∈; _⊔_; ∈→⊑; + using (Value; Env; `∅; _`,_; _↦_; _⊑_; _⊢_↓_; ⊥; all-funs∈; _⊔_; ∈→⊑; var; ↦-elim; ↦-intro; ⊔-intro; ⊥-intro; sub; ℰ; _≃_; _iff_; - Trans⊑; ConjR1⊑; ConjR2⊑; ConjL⊑; Refl⊑; Fun⊑; Bot⊑; Dist⊑; + ⊑-trans; ⊑-conj-R1; ⊑-conj-R2; ⊑-conj-L; ⊑-refl; ⊑-fun; ⊑-bot; ⊑-dist; sub-inv-fun) open import plfa.part3.Soundness using (soundness) @@ -105,29 +105,29 @@ We define the following short-hand for saying that a value is greather-than or equal to a function value. ``` -AboveFun : Value → Set -AboveFun u = Σ[ v ∈ Value ] Σ[ w ∈ Value ] v ↦ w ⊑ u +above-fun : Value → Set +above-fun u = Σ[ v ∈ Value ] Σ[ w ∈ Value ] v ↦ w ⊑ u ``` If a value `u` is greater than a function, then an even greater value `u'` is too. ``` -AboveFun-⊑ : ∀{u u' : Value} - → AboveFun u → u ⊑ u' +above-fun-⊑ : ∀{u u' : Value} + → above-fun u → u ⊑ u' ------------------- - → AboveFun u' -AboveFun-⊑ ⟨ v , ⟨ w , lt' ⟩ ⟩ lt = ⟨ v , ⟨ w , Trans⊑ lt' lt ⟩ ⟩ + → above-fun u' +above-fun-⊑ ⟨ v , ⟨ w , lt' ⟩ ⟩ lt = ⟨ v , ⟨ w , ⊑-trans lt' lt ⟩ ⟩ ``` The bottom value `⊥` is not greater than a function. ``` -AboveFun⊥ : ¬ AboveFun ⊥ -AboveFun⊥ ⟨ v , ⟨ w , lt ⟩ ⟩ +above-fun⊥ : ¬ above-fun ⊥ +above-fun⊥ ⟨ v , ⟨ w , lt ⟩ ⟩ with sub-inv-fun lt ... | ⟨ Γ , ⟨ f , ⟨ Γ⊆⊥ , ⟨ lt1 , lt2 ⟩ ⟩ ⟩ ⟩ - with Funs∈ f + with all-funs∈ f ... | ⟨ A , ⟨ B , m ⟩ ⟩ with Γ⊆⊥ m ... | () @@ -137,13 +137,13 @@ If the join of two values `u` and `u'` is greater than a function, then at least one of them is too. ``` -AboveFun-⊔ : ∀{u u'} - → AboveFun (u ⊔ u') - → AboveFun u ⊎ AboveFun u' -AboveFun-⊔{u}{u'} ⟨ v , ⟨ w , v↦w⊑u⊔u' ⟩ ⟩ +above-fun-⊔ : ∀{u u'} + → above-fun (u ⊔ u') + → above-fun u ⊎ above-fun u' +above-fun-⊔{u}{u'} ⟨ v , ⟨ w , v↦w⊑u⊔u' ⟩ ⟩ with sub-inv-fun v↦w⊑u⊔u' ... | ⟨ Γ , ⟨ f , ⟨ Γ⊆u⊔u' , ⟨ lt1 , lt2 ⟩ ⟩ ⟩ ⟩ - with Funs∈ f + with all-funs∈ f ... | ⟨ A , ⟨ B , m ⟩ ⟩ with Γ⊆u⊔u' m ... | inj₁ x = inj₁ ⟨ A , ⟨ B , (∈→⊑ x) ⟩ ⟩ @@ -154,11 +154,11 @@ On the other hand, if neither of `u` and `u'` is greater than a function, then their join is also not greater than a function. ``` -not-AboveFun-⊔ : ∀{u u' : Value} - → ¬ AboveFun u → ¬ AboveFun u' - → ¬ AboveFun (u ⊔ u') -not-AboveFun-⊔ naf1 naf2 af12 - with AboveFun-⊔ af12 +not-above-fun-⊔ : ∀{u u' : Value} + → ¬ above-fun u → ¬ above-fun u' + → ¬ above-fun (u ⊔ u') +not-above-fun-⊔ naf1 naf2 af12 + with above-fun-⊔ af12 ... | inj₁ af1 = contradiction af1 naf1 ... | inj₂ af2 = contradiction af2 naf2 ``` @@ -167,30 +167,30 @@ The converse is also true. If the join of two values is not above a function, then neither of them is individually. ``` -not-AboveFun-⊔-inv : ∀{u u' : Value} → ¬ AboveFun (u ⊔ u') - → ¬ AboveFun u × ¬ AboveFun u' -not-AboveFun-⊔-inv af = ⟨ f af , g af ⟩ +not-above-fun-⊔-inv : ∀{u u' : Value} → ¬ above-fun (u ⊔ u') + → ¬ above-fun u × ¬ above-fun u' +not-above-fun-⊔-inv af = ⟨ f af , g af ⟩ where - f : ∀{u u' : Value} → ¬ AboveFun (u ⊔ u') → ¬ AboveFun u + f : ∀{u u' : Value} → ¬ above-fun (u ⊔ u') → ¬ above-fun u f{u}{u'} af12 ⟨ v , ⟨ w , lt ⟩ ⟩ = - contradiction ⟨ v , ⟨ w , ConjR1⊑ lt ⟩ ⟩ af12 - g : ∀{u u' : Value} → ¬ AboveFun (u ⊔ u') → ¬ AboveFun u' + contradiction ⟨ v , ⟨ w , ⊑-conj-R1 lt ⟩ ⟩ af12 + g : ∀{u u' : Value} → ¬ above-fun (u ⊔ u') → ¬ above-fun u' g{u}{u'} af12 ⟨ v , ⟨ w , lt ⟩ ⟩ = - contradiction ⟨ v , ⟨ w , ConjR2⊑ lt ⟩ ⟩ af12 + contradiction ⟨ v , ⟨ w , ⊑-conj-R2 lt ⟩ ⟩ af12 ``` The property of being greater than a function value is decidable, as exhibited by the following function. ``` -AboveFun? : (v : Value) → Dec (AboveFun v) -AboveFun? ⊥ = no AboveFun⊥ -AboveFun? (v ↦ w) = yes ⟨ v , ⟨ w , Refl⊑ ⟩ ⟩ -AboveFun? (u ⊔ u') - with AboveFun? u | AboveFun? u' -... | yes ⟨ v , ⟨ w , lt ⟩ ⟩ | _ = yes ⟨ v , ⟨ w , (ConjR1⊑ lt) ⟩ ⟩ -... | no _ | yes ⟨ v , ⟨ w , lt ⟩ ⟩ = yes ⟨ v , ⟨ w , (ConjR2⊑ lt) ⟩ ⟩ -... | no x | no y = no (not-AboveFun-⊔ x y) +above-fun? : (v : Value) → Dec (above-fun v) +above-fun? ⊥ = no above-fun⊥ +above-fun? (v ↦ w) = yes ⟨ v , ⟨ w , ⊑-refl ⟩ ⟩ +above-fun? (u ⊔ u') + with above-fun? u | above-fun? u' +... | yes ⟨ v , ⟨ w , lt ⟩ ⟩ | _ = yes ⟨ v , ⟨ w , (⊑-conj-R1 lt) ⟩ ⟩ +... | no _ | yes ⟨ v , ⟨ w , lt ⟩ ⟩ = yes ⟨ v , ⟨ w , (⊑-conj-R2 lt) ⟩ ⟩ +... | no x | no y = no (not-above-fun-⊔ x y) ``` @@ -222,7 +222,7 @@ describe below. 𝕍 v (clos (M · M₁) γ) = Bot 𝕍 ⊥ (clos (ƛ M) γ) = ⊤ 𝕍 (v ↦ w) (clos (ƛ N) γ) = - (∀{c : Clos} → 𝔼 v c → AboveFun w → Σ[ c' ∈ Clos ] + (∀{c : Clos} → 𝔼 v c → above-fun w → Σ[ c' ∈ Clos ] (γ ,' c) ⊢ N ⇓ c' × 𝕍 w c') 𝕍 (u ⊔ v) (clos (ƛ N) γ) = 𝕍 u (clos (ƛ N) γ) × 𝕍 v (clos (ƛ N) γ) ``` @@ -242,7 +242,7 @@ The definition of `𝔼` is straightforward. If `v` is a greater than a function, then `M` evaluates to a closure related to `v`. ``` -𝔼 v (clos M γ') = AboveFun v → Σ[ c ∈ Clos ] γ' ⊢ M ⇓ c × 𝕍 v c +𝔼 v (clos M γ') = above-fun v → Σ[ c ∈ Clos ] γ' ⊢ M ⇓ c × 𝕍 v c ``` The proof of the main lemma is by induction on `γ ⊢ M ↓ v`, so it goes @@ -310,15 +310,15 @@ values that are not greater than a function, that is, values that are equivalent to `⊥`. In such cases, `𝕍 v (clos (ƛ N) γ')` is trivially true. ``` -not-AboveFun-𝕍 : ∀{v : Value}{Γ}{γ' : ClosEnv Γ}{N : Γ , ★ ⊢ ★ } - → ¬ AboveFun v +not-above-fun-𝕍 : ∀{v : Value}{Γ}{γ' : ClosEnv Γ}{N : Γ , ★ ⊢ ★ } + → ¬ above-fun v ------------------- → 𝕍 v (clos (ƛ N) γ') -not-AboveFun-𝕍 {⊥} af = tt -not-AboveFun-𝕍 {v ↦ v'} af = ⊥-elim (contradiction ⟨ v , ⟨ v' , Refl⊑ ⟩ ⟩ af) -not-AboveFun-𝕍 {v₁ ⊔ v₂} af - with not-AboveFun-⊔-inv af -... | ⟨ af1 , af2 ⟩ = ⟨ not-AboveFun-𝕍 af1 , not-AboveFun-𝕍 af2 ⟩ +not-above-fun-𝕍 {⊥} af = tt +not-above-fun-𝕍 {v ↦ v'} af = ⊥-elim (contradiction ⟨ v , ⟨ v' , ⊑-refl ⟩ ⟩ af) +not-above-fun-𝕍 {v₁ ⊔ v₂} af + with not-above-fun-⊔-inv af +... | ⟨ af1 , af2 ⟩ = ⟨ not-above-fun-𝕍 af1 , not-above-fun-𝕍 af2 ⟩ ``` The proofs of `𝕍-sub` and `𝔼-sub` are intertwined. @@ -335,48 +335,48 @@ cases for variables and application. We then proceed by induction on ``` sub-𝕍 {clos (` x) γ} {v} () lt sub-𝕍 {clos (L · M) γ} () lt -sub-𝕍 {clos (ƛ N) γ} vc Bot⊑ = tt -sub-𝕍 {clos (ƛ N) γ} vc (ConjL⊑ lt1 lt2) = ⟨ (sub-𝕍 vc lt1) , sub-𝕍 vc lt2 ⟩ -sub-𝕍 {clos (ƛ N) γ} ⟨ vv1 , vv2 ⟩ (ConjR1⊑ lt) = sub-𝕍 vv1 lt -sub-𝕍 {clos (ƛ N) γ} ⟨ vv1 , vv2 ⟩ (ConjR2⊑ lt) = sub-𝕍 vv2 lt -sub-𝕍 {clos (ƛ N) γ} vc (Trans⊑{v = v₂} lt1 lt2) = sub-𝕍 (sub-𝕍 vc lt2) lt1 -sub-𝕍 {clos (ƛ N) γ} vc (Fun⊑ lt1 lt2) ev1 sf - with vc (sub-𝔼 ev1 lt1) (AboveFun-⊑ sf lt2) +sub-𝕍 {clos (ƛ N) γ} vc ⊑-bot = tt +sub-𝕍 {clos (ƛ N) γ} vc (⊑-conj-L lt1 lt2) = ⟨ (sub-𝕍 vc lt1) , sub-𝕍 vc lt2 ⟩ +sub-𝕍 {clos (ƛ N) γ} ⟨ vv1 , vv2 ⟩ (⊑-conj-R1 lt) = sub-𝕍 vv1 lt +sub-𝕍 {clos (ƛ N) γ} ⟨ vv1 , vv2 ⟩ (⊑-conj-R2 lt) = sub-𝕍 vv2 lt +sub-𝕍 {clos (ƛ N) γ} vc (⊑-trans{v = v₂} lt1 lt2) = sub-𝕍 (sub-𝕍 vc lt2) lt1 +sub-𝕍 {clos (ƛ N) γ} vc (⊑-fun lt1 lt2) ev1 sf + with vc (sub-𝔼 ev1 lt1) (above-fun-⊑ sf lt2) ... | ⟨ c , ⟨ Nc , v4 ⟩ ⟩ = ⟨ c , ⟨ Nc , sub-𝕍 v4 lt2 ⟩ ⟩ -sub-𝕍 {clos (ƛ N) γ} {v ↦ w ⊔ v ↦ w'} ⟨ vcw , vcw' ⟩ Dist⊑ ev1c sf - with AboveFun? w | AboveFun? w' +sub-𝕍 {clos (ƛ N) γ} {v ↦ w ⊔ v ↦ w'} ⟨ vcw , vcw' ⟩ ⊑-dist ev1c sf + with above-fun? w | above-fun? w' ... | yes af2 | yes af3 with vcw ev1c af2 | vcw' ev1c af3 ... | ⟨ clos L δ , ⟨ L⇓c₂ , 𝕍w ⟩ ⟩ | ⟨ c₃ , ⟨ L⇓c₃ , 𝕍w' ⟩ ⟩ rewrite ⇓-determ L⇓c₃ L⇓c₂ with 𝕍→WHNF 𝕍w ... | ƛ_ = ⟨ clos L δ , ⟨ L⇓c₂ , ⟨ 𝕍w , 𝕍w' ⟩ ⟩ ⟩ -sub-𝕍 {c} {v ↦ w ⊔ v ↦ w'} ⟨ vcw , vcw' ⟩ Dist⊑ ev1c sf +sub-𝕍 {c} {v ↦ w ⊔ v ↦ w'} ⟨ vcw , vcw' ⟩ ⊑-dist ev1c sf | yes af2 | no naf3 with vcw ev1c af2 ... | ⟨ clos {Γ'} L γ₁ , ⟨ L⇓c2 , 𝕍w ⟩ ⟩ with 𝕍→WHNF 𝕍w ... | ƛ_ {N = N'} = - let 𝕍w' = not-AboveFun-𝕍{w'}{Γ'}{γ₁}{N'} naf3 in + let 𝕍w' = not-above-fun-𝕍{w'}{Γ'}{γ₁}{N'} naf3 in ⟨ clos (ƛ N') γ₁ , ⟨ L⇓c2 , 𝕍⊔-intro 𝕍w 𝕍w' ⟩ ⟩ -sub-𝕍 {c} {v ↦ w ⊔ v ↦ w'} ⟨ vcw , vcw' ⟩ Dist⊑ ev1c sf +sub-𝕍 {c} {v ↦ w ⊔ v ↦ w'} ⟨ vcw , vcw' ⟩ ⊑-dist ev1c sf | no naf2 | yes af3 with vcw' ev1c af3 ... | ⟨ clos {Γ'} L γ₁ , ⟨ L⇓c3 , 𝕍w'c ⟩ ⟩ with 𝕍→WHNF 𝕍w'c ... | ƛ_ {N = N'} = - let 𝕍wc = not-AboveFun-𝕍{w}{Γ'}{γ₁}{N'} naf2 in + let 𝕍wc = not-above-fun-𝕍{w}{Γ'}{γ₁}{N'} naf2 in ⟨ clos (ƛ N') γ₁ , ⟨ L⇓c3 , 𝕍⊔-intro 𝕍wc 𝕍w'c ⟩ ⟩ -sub-𝕍 {c} {v ↦ w ⊔ v ↦ w'} ⟨ vcw , vcw' ⟩ Dist⊑ ev1c ⟨ v' , ⟨ w'' , lt ⟩ ⟩ +sub-𝕍 {c} {v ↦ w ⊔ v ↦ w'} ⟨ vcw , vcw' ⟩ ⊑-dist ev1c ⟨ v' , ⟨ w'' , lt ⟩ ⟩ | no naf2 | no naf3 - with AboveFun-⊔ ⟨ v' , ⟨ w'' , lt ⟩ ⟩ + with above-fun-⊔ ⟨ v' , ⟨ w'' , lt ⟩ ⟩ ... | inj₁ af2 = ⊥-elim (contradiction af2 naf2) ... | inj₂ af3 = ⊥-elim (contradiction af3 naf3) ``` -* Case `Bot⊑`. We immediately have `𝕍 ⊥ (clos (ƛ N) γ)`. +* Case `⊑-bot`. We immediately have `𝕍 ⊥ (clos (ƛ N) γ)`. -* Case `ConjL⊑`. +* Case `⊑-conj-L`. v₁' ⊑ v v₂' ⊑ v ------------------- @@ -385,7 +385,7 @@ sub-𝕍 {c} {v ↦ w ⊔ v ↦ w'} ⟨ vcw , vcw' ⟩ Dist⊑ ev1c ⟨ v' , ⟨ The induction hypotheses gives us `𝕍 v₁' (clos (ƛ N) γ)` and `𝕍 v₂' (clos (ƛ N) γ)`, which is all we need for this case. -* Case `ConjR1⊑`. +* Case `⊑-conj-R1`. v' ⊑ v₁ ------------- @@ -393,7 +393,7 @@ sub-𝕍 {c} {v ↦ w ⊔ v ↦ w'} ⟨ vcw , vcw' ⟩ Dist⊑ ev1c ⟨ v' , ⟨ The induction hypothesis gives us `𝕍 v' (clos (ƛ N) γ)`. -* Case `ConjR2⊑`. +* Case `⊑-conj-R2`. v' ⊑ v₂ ------------- @@ -401,7 +401,7 @@ sub-𝕍 {c} {v ↦ w ⊔ v ↦ w'} ⟨ vcw , vcw' ⟩ Dist⊑ ev1c ⟨ v' , ⟨ Again, the induction hypothesis gives us `𝕍 v' (clos (ƛ N) γ)`. -* Case `Trans⊑`. +* Case `⊑-trans`. v' ⊑ v₂ v₂ ⊑ v ----------------- @@ -411,7 +411,7 @@ sub-𝕍 {c} {v ↦ w ⊔ v ↦ w'} ⟨ vcw , vcw' ⟩ Dist⊑ ev1c ⟨ v' , ⟨ `𝕍 v₂ (clos (ƛ N) γ)`. We apply the induction hypothesis for `v' ⊑ v₂` to conclude that `𝕍 v' (clos (ƛ N) γ)`. -* Case `Dist⊑`. This case is the most difficult. We have +* Case `⊑-dist`. This case is the most difficult. We have 𝕍 (v ↦ w) (clos (ƛ N) γ) 𝕍 (v ↦ w') (clos (ƛ N) γ) @@ -423,7 +423,7 @@ sub-𝕍 {c} {v ↦ w ⊔ v ↦ w'} ⟨ vcw , vcw' ⟩ Dist⊑ ev1c ⟨ v' , ⟨ Let `c` be an arbtrary closure such that `𝔼 v c`. Assume `w ⊔ w'` is greater than a function. Unfortunately, this does not mean that both `w` and `w'` - are above functions. But thanks to the lemma `AboveFun-⊔`, + are above functions. But thanks to the lemma `above-fun-⊔`, we know that at least one of them is greater than a function. * Suppose both of them are greater than a function. Then we have @@ -433,10 +433,10 @@ sub-𝕍 {c} {v ↦ w ⊔ v ↦ w'} ⟨ vcw , vcw' ⟩ Dist⊑ ev1c ⟨ v' , ⟨ for some `N'`. We conclude that `𝕍 (w ⊔ w') (clos (ƛ N') δ)`. * Suppose one of them is greater than a function and the other is - not: say `AboveFun w` and `¬ AboveFun w'`. Then from + not: say `above-fun w` and `¬ above-fun w'`. Then from `𝕍 (v ↦ w) (clos (ƛ N) γ)` we have `γ ⊢ N ⇓ clos L γ₁` and `𝕍 w (clos L γ₁)`. From this we have - `L ≡ ƛ N'` for some `N'`. Meanwhile, from `¬ AboveFun w'` we have + `L ≡ ƛ N'` for some `N'`. Meanwhile, from `¬ above-fun w'` we have `𝕍 w' (clos L γ₁)`. We conclude that `𝕍 (w ⊔ w') (clos (ƛ N') γ₁)`. @@ -445,12 +445,12 @@ The proof of `sub-𝔼` is direct and explained below. ``` sub-𝔼 {clos M γ} {v} {v'} 𝔼v v'⊑v fv' - with 𝔼v (AboveFun-⊑ fv' v'⊑v) + with 𝔼v (above-fun-⊑ fv' v'⊑v) ... | ⟨ c , ⟨ M⇓c , 𝕍v ⟩ ⟩ = ⟨ c , ⟨ M⇓c , sub-𝕍 𝕍v v'⊑v ⟩ ⟩ ``` -From `AboveFun v'` and `v' ⊑ v` we have `AboveFun v`. Then with `𝔼 v c` we +From `above-fun v'` and `v' ⊑ v` we have `above-fun v`. Then with `𝔼 v c` we obtain a closure `c` such that `γ ⊢ M ⇓ c` and `𝕍 v c`. We conclude with an application of `sub-𝕍` with `v' ⊑ v` to show `𝕍 v' c`. @@ -482,7 +482,7 @@ kth-x{γ' = γ'}{x = x} with γ' x ... | ⟨ c , ⟨ M'⇓c , 𝕍γx ⟩ ⟩ = ⟨ c , ⟨ (⇓-var eq M'⇓c) , 𝕍γx ⟩ ⟩ ↓→𝔼 {Γ} {γ} {γ'} 𝔾γγ' (↦-elim{L = L}{M = M}{v = v₁}{w = v} d₁ d₂) fv - with ↓→𝔼 𝔾γγ' d₁ ⟨ v₁ , ⟨ v , Refl⊑ ⟩ ⟩ + with ↓→𝔼 𝔾γγ' d₁ ⟨ v₁ , ⟨ v , ⊑-refl ⟩ ⟩ ... | ⟨ clos L' δ , ⟨ L⇓L' , 𝕍v₁↦v ⟩ ⟩ with 𝕍→WHNF 𝕍v₁↦v ... | ƛ_ {N = N} @@ -491,12 +491,12 @@ kth-x{γ' = γ'}{x = x} with γ' x ⟨ c' , ⟨ ⇓-app L⇓L' N⇓c' , 𝕍v ⟩ ⟩ ↓→𝔼 {Γ} {γ} {γ'} 𝔾γγ' (↦-intro{N = N}{v = v}{w = w} d) fv↦w = ⟨ clos (ƛ N) γ' , ⟨ ⇓-lam , E ⟩ ⟩ - where E : {c : Clos} → 𝔼 v c → AboveFun w + where E : {c : Clos} → 𝔼 v c → above-fun w → Σ[ c' ∈ Clos ] (γ' ,' c) ⊢ N ⇓ c' × 𝕍 w c' E {c} 𝔼vc fw = ↓→𝔼 (λ {x} → 𝔾-ext{Γ}{γ}{γ'} 𝔾γγ' 𝔼vc {x}) d fw -↓→𝔼 𝔾γγ' ⊥-intro f⊥ = ⊥-elim (AboveFun⊥ f⊥) +↓→𝔼 𝔾γγ' ⊥-intro f⊥ = ⊥-elim (above-fun⊥ f⊥) ↓→𝔼 𝔾γγ' (⊔-intro{v = v₁}{w = v₂} d₁ d₂) fv12 - with AboveFun? v₁ | AboveFun? v₂ + with above-fun? v₁ | above-fun? v₂ ... | yes fv1 | yes fv2 with ↓→𝔼 𝔾γγ' d₁ fv1 | ↓→𝔼 𝔾γγ' d₂ fv2 ... | ⟨ c₁ , ⟨ M⇓c₁ , 𝕍v₁ ⟩ ⟩ | ⟨ c₂ , ⟨ M⇓c₂ , 𝕍v₂ ⟩ ⟩ @@ -507,28 +507,28 @@ kth-x{γ' = γ'}{x = x} with γ' x ... | ⟨ clos {Γ'} M' γ₁ , ⟨ M⇓c₁ , 𝕍v₁ ⟩ ⟩ with 𝕍→WHNF 𝕍v₁ ... | ƛ_ {N = N} = - let 𝕍v₂ = not-AboveFun-𝕍{v₂}{Γ'}{γ₁}{N} nfv2 in + let 𝕍v₂ = not-above-fun-𝕍{v₂}{Γ'}{γ₁}{N} nfv2 in ⟨ clos (ƛ N) γ₁ , ⟨ M⇓c₁ , 𝕍⊔-intro 𝕍v₁ 𝕍v₂ ⟩ ⟩ ↓→𝔼 𝔾γγ' (⊔-intro{v = v₁}{w = v₂} d₁ d₂) fv12 | no nfv1 | yes fv2 with ↓→𝔼 𝔾γγ' d₂ fv2 ... | ⟨ clos {Γ'} M' γ₁ , ⟨ M'⇓c₂ , 𝕍2c ⟩ ⟩ with 𝕍→WHNF 𝕍2c ... | ƛ_ {N = N} = - let 𝕍1c = not-AboveFun-𝕍{v₁}{Γ'}{γ₁}{N} nfv1 in + let 𝕍1c = not-above-fun-𝕍{v₁}{Γ'}{γ₁}{N} nfv1 in ⟨ clos (ƛ N) γ₁ , ⟨ M'⇓c₂ , 𝕍⊔-intro 𝕍1c 𝕍2c ⟩ ⟩ ↓→𝔼 𝔾γγ' (⊔-intro d₁ d₂) fv12 | no nfv1 | no nfv2 - with AboveFun-⊔ fv12 + with above-fun-⊔ fv12 ... | inj₁ fv1 = ⊥-elim (contradiction fv1 nfv1) ... | inj₂ fv2 = ⊥-elim (contradiction fv2 nfv2) ↓→𝔼 {Γ} {γ} {γ'} {M} {v'} 𝔾γγ' (sub{v = v} d v'⊑v) fv' - with ↓→𝔼 {Γ} {γ} {γ'} {M} 𝔾γγ' d (AboveFun-⊑ fv' v'⊑v) + with ↓→𝔼 {Γ} {γ} {γ'} {M} 𝔾γγ' d (above-fun-⊑ fv' v'⊑v) ... | ⟨ c , ⟨ M⇓c , 𝕍v ⟩ ⟩ = ⟨ c , ⟨ M⇓c , sub-𝕍 𝕍v v'⊑v ⟩ ⟩ ``` * Case `var`. Looking up `x` in `γ'` yields some closure, `clos M' δ`, and from `𝔾 γ γ'` we have `𝔼 (γ x) (clos M' δ)`. With the premise - `AboveFun (γ x)`, we obtain a closure `c` such that `δ ⊢ M' ⇓ c` + `above-fun (γ x)`, we obtain a closure `c` such that `δ ⊢ M' ⇓ c` and `𝕍 (γ x) c`. To conclude `γ' ⊢ x ⇓ c` via `⇓-var`, we need `γ' x ≡ clos M' δ`, which is obvious, but it requires some Agda shananigans via the `kth-x` lemma to get our hands on it. @@ -539,7 +539,7 @@ kth-x{γ' = γ'}{x = x} with γ' x Of course, `L' ≡ ƛ N` for some `N`. By the induction hypothesis for `γ ⊢ M ↓ v₁`, we have `𝔼 v₁ (clos M γ')`. - Together with the premise `AboveFun v` and `𝕍 v (clos L' δ)`, + Together with the premise `above-fun v` and `𝕍 v (clos L' δ)`, we obtain a closure `c'` such that `δ ⊢ N ⇓ c'` and `𝕍 v c'`. We conclude that `γ' ⊢ L · M ⇓ c'` by rule `⇓-app`. @@ -553,11 +553,11 @@ kth-x{γ' = γ'}{x = x} with γ' x but we must first show that `𝔾 (γ , v) (γ' , c)`. We prove that by the lemma `𝔾-ext`, using facts `𝔾 γ γ'` and `𝔼 v c`. -* Case `⊥-intro`. We have the premise `AboveFun ⊥`, but that's impossible. +* Case `⊥-intro`. We have the premise `above-fun ⊥`, but that's impossible. -* Case `⊔-intro`. We have `γ ⊢ M ↓ (v₁ ⊔ v₂)` and `AboveFun (v₁ ⊔ v₂)` +* Case `⊔-intro`. We have `γ ⊢ M ↓ (v₁ ⊔ v₂)` and `above-fun (v₁ ⊔ v₂)` and need to show `γ' ⊢ M ↓ c` and `𝕍 (v₁ ⊔ v₂) c` for some `c`. - Again, by `AboveFun-⊔`, at least one of `v₁` or `v₂` is greater than + Again, by `above-fun-⊔`, at least one of `v₁` or `v₂` is greater than a function. * Suppose both `v₁` and `v₂` are greater than a function value. @@ -573,9 +573,9 @@ kth-x{γ' = γ'}{x = x} with γ' x Then because `v₂` is not greater than a function, we also have `𝕍 v₂ (clos (ƛ N) γ₁)`. We conclude that `𝕍 (v₁ ⊔ v₂) (clos (ƛ N) γ₁)`. -* Case `sub`. We have `γ ⊢ M ↓ v`, `v' ⊑ v`, and `AboveFun v'`. +* Case `sub`. We have `γ ⊢ M ↓ v`, `v' ⊑ v`, and `above-fun v'`. We need to show that `γ' ⊢ M ⇓ c` and `𝕍 v' c` for some `c`. - We have `AboveFun v` by `AboveFun-⊑`, + We have `above-fun v` by `above-fun-⊑`, so the induction hypothesis for `γ ⊢ M ↓ v` gives us a closure `c` such that `γ' ⊢ M ⇓ c` and `𝕍 v c`. We conclude that `𝕍 v' c` by `sub-𝕍`. @@ -593,7 +593,7 @@ adequacy : ∀{M : ∅ ⊢ ★}{N : ∅ , ★ ⊢ ★} → ℰ M ≃ ℰ (ƛ N ∅' ⊢ M ⇓ clos (ƛ N′) γ adequacy{M}{N} eq with ↓→𝔼 𝔾-∅ ((proj₂ (eq `∅ (⊥ ↦ ⊥))) (↦-intro ⊥-intro)) - ⟨ ⊥ , ⟨ ⊥ , Refl⊑ ⟩ ⟩ + ⟨ ⊥ , ⟨ ⊥ , ⊑-refl ⟩ ⟩ ... | ⟨ clos {Γ} M′ γ , ⟨ M⇓c , Vc ⟩ ⟩ with 𝕍→WHNF Vc ... | ƛ_ {N = N′} = diff --git a/src/plfa/part3/Compositional.lagda.md b/src/plfa/part3/Compositional.lagda.md index be413aae..9982fda2 100644 --- a/src/plfa/part3/Compositional.lagda.md +++ b/src/plfa/part3/Compositional.lagda.md @@ -35,7 +35,7 @@ open import plfa.part2.Untyped using (Context; _,_; ★; _∋_; _⊢_; `_; ƛ_; _·_) open import plfa.part3.Denotational using (Value; _↦_; _`,_; _⊔_; ⊥; _⊑_; _⊢_↓_; - Bot⊑; Fun⊑; ConjL⊑; ConjR1⊑; ConjR2⊑; Dist⊑; Refl⊑; Trans⊑; Dist⊔↦⊔; + ⊑-bot; ⊑-fun; ⊑-conj-L; ⊑-conj-R1; ⊑-conj-R2; ⊑-dist; ⊑-refl; ⊑-trans; ⊔↦⊔-dist; var; ↦-intro; ↦-elim; ⊔-intro; ⊥-intro; sub; up-env; ℰ; _≃_; ≃-sym; Denotation; Env) open plfa.part3.Denotational.≃-Reasoning @@ -63,8 +63,11 @@ rules `↦-intro`, `⊥-intro`, and `⊔-intro`. ℱ D γ (u ⊔ v) = (ℱ D γ u) × (ℱ D γ v) ``` -[JGS: add comment about how ℱ can be viewed as curry.] - +If one squints hard enough, the `ℱ` function starts to look like the +`curry` operation familar to functional programmers. It turns a +function that expects a tuple of length `n + 1` (the environment `Γ , +★`) into a function that expects a tuple of length `n` and returns a +function of one parameter. Using this `ℱ`, we hope to prove that @@ -73,7 +76,7 @@ Using this `ℱ`, we hope to prove that The function `ℱ` is preserved when going from a larger value `v` to a smaller value `u`. The proof is a straightforward induction on the derivation of `u ⊑ v`, using the `up-env` lemma in the case for the -`Fun⊑` rule. +`⊑-fun` rule. ``` sub-ℱ : ∀{Γ}{N : Γ , ★ ⊢ ★}{γ v u} @@ -81,14 +84,14 @@ sub-ℱ : ∀{Γ}{N : Γ , ★ ⊢ ★}{γ v u} → u ⊑ v ------------ → ℱ (ℰ N) γ u -sub-ℱ d Bot⊑ = tt -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 -sub-ℱ {v = v₁ ↦ v₂ ⊔ v₁ ↦ v₃} {v₁ ↦ (v₂ ⊔ v₃)} ⟨ N2 , N3 ⟩ Dist⊑ = +sub-ℱ d ⊑-bot = tt +sub-ℱ d (⊑-fun lt lt′) = sub (up-env d lt) lt′ +sub-ℱ d (⊑-conj-L lt lt₁) = ⟨ sub-ℱ d lt , sub-ℱ d lt₁ ⟩ +sub-ℱ d (⊑-conj-R1 lt) = sub-ℱ (proj₁ d) lt +sub-ℱ d (⊑-conj-R2 lt) = sub-ℱ (proj₂ d) lt +sub-ℱ {v = v₁ ↦ v₂ ⊔ v₁ ↦ v₃} {v₁ ↦ (v₂ ⊔ v₃)} ⟨ N2 , N3 ⟩ ⊑-dist = ⊔-intro N2 N3 -sub-ℱ d (Trans⊑ x₁ x₂) = sub-ℱ (sub-ℱ d x₂) x₁ +sub-ℱ d (⊑-trans x₁ x₂) = sub-ℱ (sub-ℱ d x₂) x₁ ``` [PLW: @@ -164,7 +167,7 @@ because, for example, the rule `↦-elim` applies to any value. Instead we shall define `●` in a way that directly deals with the `↦-elim` and `⊥-intro` rules but ignores `⊔-intro`. This makes the forward direction of the proof more difficult, and the case for `⊔-intro` -demonstrates why the `Dist⊑` rule is important. +demonstrates why the `⊑-dist` rule is important. So we define the application of `D₁` to `D₂`, written `D₁ ● D₂`, to include any value `w` equivalent to `⊥`, for the `⊥-intro` rule, and to include any @@ -178,7 +181,9 @@ _●_ : ∀{Γ} → Denotation Γ → Denotation Γ → Denotation Γ (D₁ ● D₂) γ w = w ⊑ ⊥ ⊎ Σ[ v ∈ Value ]( D₁ γ (v ↦ w) × D₂ γ v ) ``` -[JGS: add comment about how ● can be viewed as apply.] +If one squints hard enough, the `_●_` operator starts to look +like the `apply` operation familiar to functional programmers. +It takes two parameters and applies the first to the second. Next we consider the inversion lemma for application, which is also the forward direction of the semantic equation for application. We @@ -190,28 +195,28 @@ describe the proof below. ---------------- → (ℰ L ● ℰ M) γ v ℰ·→●ℰ (↦-elim{v = v′} d₁ d₂) = inj₂ ⟨ v′ , ⟨ d₁ , d₂ ⟩ ⟩ -ℰ·→●ℰ {v = ⊥} ⊥-intro = inj₁ Bot⊑ +ℰ·→●ℰ {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₁ lt2 = inj₁ (⊑-conj-L 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₂ - lt = (Fun⊑ Refl⊑ (ConjL⊑ (Trans⊑ lt1 Bot⊑) Refl⊑)) + lt = (⊑-fun ⊑-refl (⊑-conj-L (⊑-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₁ - lt = (Fun⊑ Refl⊑ (ConjL⊑ Refl⊑ (Trans⊑ lt2 Bot⊑))) + lt = (⊑-fun ⊑-refl (⊑-conj-L ⊑-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 + let x = inj₂ ⟨ v₁′ ⊔ v₁′′ , ⟨ sub L↓⊔ ⊔↦⊔-dist , M↓⊔ ⟩ ⟩ in x ℰ·→●ℰ {Γ}{γ}{L}{M}{v} (sub d lt) with ℰ·→●ℰ d -... | inj₁ lt2 = inj₁ (Trans⊑ lt lt2) +... | inj₁ lt2 = inj₁ (⊑-trans lt lt2) ... | inj₂ ⟨ v₁ , ⟨ L↓v12 , M↓v3 ⟩ ⟩ = - inj₂ ⟨ v₁ , ⟨ sub L↓v12 (Fun⊑ Refl⊑ lt) , M↓v3 ⟩ ⟩ + inj₂ ⟨ v₁ , ⟨ sub L↓v12 (⊑-fun ⊑-refl lt) , M↓v3 ⟩ ⟩ ``` We proceed by induction on the semantics. @@ -243,7 +248,7 @@ We proceed by induction on the semantics. `L` must be an `↦` whose input entry is `v₁′ ⊔ v₁′′`. So we use the `sub` rule to obtain `γ ⊢ L ↓ (v₁′ ⊔ v₁′′) ↦ (v₁ ⊔ v₂)`, - using the `Dist⊔→⊔` lemma (thanks to the `Dist⊑` rule) to + using the `⊔↦⊔-dist` lemma (thanks to the `⊑-dist` rule) to show that (v₁′ ⊔ v₁′′) ↦ (v₁ ⊔ v₂) ⊑ (v₁′ ↦ v₂) ⊔ (v₁′′ ↦ v₁) @@ -291,10 +296,10 @@ var-inv : ∀ {Γ v x} {γ : Env Γ} → ℰ (` x) γ v ------------------- → v ⊑ γ x -var-inv (var) = Refl⊑ -var-inv (⊔-intro d₁ d₂) = ConjL⊑ (var-inv d₁) (var-inv d₂) -var-inv (sub d lt) = Trans⊑ lt (var-inv d) -var-inv ⊥-intro = Bot⊑ +var-inv (var) = ⊑-refl +var-inv (⊔-intro d₁ d₂) = ⊑-conj-L (var-inv d₁) (var-inv d₂) +var-inv (sub d lt) = ⊑-trans lt (var-inv d) +var-inv ⊥-intro = ⊑-bot ``` To round-out the semantic equations, we establish the following one @@ -422,24 +427,24 @@ terms that result from filling the hole. ``` data Ctx : Context → Context → Set where - CHole : ∀{Γ} → Ctx Γ Γ - CLam : ∀{Γ Δ} → Ctx (Γ , ★) (Δ , ★) → Ctx (Γ , ★) Δ - CAppL : ∀{Γ Δ} → Ctx Γ Δ → Δ ⊢ ★ → Ctx Γ Δ - CAppR : ∀{Γ Δ} → Δ ⊢ ★ → Ctx Γ Δ → Ctx Γ Δ + ctx-hole : ∀{Γ} → Ctx Γ Γ + ctx-lam : ∀{Γ Δ} → Ctx (Γ , ★) (Δ , ★) → Ctx (Γ , ★) Δ + ctx-app-L : ∀{Γ Δ} → Ctx Γ Δ → Δ ⊢ ★ → Ctx Γ Δ + ctx-app-R : ∀{Γ Δ} → Δ ⊢ ★ → Ctx Γ Δ → Ctx Γ Δ ``` -* The constructor `CHole` represents the hole, and in this case the +* The constructor `ctx-hole` represents the hole, and in this case the variable context for the hole is the same as the variable context for the term that results from filling the hole. -* The constructor `CLam` takes a `Ctx` and produces a larger one that +* The constructor `ctx-lam` takes a `Ctx` and produces a larger one that adds a lambda abstraction at the top. The variable context of the hole stays the same, whereas we remove one variable from the context of the resulting term because it is bound by this lambda abstraction. -* There are two constructions for application, `CAppL` and - `CAppR`. The `CAppL` is for when the hole is inside the left-hand +* There are two constructions for application, `ctx-app-L` and + `ctx-app-R`. The `ctx-app-L` is for when the hole is inside the left-hand term (the operator) and the later is when the hole is inside the right-hand term (the operand). @@ -448,10 +453,10 @@ following `plug` function. It is defined by recursion on the context. ``` plug : ∀{Γ}{Δ} → Ctx Γ Δ → Γ ⊢ ★ → Δ ⊢ ★ -plug CHole M = M -plug (CLam C) N = ƛ plug C N -plug (CAppL C N) L = (plug C L) · N -plug (CAppR L C) M = L · (plug C M) +plug ctx-hole M = M +plug (ctx-lam C) N = ƛ plug C N +plug (ctx-app-L C N) L = (plug C L) · N +plug (ctx-app-R L C) M = L · (plug C M) ``` We are ready to state and prove the compositionality principle. Given @@ -464,13 +469,13 @@ compositionality : ∀{Γ Δ}{C : Ctx Γ Δ} {M N : Γ ⊢ ★} → ℰ M ≃ ℰ N --------------------------- → ℰ (plug C M) ≃ ℰ (plug C N) -compositionality {C = CHole} M≃N = +compositionality {C = ctx-hole} M≃N = M≃N -compositionality {C = CLam C′} M≃N = +compositionality {C = ctx-lam C′} M≃N = lam-cong (compositionality {C = C′} M≃N) -compositionality {C = CAppL C′ L} M≃N = +compositionality {C = ctx-app-L C′ L} M≃N = app-cong (compositionality {C = C′} M≃N) λ γ v → ⟨ (λ x → x) , (λ x → x) ⟩ -compositionality {C = CAppR L C′} M≃N = +compositionality {C = ctx-app-R L C′} M≃N = app-cong (λ γ v → ⟨ (λ x → x) , (λ x → x) ⟩) (compositionality {C = C′} M≃N) ``` diff --git a/src/plfa/part3/Denotational.lagda.md b/src/plfa/part3/Denotational.lagda.md index e6c687f4..34b672db 100644 --- a/src/plfa/part3/Denotational.lagda.md +++ b/src/plfa/part3/Denotational.lagda.md @@ -101,7 +101,7 @@ data Value : Set where The `⊑` relation adapts the familiar notion of subset to the Value data type. This relation plays the key role in enabling self-application. -There are two rules that are specific to functions, `Fun⊑` and `Dist⊑`, +There are two rules that are specific to functions, `⊑-fun` and `⊑-dist`, which we discuss below. ``` @@ -109,59 +109,59 @@ infix 4 _⊑_ data _⊑_ : Value → Value → Set where - Bot⊑ : ∀ {v} → ⊥ ⊑ v + ⊑-bot : ∀ {v} → ⊥ ⊑ v - ConjL⊑ : ∀ {u v w} + ⊑-conj-L : ∀ {u v w} → v ⊑ u → w ⊑ u ----------- → (v ⊔ w) ⊑ u - ConjR1⊑ : ∀ {u v w} + ⊑-conj-R1 : ∀ {u v w} → u ⊑ v ----------- → u ⊑ (v ⊔ w) - ConjR2⊑ : ∀ {u v w} + ⊑-conj-R2 : ∀ {u v w} → u ⊑ w ----------- → u ⊑ (v ⊔ w) - Trans⊑ : ∀ {u v w} + ⊑-trans : ∀ {u v w} → u ⊑ v → v ⊑ w ----- → u ⊑ w - Fun⊑ : ∀ {v w v′ w′} + ⊑-fun : ∀ {v w v′ w′} → v′ ⊑ v → w ⊑ w′ ------------------- → (v ↦ w) ⊑ (v′ ↦ w′) - Dist⊑ : ∀{v w w′} + ⊑-dist : ∀{v w w′} --------------------------------- → v ↦ (w ⊔ w′) ⊑ (v ↦ w) ⊔ (v ↦ w′) ``` The first five rules are straightforward. -The rule `Fun⊑` captures when it is OK to match a higher-order argument +The rule `⊑-fun` captures when it is OK to match a higher-order argument `v′ ↦ w′` to a table entry whose input is `v ↦ w`. Considering a call to the higher-order argument. It is OK to pass a larger argument than expected, so `v` can be larger than `v′`. Also, it is OK to disregard some of the output, so `w` can be smaller than `w′`. -The rule `Dist⊑` says that if you have two entries for the same input, +The rule `⊑-dist` says that if you have two entries for the same input, then you can combine them into a single entry and joins the two outputs. The `⊑` relation is reflexive. ``` -Refl⊑ : ∀ {v} → v ⊑ v -Refl⊑ {⊥} = Bot⊑ -Refl⊑ {v ↦ v′} = Fun⊑ Refl⊑ Refl⊑ -Refl⊑ {v₁ ⊔ v₂} = ConjL⊑ (ConjR1⊑ Refl⊑) (ConjR2⊑ Refl⊑) +⊑-refl : ∀ {v} → v ⊑ v +⊑-refl {⊥} = ⊑-bot +⊑-refl {v ↦ v′} = ⊑-fun ⊑-refl ⊑-refl +⊑-refl {v₁ ⊔ v₂} = ⊑-conj-L (⊑-conj-R1 ⊑-refl) (⊑-conj-R2 ⊑-refl) ``` The `⊔` operation is monotonic with respect to `⊑`, that is, given two @@ -172,19 +172,19 @@ larger values it produces a larger value. → v ⊑ v′ → w ⊑ w′ ----------------------- → (v ⊔ w) ⊑ (v′ ⊔ w′) -⊔⊑⊔ d₁ d₂ = ConjL⊑ (ConjR1⊑ d₁) (ConjR2⊑ d₂) +⊔⊑⊔ d₁ d₂ = ⊑-conj-L (⊑-conj-R1 d₁) (⊑-conj-R2 d₂) ``` -The `Dist⊑` rule can be used to combine two entries even when the +The `⊑-dist` rule can be used to combine two entries even when the input values are not identical. One can first combine the two inputs -using ⊔ and then apply the `Dist⊑` rule to obtain the following +using ⊔ and then apply the `⊑-dist` rule to obtain the following property. ``` -Dist⊔↦⊔ : ∀{v v′ w w′ : Value} +⊔↦⊔-dist : ∀{v v′ w w′ : Value} → (v ⊔ v′) ↦ (w ⊔ w′) ⊑ (v ↦ w) ⊔ (v′ ↦ w′) -Dist⊔↦⊔ = Trans⊑ Dist⊑ (⊔⊑⊔ (Fun⊑ (ConjR1⊑ Refl⊑) Refl⊑) - (Fun⊑ (ConjR2⊑ Refl⊑) Refl⊑)) +⊔↦⊔-dist = ⊑-trans ⊑-dist (⊔⊑⊔ (⊑-fun (⊑-conj-R1 ⊑-refl) ⊑-refl) + (⊑-fun (⊑-conj-R2 ⊑-refl) ⊑-refl)) ``` @@ -197,19 +197,19 @@ then both `u` and `v` are less than `w`. → u ⊔ v ⊑ w --------- → u ⊑ w -⊔⊑-invL (ConjL⊑ lt1 lt2) = lt1 -⊔⊑-invL (ConjR1⊑ lt) = ConjR1⊑ (⊔⊑-invL lt) -⊔⊑-invL (ConjR2⊑ lt) = ConjR2⊑ (⊔⊑-invL lt) -⊔⊑-invL (Trans⊑ lt1 lt2) = Trans⊑ (⊔⊑-invL lt1) lt2 +⊔⊑-invL (⊑-conj-L lt1 lt2) = lt1 +⊔⊑-invL (⊑-conj-R1 lt) = ⊑-conj-R1 (⊔⊑-invL lt) +⊔⊑-invL (⊑-conj-R2 lt) = ⊑-conj-R2 (⊔⊑-invL lt) +⊔⊑-invL (⊑-trans lt1 lt2) = ⊑-trans (⊔⊑-invL lt1) lt2 ⊔⊑-invR : ∀{u v w : Value} → u ⊔ v ⊑ w --------- → v ⊑ w -⊔⊑-invR (ConjL⊑ lt1 lt2) = lt2 -⊔⊑-invR (ConjR1⊑ lt) = ConjR1⊑ (⊔⊑-invR lt) -⊔⊑-invR (ConjR2⊑ lt) = ConjR2⊑ (⊔⊑-invR lt) -⊔⊑-invR (Trans⊑ lt1 lt2) = Trans⊑ (⊔⊑-invR lt1) lt2 +⊔⊑-invR (⊑-conj-L lt1 lt2) = lt2 +⊔⊑-invR (⊑-conj-R1 lt) = ⊑-conj-R1 (⊔⊑-invR lt) +⊔⊑-invR (⊑-conj-R2 lt) = ⊑-conj-R2 (⊔⊑-invR lt) +⊔⊑-invR (⊑-trans lt1 lt2) = ⊑-trans (⊔⊑-invR lt1) lt2 ``` @@ -279,19 +279,19 @@ _`⊔_ : ∀ {Γ} → Env Γ → Env Γ → Env Γ (γ `⊔ δ) x = γ x ⊔ δ x ``` -The `Refl⊑`, `ConjR1⊑`, and `ConjR2⊑` rules lift to environments. So +The `⊑-refl`, `⊑-conj-R1`, and `⊑-conj-R2` rules lift to environments. So the join of two environments `γ` and `δ` is greater than the first environment `γ` or the second environment `δ`. ``` -`Refl⊑ : ∀ {Γ} {γ : Env Γ} → γ `⊑ γ -`Refl⊑ {Γ} {γ} x = Refl⊑ {γ x} +`⊑-refl : ∀ {Γ} {γ : Env Γ} → γ `⊑ γ +`⊑-refl {Γ} {γ} x = ⊑-refl {γ x} -EnvConjR1⊑ : ∀ {Γ} → (γ : Env Γ) → (δ : Env Γ) → γ `⊑ (γ `⊔ δ) -EnvConjR1⊑ γ δ x = ConjR1⊑ Refl⊑ +⊑-env-conj-R1 : ∀ {Γ} → (γ : Env Γ) → (δ : Env Γ) → γ `⊑ (γ `⊔ δ) +⊑-env-conj-R1 γ δ x = ⊑-conj-R1 ⊑-refl -EnvConjR2⊑ : ∀ {Γ} → (γ : Env Γ) → (δ : Env Γ) → δ `⊑ (γ `⊔ δ) -EnvConjR2⊑ γ δ x = ConjR2⊑ Refl⊑ +⊑-env-conj-R2 : ∀ {Γ} → (γ : Env Γ) → (δ : Env Γ) → δ `⊑ (γ `⊔ δ) +⊑-env-conj-R2 γ δ x = ⊑-conj-R2 ⊑-refl ``` ## Denotational Semantics @@ -411,7 +411,7 @@ we'll name `v`. Then for the second application, it must map `v` to some value. Let's name it `w`. So the parameter's table must contain two entries, both `u ↦ v` and `v ↦ w`. For each application of the table, we extract the appropriate entry from it using the `sub` rule. -In particular, we use the ConjR1⊑ and ConjR2⊑ to select `u ↦ v` and `v +In particular, we use the ⊑-conj-R1 and ⊑-conj-R2 to select `u ↦ v` and `v ↦ w`, respectively, from the table `u ↦ v ⊔ v ↦ w`. So the meaning of twoᶜ is that it takes this table and parameter `u`, and it returns `w`. Indeed we derive this as follows. @@ -421,10 +421,10 @@ denot-twoᶜ : ∀{u v w : Value} → `∅ ⊢ twoᶜ ↓ ((u ↦ v ⊔ v ↦ w) denot-twoᶜ {u}{v}{w} = ↦-intro (↦-intro (↦-elim (sub var lt1) (↦-elim (sub var lt2) var))) where lt1 : v ↦ w ⊑ u ↦ v ⊔ v ↦ w - lt1 = ConjR2⊑ (Fun⊑ Refl⊑ Refl⊑) + lt1 = ⊑-conj-R2 (⊑-fun ⊑-refl ⊑-refl) lt2 : u ↦ v ⊑ u ↦ v ⊔ v ↦ w - lt2 = (ConjR1⊑ (Fun⊑ Refl⊑ Refl⊑)) + lt2 = (⊑-conj-R1 (⊑-fun ⊑-refl ⊑-refl)) ``` @@ -441,8 +441,8 @@ and then the result of the application is `w`. Δ = (ƛ (# 0) · (# 0)) denot-Δ : ∀ {v w} → `∅ ⊢ Δ ↓ ((v ↦ w ⊔ v) ↦ w) -denot-Δ = ↦-intro (↦-elim (sub var (ConjR1⊑ Refl⊑)) - (sub var (ConjR2⊑ Refl⊑))) +denot-Δ = ↦-intro (↦-elim (sub var (⊑-conj-R1 ⊑-refl)) + (sub var (⊑-conj-R2 ⊑-refl))) ``` One might worry whether this semantics can deal with diverging @@ -492,11 +492,11 @@ arguments. ``` ↦-elim2 : ∀ {Γ} {γ : Env Γ} {M₁ M₂ v₁ v₂ v₃} - → γ ⊢ M₁ ↓ (v₁ ↦ v₃) - → γ ⊢ M₂ ↓ v₂ - → v₁ ⊑ v₂ - ------------------ - → γ ⊢ (M₁ · M₂) ↓ v₃ + → γ ⊢ M₁ ↓ (v₁ ↦ v₃) + → γ ⊢ M₂ ↓ v₂ + → v₁ ⊑ v₂ + ------------------ + → γ ⊢ (M₁ · M₂) ↓ v₃ ↦-elim2 d₁ d₂ lt = ↦-elim d₁ (sub d₂ lt) ``` @@ -706,7 +706,7 @@ ext-nth : ∀ {Γ Δ v} {γ : Env Γ} {δ : Env Δ} → γ `⊑ (δ ∘ ρ) ------------------------------ → (γ `, v) `⊑ ((δ `, v) ∘ ext ρ) -ext-nth ρ lt Z = Refl⊑ +ext-nth ρ lt Z = ⊑-refl ext-nth ρ lt (S n′) = lt n′ ``` @@ -766,19 +766,19 @@ which gives us `δ ⊢ rename (λ {A} x → x) M ↓ v`, and then we apply the `rename-id` lemma to obtain `δ ⊢ M ↓ v`. ``` -Env⊑ : ∀ {Γ} {γ : Env Γ} {δ : Env Γ} {M v} +⊑-env : ∀ {Γ} {γ : Env Γ} {δ : Env Γ} {M v} → γ ⊢ M ↓ v → γ `⊑ δ ---------- → δ ⊢ M ↓ v -Env⊑{Γ}{γ}{δ}{M}{v} d lt +⊑-env{Γ}{γ}{δ}{M}{v} d lt with rename-pres{Γ}{Γ}{v}{γ}{δ}{M} (λ {A} x → x) lt d ... | d′ rewrite rename-id {Γ}{★}{M} = d′ ``` In the proof that substitution reflects denotations, in the case for -lambda abstraction, we use a minor variation of `Env⊑`, in which just +lambda abstraction, we use a minor variation of `⊑-env`, in which just the last element of the environment gets larger. ``` @@ -787,11 +787,11 @@ up-env : ∀ {Γ} {γ : Env Γ} {M v u₁ u₂} → u₁ ⊑ u₂ ----------------- → (γ `, u₂) ⊢ M ↓ v -up-env d lt = Env⊑ d (nth-le lt) +up-env d lt = ⊑-env d (nth-le lt) where nth-le : ∀ {γ u₁ u₂} → u₁ ⊑ u₂ → (γ `, u₁) `⊑ (γ `, u₂) nth-le lt Z = lt - nth-le lt (S n) = Refl⊑ + nth-le lt (S n) = ⊑-refl ``` @@ -800,10 +800,10 @@ up-env d lt = Env⊑ d (nth-le lt) What can we deduce from knowing that a function `v ↦ w` is less than some value `u`? What can we deduce about `u`? The answer to this question is called the inversion property of less-than for functions. -This question is not easy to answer because of the `Dist⊑` rule, which +This question is not easy to answer because of the `⊑-dist` rule, which relates a function on the left to a pair of functions on the right. So `u` may include several functions that, as a group, relate to -`v ↦ w`. Furthermore, because of the rules `ConjR1⊑` and `ConjR2⊑`, +`v ↦ w`. Furthermore, because of the rules `⊑-conj-R1` and `⊑-conj-R2`, there may be other values inside `u`, such as `⊥`, that have nothing to do with `v ↦ w`. But in general, we can deduce that `u` includes a collection of functions where the join of their domains is less @@ -852,20 +852,20 @@ imply the less-than relation but not the other way around. → u ∈ v ----- → u ⊑ v -∈→⊑ {.⊥} {⊥} refl = Bot⊑ -∈→⊑ {v ↦ w} {v ↦ w} refl = Refl⊑ -∈→⊑ {u} {v ⊔ w} (inj₁ x) = ConjR1⊑ (∈→⊑ x) -∈→⊑ {u} {v ⊔ w} (inj₂ y) = ConjR2⊑ (∈→⊑ y) +∈→⊑ {.⊥} {⊥} refl = ⊑-bot +∈→⊑ {v ↦ w} {v ↦ w} refl = ⊑-refl +∈→⊑ {u} {v ⊔ w} (inj₁ x) = ⊑-conj-R1 (∈→⊑ x) +∈→⊑ {u} {v ⊔ w} (inj₂ y) = ⊑-conj-R2 (∈→⊑ y) ⊆→⊑ : ∀{u v : Value} → u ⊆ v ----- → u ⊑ v ⊆→⊑ {⊥} s with s {⊥} refl -... | x = Bot⊑ +... | x = ⊑-bot ⊆→⊑ {u ↦ u′} s with s {u ↦ u′} refl ... | x = ∈→⊑ x -⊆→⊑ {u ⊔ u′} s = ConjL⊑ (⊆→⊑ (λ z → s (inj₁ z))) (⊆→⊑ (λ z → s (inj₂ z))) +⊆→⊑ {u ⊔ u′} s = ⊑-conj-L (⊆→⊑ (λ z → s (inj₁ z))) (⊆→⊑ (λ z → s (inj₂ z))) ``` We shall also need some inversion principles for value inclusion. If @@ -897,15 +897,15 @@ then `v ↦ w` must be a member of `u`. To identify collections of functions, we define the following two predicates. We write `Fun u` if `u` is a function value, that is, if -`u ≡ v ↦ w` for some values `v` and `w`. We write `Funs v` if all the elements +`u ≡ v ↦ w` for some values `v` and `w`. We write `all-funs v` if all the elements of `v` are functions. ``` data Fun : Value → Set where fun : ∀{u v w} → u ≡ (v ↦ w) → Fun u -Funs : Value → Set -Funs v = ∀{u} → u ∈ v → Fun u +all-funs : Value → Set +all-funs v = ∀{u} → u ∈ v → Fun u ``` The value `⊥` is not a function. @@ -920,14 +920,14 @@ one element. Thus, if all the elements are functions, there is at least one that is a function. ``` -Funs∈ : ∀{u} - → Funs u +all-funs∈ : ∀{u} + → all-funs u → Σ[ v ∈ Value ] Σ[ w ∈ Value ] v ↦ w ∈ u -Funs∈ {⊥} f with f {⊥} refl +all-funs∈ {⊥} f with f {⊥} refl ... | fun () -Funs∈ {v ↦ w} f = ⟨ v , ⟨ w , refl ⟩ ⟩ -Funs∈ {u ⊔ u′} f - with Funs∈ λ z → f (inj₁ z) +all-funs∈ {v ↦ w} f = ⟨ v , ⟨ w , refl ⟩ ⟩ +all-funs∈ {u ⊔ u′} f + with all-funs∈ λ z → f (inj₁ z) ... | ⟨ v , ⟨ w , m ⟩ ⟩ = ⟨ v , ⟨ w , (inj₁ m) ⟩ ⟩ ``` @@ -961,7 +961,7 @@ that `v` is included in the domain of `v`. ``` ↦∈→⊆dom : ∀{u v w : Value} - → Funs u → (v ↦ w) ∈ u + → all-funs u → (v ↦ w) ∈ u ---------------------- → v ⊆ dom u ↦∈→⊆dom {⊥} fg () u∈v @@ -1000,7 +1000,7 @@ than `w`. ``` factor : (u : Value) → (u′ : Value) → (v : Value) → (w : Value) → Set -factor u u′ v w = Funs u′ × u′ ⊆ u × dom u′ ⊑ v × w ⊑ cod u′ +factor u u′ v w = all-funs u′ × u′ ⊆ u × dom u′ ⊑ v × w ⊑ cod u′ ``` We prove the inversion principle for functions by induction on the @@ -1010,17 +1010,17 @@ u`), and strengthen the conclusion to say that for _every_ function value `v ↦ w ∈ u₁`, we have that `v ↦ w` factors `u₂` into some value `u₃`. -### Inversion of less-than for functions, the case for Trans⊑ +### Inversion of less-than for functions, the case for ⊑-trans -The crux of the proof is the case for `Trans⊑`. +The crux of the proof is the case for `⊑-trans`. u₁ ⊑ u u ⊑ u₂ - --------------- (Trans⊑) + --------------- (⊑-trans) u₁ ⊑ u₂ By the induction hypothesis for `u₁ ⊑ u`, we know that `v ↦ w factors u into u′`, for some value `u′`, -so we have `Funs u′` and `u′ ⊆ u`. +so we have `all-funs u′` and `u′ ⊆ u`. By the induction hypothesis for `u ⊑ u₂`, we know that for any `v′ ↦ w′ ∈ u`, `v′ ↦ w′` factors `u₂` into `u₃`. With these facts in hand, we proceed by induction on `u′` @@ -1029,7 +1029,7 @@ We discuss each case of the proof in the text below. ``` sub-inv-trans : ∀{u′ u₂ u : Value} - → Funs u′ → u′ ⊆ u + → all-funs u′ → u′ ⊆ u → (∀{v′ w′} → v′ ↦ w′ ∈ u → Σ[ u₃ ∈ Value ] factor u₂ u₃ v′ w′) --------------------------------------------------------------- → Σ[ u₃ ∈ Value ] factor u₂ u₃ (dom u′) (cod u′) @@ -1063,7 +1063,7 @@ sub-inv-trans {u₁′ ⊔ u₂′} {u₂} {u} fg u′⊆u IH `dom u′ ≡ u₁′` and `cod u′ ≡ u₂′`. * Suppose `u′ ≡ u₁′ ⊔ u₂′`. Then we have `u₁′ ⊆ u` and `u₂′ ⊆ u`. We also - have `Funs u₁′` and `Funs u₂′`, so we can apply the induction hypothesis + have `all-funs u₁′` and `all-funs u₂′`, so we can apply the induction hypothesis for both `u₁′` and `u₂′`. So there exists values `u₃₁` and `u₃₂` such that `(dom u₁′) ↦ (cod u₁′)` factors `u` into `u₃₁` and `(dom u₂′) ↦ (cod u₂′)` factors `u` into `u₃₂`. @@ -1091,32 +1091,32 @@ sub-inv : ∀{u₁ u₂ : Value} → ∀{v w} → v ↦ w ∈ u₁ ------------------------------------- → Σ[ u₃ ∈ Value ] factor u₂ u₃ v w -sub-inv {⊥} {u₂} Bot⊑ {v} {w} () -sub-inv {u₁₁ ⊔ u₁₂} {u₂} (ConjL⊑ lt1 lt2) {v} {w} (inj₁ x) = sub-inv lt1 x -sub-inv {u₁₁ ⊔ u₁₂} {u₂} (ConjL⊑ lt1 lt2) {v} {w} (inj₂ y) = sub-inv lt2 y -sub-inv {u₁} {u₂₁ ⊔ u₂₂} (ConjR1⊑ lt) {v} {w} m +sub-inv {⊥} {u₂} ⊑-bot {v} {w} () +sub-inv {u₁₁ ⊔ u₁₂} {u₂} (⊑-conj-L lt1 lt2) {v} {w} (inj₁ x) = sub-inv lt1 x +sub-inv {u₁₁ ⊔ u₁₂} {u₂} (⊑-conj-L lt1 lt2) {v} {w} (inj₂ y) = sub-inv lt2 y +sub-inv {u₁} {u₂₁ ⊔ u₂₂} (⊑-conj-R1 lt) {v} {w} m with sub-inv lt m ... | ⟨ u₃₁ , ⟨ fu₃₁ , ⟨ u₃₁⊆u₂₁ , ⟨ domu₃₁⊑v , w⊑codu₃₁ ⟩ ⟩ ⟩ ⟩ = ⟨ u₃₁ , ⟨ fu₃₁ , ⟨ (λ {w} z → inj₁ (u₃₁⊆u₂₁ z)) , ⟨ domu₃₁⊑v , w⊑codu₃₁ ⟩ ⟩ ⟩ ⟩ -sub-inv {u₁} {u₂₁ ⊔ u₂₂} (ConjR2⊑ lt) {v} {w} m +sub-inv {u₁} {u₂₁ ⊔ u₂₂} (⊑-conj-R2 lt) {v} {w} m with sub-inv lt m ... | ⟨ u₃₂ , ⟨ fu₃₂ , ⟨ u₃₂⊆u₂₂ , ⟨ domu₃₂⊑v , w⊑codu₃₂ ⟩ ⟩ ⟩ ⟩ = ⟨ u₃₂ , ⟨ fu₃₂ , ⟨ (λ {C} z → inj₂ (u₃₂⊆u₂₂ z)) , ⟨ domu₃₂⊑v , w⊑codu₃₂ ⟩ ⟩ ⟩ ⟩ -sub-inv {u₁} {u₂} (Trans⊑{v = u} u₁⊑u u⊑u₂) {v} {w} v↦w∈u₁ +sub-inv {u₁} {u₂} (⊑-trans{v = u} u₁⊑u u⊑u₂) {v} {w} v↦w∈u₁ with sub-inv u₁⊑u v↦w∈u₁ ... | ⟨ u′ , ⟨ fu′ , ⟨ u′⊆u , ⟨ domu′⊑v , w⊑codu′ ⟩ ⟩ ⟩ ⟩ with sub-inv-trans {u′} fu′ u′⊆u (sub-inv u⊑u₂) ... | ⟨ u₃ , ⟨ fu₃ , ⟨ u₃⊆u₂ , ⟨ domu₃⊑domu′ , codu′⊑codu₃ ⟩ ⟩ ⟩ ⟩ = - ⟨ u₃ , ⟨ fu₃ , ⟨ u₃⊆u₂ , ⟨ Trans⊑ domu₃⊑domu′ domu′⊑v , - Trans⊑ w⊑codu′ codu′⊑codu₃ ⟩ ⟩ ⟩ ⟩ -sub-inv {u₁₁ ↦ u₁₂} {u₂₁ ↦ u₂₂} (Fun⊑ lt1 lt2) refl = + ⟨ u₃ , ⟨ fu₃ , ⟨ u₃⊆u₂ , ⟨ ⊑-trans domu₃⊑domu′ domu′⊑v , + ⊑-trans w⊑codu′ codu′⊑codu₃ ⟩ ⟩ ⟩ ⟩ +sub-inv {u₁₁ ↦ u₁₂} {u₂₁ ↦ u₂₂} (⊑-fun lt1 lt2) refl = ⟨ u₂₁ ↦ u₂₂ , ⟨ (λ {w} → fun) , ⟨ (λ {C} z → z) , ⟨ lt1 , lt2 ⟩ ⟩ ⟩ ⟩ -sub-inv {u₂₁ ↦ (u₂₂ ⊔ u₂₃)} {u₂₁ ↦ u₂₂ ⊔ u₂₁ ↦ u₂₃} Dist⊑ +sub-inv {u₂₁ ↦ (u₂₂ ⊔ u₂₃)} {u₂₁ ↦ u₂₂ ⊔ u₂₁ ↦ u₂₃} ⊑-dist {.u₂₁} {.(u₂₂ ⊔ u₂₃)} refl = - ⟨ u₂₁ ↦ u₂₂ ⊔ u₂₁ ↦ u₂₃ , ⟨ f , ⟨ g , ⟨ ConjL⊑ Refl⊑ Refl⊑ , Refl⊑ ⟩ ⟩ ⟩ ⟩ - where f : Funs (u₂₁ ↦ u₂₂ ⊔ u₂₁ ↦ u₂₃) + ⟨ u₂₁ ↦ u₂₂ ⊔ u₂₁ ↦ u₂₃ , ⟨ f , ⟨ g , ⟨ ⊑-conj-L ⊑-refl ⊑-refl , ⊑-refl ⟩ ⟩ ⟩ ⟩ + where f : all-funs (u₂₁ ↦ u₂₂ ⊔ u₂₁ ↦ u₂₃) f (inj₁ x) = fun x f (inj₂ y) = fun y g : (u₂₁ ↦ u₂₂ ⊔ u₂₁ ↦ u₂₃) ⊆ (u₂₁ ↦ u₂₂ ⊔ u₂₁ ↦ u₂₃) @@ -1126,9 +1126,9 @@ sub-inv {u₂₁ ↦ (u₂₂ ⊔ u₂₃)} {u₂₁ ↦ u₂₂ ⊔ u₂₁ ↦ Let `v` and `w` be arbitrary values. -* Case `Bot⊑`. So `u₁ ≡ ⊥`. We have `v ↦ w ∈ ⊥`, but that is impossible. +* Case `⊑-bot`. So `u₁ ≡ ⊥`. We have `v ↦ w ∈ ⊥`, but that is impossible. -* Case `ConjL⊑`. +* Case `⊑-conj-L`. u₁₁ ⊑ u₂ u₁₂ ⊑ u₂ ------------------- @@ -1142,7 +1142,7 @@ Let `v` and `w` be arbitrary values. * Subcase `v ↦ w ∈ u₁₂`. We conclude by the induction hypothesis for `u₁₂ ⊑ u₂`. -* Case `ConjR1⊑`. +* Case `⊑-conj-R1`. u₁ ⊑ u₂₁ -------------- @@ -1154,10 +1154,10 @@ Let `v` and `w` be arbitrary values. we just need to show that `u₃₁ ⊆ u₂₁ ⊔ u₂₂`, but that follows directly from `u₃₁ ⊆ u₂₁`. -* Case `ConjR2⊑`. This case follows by reasoning similar to - the case for `ConjR1⊑`. +* Case `⊑-conj-R2`. This case follows by reasoning similar to + the case for `⊑-conj-R1`. -* Case `Trans⊑`. +* Case `⊑-trans`. u₁ ⊑ u u ⊑ u₂ --------------- @@ -1165,7 +1165,7 @@ Let `v` and `w` be arbitrary values. By the induction hypothesis for `u₁ ⊑ u`, we know that `v ↦ w` factors `u` into `u′`, for some value `u′`, - so we have `Funs u′` and `u′ ⊆ u`. + so we have `all-funs u′` and `u′ ⊆ u`. By the induction hypothesis for `u ⊑ u₂`, we know that for any `v′ ↦ w′ ∈ u`, `v′ ↦ w′` factors `u₂`. Now we apply the lemma sub-inv-trans, which gives us @@ -1175,7 +1175,7 @@ Let `v` and `w` be arbitrary values. From `w ⊑ cod u′` and `cod u′ ⊑ cod u₃`, we have `w ⊑ cod u₃`, and this case is complete. -* Case `Fun⊑`. +* Case `⊑-fun`. u₂₁ ⊑ u₁₁ u₁₂ ⊑ u₂₂ --------------------- @@ -1186,7 +1186,7 @@ Let `v` and `w` be arbitrary values. We need to show that `dom (u₂₁ ↦ u₂₂) ⊑ u₁₁` and `u₁₂ ⊑ cod (u₂₁ ↦ u₂₂)`, but that is equivalent to our premises `u₂₁ ⊑ u₁₁` and `u₁₂ ⊑ u₂₂`. -* Case `Dist⊑`. +* Case `⊑-dist`. --------------------------------------------- u₂₁ ↦ (u₂₂ ⊔ u₂₃) ⊑ (u₂₁ ↦ u₂₂) ⊔ (u₂₁ ↦ u₂₃) @@ -1208,14 +1208,14 @@ and we modify the conclusion to say that for every sub-inv-fun : ∀{v w u₁ : Value} → (v ↦ w) ⊑ u₁ ----------------------------------------------------- - → Σ[ u₂ ∈ Value ] Funs u₂ × u₂ ⊆ u₁ + → Σ[ u₂ ∈ Value ] all-funs u₂ × u₂ ⊆ u₁ × (∀{v′ w′} → (v′ ↦ w′) ∈ u₂ → v′ ⊑ v) × w ⊑ cod u₂ sub-inv-fun{v}{w}{u₁} abc with sub-inv abc {v}{w} refl ... | ⟨ u₂ , ⟨ f , ⟨ u₂⊆u₁ , ⟨ db , cc ⟩ ⟩ ⟩ ⟩ = ⟨ u₂ , ⟨ f , ⟨ u₂⊆u₁ , ⟨ G , cc ⟩ ⟩ ⟩ ⟩ where G : ∀{D E} → (D ↦ E) ∈ u₂ → D ⊑ v - G{D}{E} m = Trans⊑ (⊆→⊑ (↦∈→⊆dom f m)) db + G{D}{E} m = ⊑-trans (⊆→⊑ (↦∈→⊆dom f m)) db ``` The second corollary is the inversion rule that one would expect for @@ -1229,12 +1229,12 @@ less-than with functions on the left and right-hand sides. ↦⊑↦-inv{v}{w}{v′}{w′} lt with sub-inv-fun lt ... | ⟨ Γ , ⟨ f , ⟨ Γ⊆v34 , ⟨ lt1 , lt2 ⟩ ⟩ ⟩ ⟩ - with Funs∈ f + with all-funs∈ f ... | ⟨ u , ⟨ u′ , u↦u′∈Γ ⟩ ⟩ with Γ⊆v34 u↦u′∈Γ ... | refl = let codΓ⊆w′ = ⊆↦→cod⊆ Γ⊆v34 in - ⟨ lt1 u↦u′∈Γ , Trans⊑ lt2 (⊆→⊑ codΓ⊆w′) ⟩ + ⟨ lt1 u↦u′∈Γ , ⊑-trans lt2 (⊆→⊑ codΓ⊆w′) ⟩ ``` diff --git a/src/plfa/part3/Soundness.lagda.md b/src/plfa/part3/Soundness.lagda.md index 7bca27e9..a1f788e7 100644 --- a/src/plfa/part3/Soundness.lagda.md +++ b/src/plfa/part3/Soundness.lagda.md @@ -50,7 +50,7 @@ open import plfa.part2.Untyped open import plfa.part2.Substitution using (Rename; Subst; ids) open import plfa.part3.Denotational using (Value; ⊥; Env; _⊢_↓_; _`,_; _⊑_; _`⊑_; `⊥; _`⊔_; init; last; init-last; - Refl⊑; Trans⊑; `Refl⊑; Env⊑; EnvConjR1⊑; EnvConjR2⊑; up-env; + ⊑-refl; ⊑-trans; `⊑-refl; ⊑-env; ⊑-env-conj-R1; ⊑-env-conj-R2; up-env; var; ↦-elim; ↦-intro; ⊥-intro; ⊔-intro; sub; rename-pres; ℰ; _≃_; ≃-trans) open import plfa.part3.Compositional using (lambda-inversion; var-inv) @@ -96,7 +96,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′) ``` The proof is by cases on the de Bruijn index `x`. @@ -246,7 +246,7 @@ nth-ext : ∀ {Γ Δ v} {γ : Env Γ} {δ : Env Δ} → (δ ∘ ρ) `⊑ γ ------------------------------ → ((δ `, v) ∘ ext ρ) `⊑ (γ `, v) -nth-ext ρ lt Z = Refl⊑ +nth-ext ρ lt Z = ⊑-refl nth-ext ρ lt (S x) = lt x ``` @@ -259,7 +259,7 @@ rename-reflect : ∀ {Γ Δ v} {γ : Env Γ} {δ : Env Δ} { M : Γ ⊢ ★} ------------------------------------ → γ ⊢ M ↓ v rename-reflect {M = ` x} all-n d with var-inv d -... | lt = sub var (Trans⊑ lt (all-n x)) +... | lt = sub var (⊑-trans lt (all-n x)) rename-reflect {M = ƛ N}{ρ = ρ} all-n (↦-intro d) = ↦-intro (rename-reflect (nth-ext ρ all-n) d) rename-reflect {M = ƛ N} all-n ⊥-intro = ⊥-intro @@ -310,7 +310,7 @@ rename-inc-reflect : ∀ {Γ v′ v} {γ : Env Γ} { M : Γ ⊢ ★} → (γ `, v′) ⊢ rename S_ M ↓ v ---------------------------- → γ ⊢ M ↓ v -rename-inc-reflect d = rename-reflect `Refl⊑ d +rename-inc-reflect d = rename-reflect `⊑-refl d ``` @@ -476,8 +476,8 @@ subst-reflect{Γ}{Δ}{γ}{σ = σ} (↦-elim d₁ d₂) with subst-reflect {M = M₁} d₁ refl | subst-reflect {M = M₂} d₂ refl ... | ⟨ δ₁ , ⟨ subst-δ₁ , m1 ⟩ ⟩ | ⟨ δ₂ , ⟨ subst-δ₂ , m2 ⟩ ⟩ = ⟨ δ₁ `⊔ δ₂ , ⟨ subst-⊔ {γ₁ = δ₁}{γ₂ = δ₂}{σ = σ} subst-δ₁ subst-δ₂ , - ↦-elim (Env⊑ m1 (EnvConjR1⊑ δ₁ δ₂)) - (Env⊑ m2 (EnvConjR2⊑ δ₁ δ₂)) ⟩ ⟩ + ↦-elim (⊑-env m1 (⊑-env-conj-R1 δ₁ δ₂)) + (⊑-env m2 (⊑-env-conj-R2 δ₁ δ₂)) ⟩ ⟩ subst-reflect {M = M}{σ = σ} (↦-intro d) eqL with M ... | ` x with (↦-intro d) @@ -496,8 +496,8 @@ subst-reflect {σ = σ} (⊔-intro d₁ d₂) eq with subst-reflect {σ = σ} d₁ eq | subst-reflect {σ = σ} d₂ eq ... | ⟨ δ₁ , ⟨ subst-δ₁ , m1 ⟩ ⟩ | ⟨ δ₂ , ⟨ subst-δ₂ , m2 ⟩ ⟩ = ⟨ δ₁ `⊔ δ₂ , ⟨ subst-⊔ {γ₁ = δ₁}{γ₂ = δ₂}{σ = σ} subst-δ₁ subst-δ₂ , - ⊔-intro (Env⊑ m1 (EnvConjR1⊑ δ₁ δ₂)) - (Env⊑ m2 (EnvConjR2⊑ δ₁ δ₂)) ⟩ ⟩ + ⊔-intro (⊑-env m1 (⊑-env-conj-R1 δ₁ δ₂)) + (⊑-env m2 (⊑-env-conj-R2 δ₁ δ₂)) ⟩ ⟩ subst-reflect (sub d lt) eq with subst-reflect d eq ... | ⟨ δ , ⟨ subst-δ , m ⟩ ⟩ = ⟨ δ , ⟨ subst-δ , sub m lt ⟩ ⟩ @@ -512,8 +512,8 @@ subst-reflect (sub d lt) eq * Case `M ≡ M₁ · M₂`: By the induction hypothesis, we have some `δ₁` and `δ₂` such that `δ₁ ⊢ M₁ ↓ v₁ ↦ v₃` and `γ ⊢ σ ↓ δ₁`, as well as `δ₂ ⊢ M₂ ↓ v₁` and `γ ⊢ σ ↓ δ₂`. - By `Env⊑` we have `δ₁ ⊔ δ₂ ⊢ M₁ ↓ v₁ ↦ v₃` and `δ₁ ⊔ δ₂ ⊢ M₂ ↓ v₁` - (using `EnvConjR1⊑` and `EnvConjR2⊑`), and therefore + By `⊑-env` we have `δ₁ ⊔ δ₂ ⊢ M₁ ↓ v₁ ↦ v₃` and `δ₁ ⊔ δ₂ ⊢ M₂ ↓ v₁` + (using `⊑-env-conj-R1` and `⊑-env-conj-R2`), and therefore `δ₁ ⊔ δ₂ ⊢ M₁ · M₂ ↓ v₃`. We conclude this case by obtaining `γ ⊢ σ ↓ δ₁ ⊔ δ₂` by the `subst-⊔` lemma. @@ -538,7 +538,7 @@ subst-reflect (sub d lt) eq * Case `⊔-intro`: By the induction hypothesis we have `δ₁ ⊢ M ↓ v₁`, `δ₂ ⊢ M ↓ v₂`, `δ ⊢ σ ↓ δ₁`, and `δ ⊢ σ ↓ δ₂`. We have `δ₁ ⊔ δ₂ ⊢ M ↓ v₁` and `δ₁ ⊔ δ₂ ⊢ M ↓ v₂` - by `Env⊑` with `EnvConjR1⊑` and `EnvConjR2⊑`. + by `⊑-env` with `⊑-env-conj-R1` and `⊑-env-conj-R2`. So by `⊔-intro` we have `δ₁ ⊔ δ₂ ⊢ M ↓ v₁ ⊔ v₂`. By `subst-⊔` we conclude that `δ ⊢ σ ↓ δ₁ ⊔ δ₂`. @@ -565,7 +565,7 @@ subst-zero-reflect : ∀ {Δ} {δ : Env Δ} {γ : Env (Δ , ★)} {M : Δ ⊢ subst-zero-reflect {δ = δ} {γ = γ} δσγ = ⟨ last γ , ⟨ lemma , δσγ Z ⟩ ⟩ where lemma : γ `⊑ (δ `, last γ) - lemma Z = Refl⊑ + lemma Z = ⊑-refl lemma (S x) = var-inv (δσγ (S x)) ``` @@ -586,14 +586,14 @@ substitution-reflect : ∀ {Δ} {δ : Env Δ} {N : Δ , ★ ⊢ ★} {M : Δ ⊢ → Σ[ w ∈ Value ] δ ⊢ M ↓ w × (δ `, w) ⊢ N ↓ v substitution-reflect d with subst-reflect d refl ... | ⟨ γ , ⟨ δσγ , γNv ⟩ ⟩ with subst-zero-reflect δσγ -... | ⟨ w , ⟨ ineq , δMw ⟩ ⟩ = ⟨ w , ⟨ δMw , Env⊑ γNv ineq ⟩ ⟩ +... | ⟨ w , ⟨ ineq , δMw ⟩ ⟩ = ⟨ w , ⟨ δMw , ⊑-env γNv ineq ⟩ ⟩ ``` We apply the `subst-reflect` lemma to obtain `δ ⊢ subst-zero M ↓ γ` and `γ ⊢ N ↓ v` for some `γ`. Using the former, the `subst-zero-reflect` lemma gives us `γ ⊑ (δ , w)` and `δ ⊢ M ↓ w`. We conclude that -`δ , w ⊢ N ↓ v` by applying the `Env⊑` lemma, using +`δ , w ⊢ N ↓ v` by applying the `⊑-env` lemma, using `γ ⊢ N ↓ v` and `γ ⊑ (δ , w)`.