michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

more apostrophes and unicode

Browse source
This commit is contained in:
Jeremy Siek 2019-05-19 15:19:33 -04:00
parent 2f378e78be
commit 57ca84d211
4 changed files with 149 additions and 119 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/plfa/Adequacy.lagda
View file

@ -635,3 +635,12 @@ cbn↔reduce {M} = ⟨ (λ x → reduce→cbn (proj₂ x)) ,
(λ x → cbn→reduce (proj₂ (proj₂ (proj₂ x)))) ⟩
\end{code}
## Unicode
This chapter uses the following unicode:
𝔼 U+1D53C MATHEMATICAL DOUBLE-STRUCK CAPITAL E (\bE)
𝔾 U+1D53E MATHEMATICAL DOUBLE-STRUCK CAPITAL G (\bG)
𝕍 U+1D53E MATHEMATICAL DOUBLE-STRUCK CAPITAL V (\bV)

150
src/plfa/Compositional.lagda
View file

@ -63,7 +63,7 @@ sub-ℱ : ∀{Γ}{N : Γ , ★ ⊢ ★}{γ v u}
------------
→ ℱ (ℰ N) γ u
sub-ℱ d Bot⊑ = tt
sub-ℱ d (Fun⊑ lt lt') = sub (up-env d lt) lt'
sub-ℱ d (Fun⊑ lt lt′) = sub (up-env d lt) lt′
sub-ℱ d (ConjL⊑ lt lt₁) = ⟨ sub-ℱ d lt , sub-ℱ d lt₁ ⟩
sub-ℱ d (ConjR1⊑ lt) = sub-ℱ (proj₁ d) lt
sub-ℱ d (ConjR2⊑ lt) = sub-ℱ (proj₂ d) lt
@ -159,23 +159,23 @@ describe the proof below.
→ ℰ (L · M) γ v
----------------
→ (ℰ L ● ℰ M) γ v
ℰ·→●ℰ (↦-elim{v = v'} d₁ d₂) = inj₂ ⟨ v' , ⟨ d₁ , d₂ ⟩ ⟩
ℰ·→●ℰ (↦-elim{v = v′} d₁ d₂) = inj₂ ⟨ v′ , ⟨ d₁ , d₂ ⟩ ⟩
ℰ·→●ℰ {v = ⊥} ⊥-intro = inj₁ Bot⊑
ℰ·→●ℰ {Γ}{γ}{L}{M}{v} (⊔-intro{v = v₁}{w = v₂} d₁ d₂)
with ℰ·→●ℰ d₁ | ℰ·→●ℰ d₂
... | inj₁ lt1 | inj₁ lt2 = inj₁ (ConjL⊑ lt1 lt2)
... | inj₁ lt1 | inj₂ ⟨ v₁' , ⟨ L↓v12 , M↓v3 ⟩ ⟩ =
inj₂ ⟨ v₁' , ⟨ sub L↓v12 lt , M↓v3 ⟩ ⟩
where lt : v₁' ↦ (v₁ ⊔ v₂) ⊑ v₁' ↦ v₂
... | inj₁ lt1 | inj₂ ⟨ v₁′ , ⟨ L↓v12 , M↓v3 ⟩ ⟩ =
inj₂ ⟨ v₁′ , ⟨ sub L↓v12 lt , M↓v3 ⟩ ⟩
where lt : v₁′ ↦ (v₁ ⊔ v₂) ⊑ v₁′ ↦ v₂
lt = (Fun⊑ Refl⊑ (ConjL⊑ (Trans⊑ lt1 Bot⊑) Refl⊑))
... | inj₂ ⟨ v₁' , ⟨ L↓v12 , M↓v3 ⟩ ⟩ | inj₁ lt2 =
inj₂ ⟨ v₁' , ⟨ sub L↓v12 lt , M↓v3 ⟩ ⟩
where lt : v₁' ↦ (v₁ ⊔ v₂) ⊑ v₁' ↦ v₁
... | inj₂ ⟨ v₁′ , ⟨ L↓v12 , M↓v3 ⟩ ⟩ | inj₁ lt2 =
inj₂ ⟨ v₁′ , ⟨ sub L↓v12 lt , M↓v3 ⟩ ⟩
where lt : v₁′ ↦ (v₁ ⊔ v₂) ⊑ v₁′ ↦ v₁
lt = (Fun⊑ Refl⊑ (ConjL⊑ Refl⊑ (Trans⊑ lt2 Bot⊑)))
... | inj₂ ⟨ v₁' , ⟨ L↓v12 , M↓v3 ⟩ ⟩ | inj₂ ⟨ v₁'' , ⟨ L↓v12' , M↓v3' ⟩ ⟩ =
let L↓⊔ = ⊔-intro L↓v12 L↓v12' in
let M↓⊔ = ⊔-intro M↓v3 M↓v3' in
let x = inj₂ ⟨ v₁' ⊔ v₁'' , ⟨ sub L↓⊔ Dist⊔↦⊔ , M↓⊔ ⟩ ⟩ in
... | inj₂ ⟨ v₁′ , ⟨ L↓v12 , M↓v3 ⟩ ⟩ | inj₂ ⟨ v₁′′ , ⟨ L↓v12′ , M↓v3′ ⟩ ⟩ =
let L↓⊔ = ⊔-intro L↓v12 L↓v12′ in
let M↓⊔ = ⊔-intro M↓v3 M↓v3′ in
let x = inj₂ ⟨ v₁′ ⊔ v₁′′ , ⟨ sub L↓⊔ Dist⊔↦⊔ , M↓⊔ ⟩ ⟩ in
x
ℰ·→●ℰ {Γ}{γ}{L}{M}{v} (sub d lt)
with ℰ·→●ℰ d
@ -186,7 +186,7 @@ describe the proof below.
We proceed by induction on the semantics.
* In case `↦-elim` we have `γ ⊢ L ↓ (v' ↦ v)` and `γ ⊢ M ↓ v'`,
* In case `↦-elim` we have `γ ⊢ L ↓ (v′ ↦ v)` and `γ ⊢ M ↓ v′`,
which is all we need to show `(ℰ L ● ℰ M) γ v`.
* In case `⊥-intro` we have `v = ⊥`. We conclude that `v ⊑ ⊥`.
@ -197,26 +197,26 @@ We proceed by induction on the semantics.
We have four subcases to consider.
* Suppose `v₁ ⊑ ⊥` and `v₂ ⊑ ⊥`. Then `v₁ ⊔ v₂ ⊑ ⊥`.
* Suppose `v₁ ⊑ ⊥`, `γ ⊢ L ↓ v₁' ↦ v₂`, and `γ ⊢ M ↓ v₁'`.
We have `γ ⊢ L ↓ v₁' ↦ (v₁ ⊔ v₂)` by rule `sub`
because `v₁' ↦ (v₁ ⊔ v₂) ⊑ v₁' ↦ v₂`.
* Suppose `γ ⊢ L ↓ v₁' ↦ v₁`, `γ ⊢ M ↓ v₁'`, and `v₂ ⊑ ⊥`.
We have `γ ⊢ L ↓ v₁' ↦ (v₁ ⊔ v₂)` by rule `sub`
because `v₁' ↦ (v₁ ⊔ v₂) ⊑ v₁' ↦ v₁`.
* Suppose `γ ⊢ L ↓ v₁'' ↦ v₁, γ ⊢ M ↓ v₁''`,
`γ ⊢ L ↓ v₁' ↦ v₂`, and `γ ⊢ M ↓ v₁'`.
* Suppose `v₁ ⊑ ⊥`, `γ ⊢ L ↓ v₁′ ↦ v₂`, and `γ ⊢ M ↓ v₁′`.
We have `γ ⊢ L ↓ v₁′ ↦ (v₁ ⊔ v₂)` by rule `sub`
because `v₁′ ↦ (v₁ ⊔ v₂) ⊑ v₁′ ↦ v₂`.
* Suppose `γ ⊢ L ↓ v₁′ ↦ v₁`, `γ ⊢ M ↓ v₁′`, and `v₂ ⊑ ⊥`.
We have `γ ⊢ L ↓ v₁′ ↦ (v₁ ⊔ v₂)` by rule `sub`
because `v₁′ ↦ (v₁ ⊔ v₂) ⊑ v₁′ ↦ v₁`.
* Suppose `γ ⊢ L ↓ v₁′′ ↦ v₁, γ ⊢ M ↓ v₁′′`,
`γ ⊢ L ↓ v₁′ ↦ v₂`, and `γ ⊢ M ↓ v₁′`.
This case is the most interesting.
By two uses of the rule `⊔-intro` we have
`γ ⊢ L ↓ (v₁' ↦ v₂) ⊔ (v₁'' ↦ v₁)` and
`γ ⊢ M ↓ (v₁' ⊔ v₁'')`. But this does not yet match
`γ ⊢ L ↓ (v₁′ ↦ v₂) ⊔ (v₁′′ ↦ v₁)` and
`γ ⊢ M ↓ (v₁′ ⊔ v₁′′)`. But this does not yet match
what we need for `ℰ L ● ℰ M` because the result of
`L` must be an `↦` whose input entry is `v₁' ⊔ v₁''`.
`L` must be an `↦` whose input entry is `v₁′ ⊔ v₁′′`.
So we use the `sub` rule to obtain
`γ ⊢ L ↓ (v₁' ⊔ v₁'') ↦ (v₁ ⊔ v₂)`,
`γ ⊢ L ↓ (v₁′ ⊔ v₁′′) ↦ (v₁ ⊔ v₂)`,
using the `Dist⊔→⊔` lemma (thanks to the `Dist⊑` rule) to
show that
(v₁' ⊔ v₁'') ↦ (v₁ ⊔ v₂) ⊑ (v₁' ↦ v₂) ⊔ (v₁'' ↦ v₁)
(v₁′ ⊔ v₁′′) ↦ (v₁ ⊔ v₂) ⊑ (v₁′ ↦ v₂) ⊔ (v₁′′ ↦ v₁)
So we have proved what is needed for this case.
@ -225,9 +225,9 @@ We proceed by induction on the semantics.
We have two subcases to consider.
* Suppose `v₁ ⊑ ⊥`. We conclude that `v ⊑ ⊥`.
* Suppose `Γ ⊢ L ↓ v' → v₁` and `Γ ⊢ M ↓ v'`.
We conclude with `Γ ⊢ L ↓ v' → v` by rule `sub`, because
`v' → v ⊑ v' → v₁`.
* Suppose `Γ ⊢ L ↓ v′ → v₁` and `Γ ⊢ M ↓ v′`.
We conclude with `Γ ⊢ L ↓ v′ → v` by rule `sub`, because
`v′ → v ⊑ v′ → v₁`.
The forward direction is proved by cases on the premise `(ℰ L ● ℰ M) γ v`.
@ -288,23 +288,23 @@ that surrounding two denotationally-equal terms in the same context
produces two programs that are denotationally equal.
We begin by showing that denotational equality is a congruence with
respect to lambda abstraction: that `ℰ N ≃ ℰ N'` implies `ℰ (ƛ N) ≃ ℰ
(ƛ N')`. We shall use the `lam-equiv` equation to reduce this question to
respect to lambda abstraction: that `ℰ N ≃ ℰ N′` implies `ℰ (ƛ N) ≃ ℰ
(ƛ N′)`. We shall use the `lam-equiv` equation to reduce this question to
whether `ℱ` is a congruence.
\begin{code}
ℱ-cong : ∀{Γ}{D D' : Denotation (Γ , ★)}
→ D ≃ D'
ℱ-cong : ∀{Γ}{D D′ : Denotation (Γ , ★)}
→ D ≃ D′
-----------
→ ℱ D ≃ ℱ D'
ℱ-cong{Γ} D≃D' γ v =
⟨ (λ x → ℱ≃{γ}{v} x D≃D') , (λ x → ℱ≃{γ}{v} x (≃-sym D≃D')) ⟩
→ ℱ D ≃ ℱ D′
ℱ-cong{Γ} D≃D′ γ v =
⟨ (λ x → ℱ≃{γ}{v} x D≃D′) , (λ x → ℱ≃{γ}{v} x (≃-sym D≃D′)) ⟩
where
ℱ≃ : ∀{γ : Env Γ}{v}{D D' : Denotation (Γ , ★)}
→ ℱ D γ v → D ≃ D' → ℱ D' γ v
ℱ≃ {v = ⊥} fd dd' = tt
ℱ≃ {γ}{v ↦ w} fd dd' = proj₁ (dd' (γ `, v) w) fd
ℱ≃ {γ}{u ⊔ w} fd dd' = ⟨ ℱ≃{γ}{u} (proj₁ fd) dd' , ℱ≃{γ}{w} (proj₂ fd) dd' ⟩
ℱ≃ : ∀{γ : Env Γ}{v}{D D′ : Denotation (Γ , ★)}
→ ℱ D γ v → D ≃ D′ → ℱ D′ γ v
ℱ≃ {v = ⊥} fd dd′ = tt
ℱ≃ {γ}{v ↦ w} fd dd′ = proj₁ (dd′ (γ `, v) w) fd
ℱ≃ {γ}{u ⊔ w} fd dd′ = ⟨ ℱ≃{γ}{u} (proj₁ fd) dd′ , ℱ≃{γ}{w} (proj₂ fd) dd′ ⟩
\end{code}
The proof of `ℱ-cong` uses the lemma `ℱ≃` to handle both directions of
@ -315,38 +315,38 @@ We now prove that lambda abstraction is a congruence by direct
equational reasoning.
\begin{code}
lam-cong : ∀{Γ}{N N' : Γ , ★ ⊢ ★}
→ ℰ N ≃ ℰ N'
lam-cong : ∀{Γ}{N N′ : Γ , ★ ⊢ ★}
→ ℰ N ≃ ℰ N′
-----------------
→ ℰ (ƛ N) ≃ ℰ (ƛ N')
lam-cong {Γ}{N}{N'} N≃N' =
→ ℰ (ƛ N) ≃ ℰ (ƛ N′)
lam-cong {Γ}{N}{N′} N≃N′ =
start
ℰ (ƛ N)
≃⟨ lam-equiv ⟩
ℱ (ℰ N)
≃⟨ ℱ-cong N≃N' ⟩
ℱ (ℰ N')
≃⟨ ℱ-cong N≃N′ ⟩
ℱ (ℰ N′)
≃⟨ ≃-sym lam-equiv ⟩
ℰ (ƛ N')
ℰ (ƛ N′)
☐
\end{code}
Next we prove that denotational equality is a congruence for
application: that `ℰ L ≃ ℰ L'` and `ℰ M ≃ ℰ M'` imply
`ℰ (L · M) ≃ ℰ (L' · M')`. The `app-equiv` equation
application: that `ℰ L ≃ ℰ L′` and `ℰ M ≃ ℰ M′` imply
`ℰ (L · M) ≃ ℰ (L′ · M′)`. The `app-equiv` equation
reduces this to the question of whether the `●` operator
is a congruence.
\begin{code}
●-cong : ∀{Γ}{D₁ D₁' D₂ D₂' : Denotation Γ}
→ D₁ ≃ D₁' → D₂ ≃ D₂'
→ (D₁ ● D₂) ≃ (D₁' ● D₂')
●-cong : ∀{Γ}{D₁ D₁′ D₂ D₂′ : Denotation Γ}
→ D₁ ≃ D₁′ → D₂ ≃ D₂′
→ (D₁ ● D₂) ≃ (D₁′ ● D₂′)
●-cong {Γ} d1 d2 γ v = ⟨ (λ x → ●≃ x d1 d2) ,
(λ x → ●≃ x (≃-sym d1) (≃-sym d2)) ⟩
where
●≃ : ∀{γ : Env Γ}{v}{D₁ D₁' D₂ D₂' : Denotation Γ}
→ (D₁ ● D₂) γ v → D₁ ≃ D₁' → D₂ ≃ D₂'
→ (D₁' ● D₂') γ v
●≃ : ∀{γ : Env Γ}{v}{D₁ D₁′ D₂ D₂′ : Denotation Γ}
→ (D₁ ● D₂) γ v → D₁ ≃ D₁′ → D₂ ≃ D₂′
→ (D₁′ ● D₂′) γ v
●≃ (inj₁ v⊑⊥) eq₁ eq₂ = inj₁ v⊑⊥
●≃ {γ} {w} (inj₂ ⟨ v , ⟨ Dv↦w , Dv ⟩ ⟩) eq₁ eq₂ =
inj₂ ⟨ v , ⟨ proj₁ (eq₁ γ (v ↦ w)) Dv↦w , proj₁ (eq₂ γ v) Dv ⟩ ⟩
@ -359,20 +359,20 @@ With the congruence of `●`, we can prove that application is a
congruence by direct equational reasoning.
\begin{code}
app-cong : ∀{Γ}{L L' M M' : Γ ⊢ ★}
→ ℰ L ≃ ℰ L'
→ ℰ M ≃ ℰ M'
app-cong : ∀{Γ}{L L′ M M′ : Γ ⊢ ★}
→ ℰ L ≃ ℰ L′
→ ℰ M ≃ ℰ M′
-------------------------
→ ℰ (L · M) ≃ ℰ (L' · M')
app-cong {Γ}{L}{L'}{M}{M'} L≅L' M≅M' =
→ ℰ (L · M) ≃ ℰ (L′ · M′)
app-cong {Γ}{L}{L′}{M}{M′} L≅L′ M≅M′ =
start
ℰ (L · M)
≃⟨ app-equiv ⟩
ℰ L ● ℰ M
≃⟨ ●-cong L≅L' M≅M' ⟩
ℰ L' ● ℰ M'
≃⟨ ●-cong L≅L′ M≅M′ ⟩
ℰ L′ ● ℰ M′
≃⟨ ≃-sym app-equiv ⟩
ℰ (L' · M')
ℰ (L′ · M′)
☐
\end{code}
@ -434,15 +434,23 @@ compositionality : ∀{Γ Δ}{C : Ctx Γ Δ} {M N : Γ ⊢ ★}
---------------------------
→ ℰ (plug C M) ≃ ℰ (plug C N)
compositionality {C = CHole} M≃N =
M≃N
compositionality {C = CLam C'} M≃N =
lam-cong (compositionality {C = C'} M≃N)
compositionality {C = CAppL C' L} M≃N =
app-cong (compositionality {C = C'} M≃N) λ γ v → ⟨ (λ x → x) , (λ x → x) ⟩
compositionality {C = CAppR L C'} M≃N =
app-cong (λ γ v → ⟨ (λ x → x) , (λ x → x) ⟩) (compositionality {C = C'} M≃N)
M≃N
compositionality {C = CLam C′} M≃N =
lam-cong (compositionality {C = C′} M≃N)
compositionality {C = CAppL C′ L} M≃N =
app-cong (compositionality {C = C′} M≃N) λ γ v → ⟨ (λ x → x) , (λ x → x) ⟩
compositionality {C = CAppR L C′} M≃N =
app-cong (λ γ v → ⟨ (λ x → x) , (λ x → x) ⟩) (compositionality {C = C′} M≃N)
\end{code}
The proof is a straightforward induction on the context `C`, using the
congruence properties `lam-cong` and `app-cong` that we established
above.
## Unicode
This chapter uses the following unicode:
ℱ U+2131 SCRIPT CAPITAL F (\McF)
● U+2131 BLACK CIRCLE (\cib)

7
src/plfa/ContextualEquivalence.lagda
View file

@ -115,3 +115,10 @@ denot-equal-contex-equal{Γ}{M}{N} eq {C} =
⟨ (λ tm → denot-equal-terminates eq tm) ,
(λ tn → denot-equal-terminates (≃-sym eq) tn) ⟩
\end{code}
## Unicode
This chapter uses the following unicode:
≅ U+2245 APPROXIMATELY EQUAL TO (\~= or \cong)

102
src/plfa/Soundness.lagda
View file

@ -102,7 +102,7 @@ subst-ext : ∀ {Γ Δ v} {γ : Env Γ} {δ : Env Δ}
--------------------------
→ δ `, v `⊢ exts σ ↓ γ `, v
subst-ext σ d Z = var
subst-ext σ d (S x) = rename-pres S_ (λ _ → Refl⊑) (d x)
subst-ext σ d (S x′) = rename-pres S_ (λ _ → Refl⊑) (d x′)
\end{code}
The proof is by cases on the de Bruijn index `x`.
@ -110,8 +110,8 @@ The proof is by cases on the de Bruijn index `x`.
* If it is `Z`, then we need to show that `δ , v ⊢ # 0 ↓ v`,
which we have by rule `var`.
* If it is `S x'`,then we need to show that
`δ , v ⊢ rename S_ (σ x') ↓ nth x' γ`,
* If it is `S x′`,then we need to show that
`δ , v ⊢ rename S_ (σ x′) ↓ nth x′ γ`,
which we obtain by the `rename-pres` lemma.
With the extension lemma in hand, the proof that simultaneous
@ -312,8 +312,8 @@ In the upcoming uses of `rename-reflect`, the renaming will always be
the increment function. So we prove a corollary for that special case.
\begin{code}
rename-inc-reflect : ∀ {Γ v' v} {γ : Env Γ} { M : Γ ⊢ ★}
→ (γ `, v') ⊢ rename S_ M ↓ v
rename-inc-reflect : ∀ {Γ v′ v} {γ : Env Γ} { M : Γ ⊢ ★}
→ (γ `, v′) ⊢ rename S_ M ↓ v
----------------------------
→ γ ⊢ M ↓ v
rename-inc-reflect d = rename-reflect `Refl⊑ d
@ -376,7 +376,7 @@ nth-const-env : ∀{Γ} {x : Γ ∋ ★} {v} → (const-env x v) x ≡ v
nth-const-env {x = x} rewrite var≟-refl x = refl
\end{code}
The nth element of `const-env n' v` is the value `⊥, so long as `n ≢ n'`.
The nth element of `const-env n′ v` is the value `⊥, so long as `n ≢ n′`.
\begin{code}
diff-nth-const-env : ∀{Γ} {x y : Γ ∋ ★} {v}
@ -482,13 +482,13 @@ subst-reflect {M = M}{σ = σ} (var {x = y}) eqL with M
... | ` x with var {x = y}
... | yv rewrite sym eqL = subst-reflect-var {σ = σ} yv
subst-reflect {M = M} (var {x = y}) () | M₁ · M₂
subst-reflect {M = M} (var {x = y}) () | ƛ M'
subst-reflect {M = M} (var {x = y}) () | ƛ M′
subst-reflect {M = M}{σ = σ} (↦-elim d₁ d₂) eqL
with M
... | ` x with ↦-elim d₁ d₂
... | d' rewrite sym eqL = subst-reflect-var {σ = σ} d'
subst-reflect (↦-elim d₁ d₂) () | ƛ M'
... | d′ rewrite sym eqL = subst-reflect-var {σ = σ} d′
subst-reflect (↦-elim d₁ d₂) () | ƛ M′
subst-reflect{Γ}{Δ}{γ}{σ = σ} (↦-elim d₁ d₂)
refl | M₁ · M₂
with subst-reflect {M = M₁} d₁ refl | subst-reflect {M = M₂} d₂ refl
@ -499,8 +499,8 @@ subst-reflect{Γ}{Δ}{γ}{σ = σ} (↦-elim d₁ d₂)
subst-reflect {M = M}{σ = σ} (↦-intro d) eqL with M
... | ` x with (↦-intro d)
... | d' rewrite sym eqL = subst-reflect-var {σ = σ} d'
subst-reflect {σ = σ} (↦-intro d) eq | ƛ M'
... | d′ rewrite sym eqL = subst-reflect-var {σ = σ} d′
subst-reflect {σ = σ} (↦-intro d) eq | ƛ M′
with subst-reflect {σ = exts σ} d (lambda-inj eq)
... | ⟨ δ′ , ⟨ exts-σ-δ′ , m′ ⟩ ⟩ =
⟨ init δ′ , ⟨ ((λ x → rename-inc-reflect (exts-σ-δ′ (S x)))) ,
@ -536,17 +536,17 @@ subst-reflect (sub d lt) eq
We conclude this case by obtaining `γ ⊢ σ ↓ δ₁ ⊔ δ₂`
by the `subst-⊔` lemma.
* Case `↦-intro`: We have `subst σ M ≡ ƛ L'`. We proceed by cases on `M`.
* Case `↦-intro`: We have `subst σ M ≡ ƛ L′`. We proceed by cases on `M`.
* Case `M ≡ x`: We apply the `subst-reflect-var` lemma.
* Case `M ≡ ƛ M'`: By the induction hypothesis, we have
`(δ' , v') ⊢ M' ↓ v₂` and `(δ , v₁) ⊢ exts σ ↓ (δ' , v')`.
From the later we have `(δ , v₁) ⊢ # 0 ↓ v'`.
By the lemma `var-inv` we have `v' ⊑ v₁`, so by the `up-env` lemma we
have `(δ' , v₁) ⊢ M' ↓ v₂` and therefore `δ' ⊢ ƛ M' ↓ v₁ → v₂`. We
also need to show that `δ `⊢ σ ↓ δ'`. Fix `k`. We have
`(δ , v₁) ⊢ rename S_ σ k ↓ nth k δ'`. We then apply the lemma
`rename-inc-reflect` to obtain `δ ⊢ σ k ↓ nth k δ'`, so this case is
* Case `M ≡ ƛ M′`: By the induction hypothesis, we have
`(δ′ , v′) ⊢ M′ ↓ v₂` and `(δ , v₁) ⊢ exts σ ↓ (δ′ , v′)`.
From the later we have `(δ , v₁) ⊢ # 0 ↓ v′`.
By the lemma `var-inv` we have `v′ ⊑ v₁`, so by the `up-env` lemma we
have `(δ′ , v₁) ⊢ M′ ↓ v₂` and therefore `δ′ ⊢ ƛ M′ ↓ v₁ → v₂`. We
also need to show that `δ `⊢ σ ↓ δ′`. Fix `k`. We have
`(δ , v₁) ⊢ rename S_ σ k ↓ nth k δ′`. We then apply the lemma
`rename-inc-reflect` to obtain `δ ⊢ σ k ↓ nth k δ′`, so this case is
complete.
* Case `⊥-intro`: We choose `⊥` for `δ`.
@ -571,45 +571,45 @@ give terms `N : (Γ , ★ ⊢ ★)` and `M : (Γ ⊢ ★)`,
if `γ ⊢ N [ M ] ↓ w`, then `γ ⊢ M ↓ v` and `(γ , v) ⊢ N ↓ w`
for some value `v`. We have `N [ M ] = subst (subst-zero M) N`.
We apply the `subst-reflect` lemma to obtain
`γ ⊢ subst-zero M ↓ (δ' , v')` and `(δ' , v') ⊢ N ↓ w`
for some `δ'` and `v'`.
`γ ⊢ subst-zero M ↓ (δ′ , v′)` and `(δ′ , v′) ⊢ N ↓ w`
for some `δ′` and `v′`.
Instantiating `γ ⊢ subst-zero M ↓ (δ' , v')` at `k = 0`
gives us `γ ⊢ M ↓ v'`. We choose `w = v'`, so the first
Instantiating `γ ⊢ subst-zero M ↓ (δ′ , v′)` at `k = 0`
gives us `γ ⊢ M ↓ v′`. We choose `w = v′`, so the first
part of our conclusion is complete.
It remains to prove `(γ , v') ⊢ N ↓ v`. First, we obtain
`(γ , v') ⊢ rename var-id N ↓ v` by the `rename-pres` lemma
applied to `(δ' , v') ⊢ N ↓ v`, with the `var-id` renaming,
`γ = (δ' , v')`, and `δ = (γ , v')`. To apply this lemma,
It remains to prove `(γ , v′) ⊢ N ↓ v`. First, we obtain
`(γ , v′) ⊢ rename var-id N ↓ v` by the `rename-pres` lemma
applied to `(δ′ , v′) ⊢ N ↓ v`, with the `var-id` renaming,
`γ = (δ′ , v′)`, and `δ = (γ , v′)`. To apply this lemma,
we need to show that
`nth n (δ' , v') ⊑ nth (var-id n) (γ , v')` for any `n`.
`nth n (δ′ , v′) ⊑ nth (var-id n) (γ , v′)` for any `n`.
This is accomplished by the following lemma, which
makes use of `γ ⊢ subst-zero M ↓ (δ' , v')`.
makes use of `γ ⊢ subst-zero M ↓ (δ′ , v′)`.
\begin{code}
nth-id-le : ∀{Γ}{δ'}{v'}{γ}{M}
→ γ `⊢ subst-zero M ↓ (δ' `, v')
nth-id-le : ∀{Γ}{δ′}{v′}{γ}{M}
→ γ `⊢ subst-zero M ↓ (δ′ `, v′)
-----------------------------------------------------
→ (x : Γ , ★ ∋ ★) → (δ' `, v') x ⊑ (γ `, v') (var-id x)
nth-id-le γ-sz-δ'v' Z = Refl⊑
nth-id-le γ-sz-δ'v' (S n') = var-inv (γ-sz-δ'v' (S n'))
→ (x : Γ , ★ ∋ ★) → (δ′ `, v′) x ⊑ (γ `, v′) (var-id x)
nth-id-le γ-sz-δ′v′ Z = Refl⊑
nth-id-le γ-sz-δ′v′ (S n′) = var-inv (γ-sz-δ′v′ (S n′))
\end{code}
The above lemma proceeds by induction on `n`.
* If it is `Z`, then we show that `v' ⊑ v'` by `Refl⊑`.
* If it is `S n'`, then from the premise we obtain
`γ ⊢ # n' ↓ nth n' δ'`. By `var-inv` we have
`nth n' δ' ⊑ nth n' γ` from which we conclude that
`nth (S n') (δ' , v') ⊑ nth (var-id (S n')) (γ , v')`.
* If it is `Z`, then we show that `v′ ⊑ v′` by `Refl⊑`.
* If it is `S n′`, then from the premise we obtain
`γ ⊢ # n′ ↓ nth n′ δ′`. By `var-inv` we have
`nth n′ δ′ ⊑ nth n′ γ` from which we conclude that
`nth (S n′) (δ′ , v′) ⊑ nth (var-id (S n′)) (γ , v′)`.
Returning to the proof that single substitution reflects
denotations, we have just proved that
(γ `, v') ⊢ rename var-id N ↓ v
(γ `, v′) ⊢ rename var-id N ↓ v
but we need to show `(γ `, v') ⊢ N ↓ v`.
but we need to show `(γ `, v′) ⊢ N ↓ v`.
So we apply the `rename-id` lemma to obtain
`rename var-id N ≡ N`.
@ -647,30 +647,30 @@ reflect-beta : ∀{Γ}{γ : Env Γ}{M N}{v}
→ γ ⊢ (ƛ N) · M ↓ v
reflect-beta d
with substitution-reflect d
... | ⟨ v₂' , ⟨ d₁' , d₂' ⟩ ⟩ = ↦-elim (↦-intro d₂') d₁'
... | ⟨ v₂′ , ⟨ d₁′ , d₂′ ⟩ ⟩ = ↦-elim (↦-intro d₂′) d₁′
reflect : ∀ {Γ} {γ : Env Γ} {M M' N v}
→ γ ⊢ N ↓ v → M —→ M' → M' ≡ N
reflect : ∀ {Γ} {γ : Env Γ} {M M′ N v}
→ γ ⊢ N ↓ v → M —→ M′ → M′ ≡ N
---------------------------------
→ γ ⊢ M ↓ v
reflect var (ξ₁ r) ()
reflect var (ξ₂ r) ()
reflect{γ = γ} (var{x = x}) β mn
with var{γ = γ}{x = x}
... | d' rewrite sym mn = reflect-beta d'
... | d′ rewrite sym mn = reflect-beta d′
reflect var (ζ r) ()
reflect (↦-elim d₁ d₂) (ξ₁ r) refl = ↦-elim (reflect d₁ r refl) d₂
reflect (↦-elim d₁ d₂) (ξ₂ r) refl = ↦-elim d₁ (reflect d₂ r refl)
reflect (↦-elim d₁ d₂) β mn
with ↦-elim d₁ d₂
... | d' rewrite sym mn = reflect-beta d'
... | d′ rewrite sym mn = reflect-beta d′
reflect (↦-elim d₁ d₂) (ζ r) ()
reflect (↦-intro d) (ξ₁ r) ()
reflect (↦-intro d) (ξ₂ r) ()
reflect (↦-intro d) β mn
with ↦-intro d
... | d' rewrite sym mn = reflect-beta d'
... | d′ rewrite sym mn = reflect-beta d′
reflect (↦-intro d) (ζ r) refl = ↦-intro (reflect d r refl)
reflect ⊥-intro r mn = ⊥-intro
reflect (⊔-intro d₁ d₂) r mn rewrite sym mn =
@ -708,3 +708,9 @@ soundness {Γ} (L —→⟨ r ⟩ M—↠N) γ v =
≃-trans {Γ} e ih γ v
\end{code}
## Unicode
This chapter uses the following unicode:
≟ U+225F QUESTIONED EQUAL TO (\?=)