lowercase constructors
This commit is contained in:
Jeremy Siek
parent
0e27b583c2
commit
3f9f9c3c00
5 changed files with 253 additions and 248 deletions
|
|
@ -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.
|
||||
|
|
|
|||
|
|
@ -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′} =
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
```
|
||||
|
||||
|
|
|
|||
|
|
@ -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))
|
||||
```
|
||||
|
||||
<!-- above might read more nicely if we introduce inequational reasoning -->
|
||||
|
|
@ -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′) ⟩
|
||||
```
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -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)`.
|
||||
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue