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

another tweak

Browse source
This commit is contained in:
Jeremy Siek 2020-03-11 15:45:02 -04:00
parent 552ec893c6
commit 6b595851d6
1 changed files with 7 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/plfa/part3/Denotational.lagda.md
View file

@ -768,14 +768,14 @@ of the cases are trivial except the cases for variables and lambda.
values.
## Identity renamings and environment strengthening
## Environment strengthening and identity renaming
We shall need a corollary of the renaming lemma that says that if `M`
results in `v`, then we can replace a value in the environment with a
larger one (a stronger one), and `M` still results in `v`. In
We shall need a corollary of the renaming lemma that says that
replacing the environment with a larger one (a stronger one) does not
change whether a term `M` results in particular value `v`. In
particular, if `γ ⊢ M ↓ v` and `γ ⊑ δ`, then `δ ⊢ M ↓ v`. What does
this have to do with renaming? It's renaming with the identity
function. So we apply the renaming lemma with the identity renaming,
function. We apply the renaming lemma with the identity renaming,
which gives us `δ ⊢ rename (λ {A} x → x) M ↓ v`, and then we apply the
`rename-id` lemma to obtain `δ ⊢ M ↓ v`.
@ -787,8 +787,8 @@ which gives us `δ ⊢ rename (λ {A} x → x) M ↓ v`, and then we apply the
→ δ ⊢ M ↓ v
⊑-env{Γ}{γ}{δ}{M}{v} d lt
with rename-pres{Γ}{Γ}{v}{γ}{δ}{M} (λ {A} x → x) lt d
... | d′ rewrite rename-id {Γ}{★}{M} =
d′
... | δ⊢id[M]↓v rewrite rename-id {Γ}{★}{M} =
δ⊢id[M]↓v
```
In the proof that substitution reflects denotations, in the case for