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

tweak

Browse source
This commit is contained in:
Jeremy Siek 2020-07-17 10:08:38 -04:00
parent b538aba98b
commit 5095ca11c1
1 changed files with 12 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/plfa/part2/Subtyping.lagda.md
View file

@ -616,7 +616,7 @@ terms. Thus, the `subst` function is split into two parts: a raw
`subst` function that operators on terms and a `subst-pres` lemma that `subst` function that operators on terms and a `subst-pres` lemma that
proves that substitution preserves types. We define `subst` in this proves that substitution preserves types. We define `subst` in this
section and postpone `subst-pres` to the section and postpone `subst-pres` to the
[Preservation](#subtyping-pres) section. Likewise for `rename`. [Preservation](#subtyping-preservation) section. Likewise for `rename`.
We begin by defining the `ext` function on renamings. We begin by defining the `ext` function on renamings.
``` ```
@ -877,13 +877,14 @@ typed (C-suc c) = ⊢suc (typed c)
typed (C-rcd ⊢Ms dks As<:Bs) = ⊢<: (⊢rcd ⊢Ms dks) As<:Bs typed (C-rcd ⊢Ms dks As<:Bs) = ⊢<: (⊢rcd ⊢Ms dks) As<:Bs
``` ```
## Progress ## Progress <a name="subtyping-progress"></a>
The Progress theorem states that a well-typed term may either take a The Progress theorem states that a well-typed term may either take a
reduction step or it is already a value. The proof of Progress is like reduction step or it is already a value. The proof of Progress is like
the one in the [Properties](./Properties.lagda.md); it proceeds by the one in the [Properties]({{ site.baseurl }}/Properties/); it
induction on the typing derivation and most of the cases remain the proceeds by induction on the typing derivation and most of the cases
same. Below we discuss the new cases for records and subsumption. remain the same. Below we discuss the new cases for records and
subsumption.
``` ```
data Progress (M : Term) : Set where data Progress (M : Term) : Set where
@ -932,11 +933,10 @@ progress (⊢# {n}{Γ}{A}{M}{l}{ls}{As}{i}{d} ⊢M ls[i]=l As[i]=A)
with canonical ⊢M VM with canonical ⊢M VM
... | C-rcd {ks = ms}{As = Bs} ⊢Ms _ (<:-rcd ls⊆ms _) ... | C-rcd {ks = ms}{As = Bs} ⊢Ms _ (<:-rcd ls⊆ms _)
with lookup-⊆ {i = i} ls⊆ms with lookup-⊆ {i = i} ls⊆ms
... | ⟨ k , ls[i]=ms[k] ⟩ = step (β-# {j = k} (trans (sym ls[i]=ms[k]) ls[i]=l)) ... | ⟨ k , ls[i]=ms[k] ⟩ = step (β-# {j = k}(trans (sym ls[i]=ms[k]) ls[i]=l))
progress (⊢rcd x d) = done V-rcd progress (⊢rcd x d) = done V-rcd
progress (⊢<: {A = A}{B} ⊢M A<:B) = progress ⊢M progress (⊢<: {A = A}{B} ⊢M A<:B) = progress ⊢M
``` ```
* Case `⊢#`: We have `Γ ⊢ M ⦂ ｛ ls ⦂ As ｝`, `lookup ls i ≡ l`, and `lookup As i ≡ A`. * Case `⊢#`: We have `Γ ⊢ M ⦂ ｛ ls ⦂ As ｝`, `lookup ls i ≡ l`, and `lookup As i ≡ A`.
By the induction hypothesis, either `M —→ M′` or `M` is a value. In the later case we By the induction hypothesis, either `M —→ M′` or `M` is a value. In the later case we
conclude that `M # l —→ M′ # l` by rule `ξ-#`. On the other hand, if `M` is a value, conclude that `M # l —→ M′ # l` by rule `ξ-#`. On the other hand, if `M` is a value,
@ -950,7 +950,7 @@ progress (⊢<: {A = A}{B} ⊢M A<:B) = progress ⊢M
* Case `⊢<:`: we invoke the induction hypothesis on sub-derivation of `Γ ⊢ M ⦂ A`. * Case `⊢<:`: we invoke the induction hypothesis on sub-derivation of `Γ ⊢ M ⦂ A`.
## Preservation <a name="subtyping-pres"></a> ## Preservation <a name="subtyping-preservation"></a>
In this section we prove that when a well-typed term takes a reduction In this section we prove that when a well-typed term takes a reduction
step, the result is another well-typed term with the same type. step, the result is another well-typed term with the same type.