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

continuing to revise Stlc and StlcProp

Browse source
This commit is contained in:
Philip Wadler 2017-07-11 13:55:00 +01:00
parent eceafb86eb
commit c059b831af
2 changed files with 145 additions and 164 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

60
src/Stlc.lagda
View file

@ -34,7 +34,7 @@ infix 15 λ[_∶_]_
infix 15 if_then_else_ infix 15 if_then_else_
data Term : Set where data Term : Set where
var : Id → Term ` : Id → Term
λ[_∶_]_ : Id → Type → Term → Term λ[_∶_]_ : Id → Type → Term → Term
_·_ : Term → Term → Term _·_ : Term → Term → Term
true : Term true : Term
@ -49,8 +49,8 @@ f = id 0
x = id 1 x = id 1
not two : Term not two : Term
not = λ[ x ∶ 𝔹 ] (if var x then false else true) not = λ[ x ∶ 𝔹 ] (if ` x then false else true)
two = λ[ f ∶ 𝔹 ⇒ 𝔹 ] λ[ x ∶ 𝔹 ] var f · (var f · var x) two = λ[ f ∶ 𝔹 ⇒ 𝔹 ] λ[ x ∶ 𝔹 ] ` f · (` f · ` x)
\end{code} \end{code}
## Values ## Values
@ -66,9 +66,9 @@ data Value : Term → Set where
\begin{code} \begin{code}
_[_∶=_] : Term → Id → Term → Term _[_∶=_] : Term → Id → Term → Term
(var x′) [ x ∶= V ] with x ≟ x′ (` x′) [ x ∶= V ] with x ≟ x′
... | yes _ = V ... | yes _ = V
... | no _ = var x′ ... | no _ = ` x′
(λ[ x′ ∶ A′ ] N′) [ x ∶= V ] with x ≟ x′ (λ[ x′ ∶ A′ ] N′) [ x ∶= V ] with x ≟ x′
... | yes _ = λ[ x′ ∶ A′ ] N′ ... | yes _ = λ[ x′ ∶ A′ ] N′
... | no _ = λ[ x′ ∶ A′ ] (N′ [ x ∶= V ]) ... | no _ = λ[ x′ ∶ A′ ] (N′ [ x ∶= V ])
@ -84,22 +84,22 @@ _[_∶=_] : Term → Id → Term → Term
infix 10 _⟹_ infix 10 _⟹_
data _⟹_ : Term → Term → Set where data _⟹_ : Term → Term → Set where
β⇒ : ∀ {x A N V} → Value V → βλ· : ∀ {x A N V} → Value V →
(λ[ x ∶ A ] N) · V ⟹ N [ x ∶= V ] (λ[ x ∶ A ] N) · V ⟹ N [ x ∶= V ]
γ⇒₁ : ∀ {L L' M} → ξ·₁ : ∀ {L L′ M} →
L ⟹ L' → L ⟹ L′ →
L · M ⟹ L' · M L · M ⟹ L′ · M
γ⇒₂ : ∀ {V M M'} → ξ·₂ : ∀ {V M M′} →
Value V → Value V →
M ⟹ M' → M ⟹ M′ →
V · M ⟹ V · M' V · M ⟹ V · M′
β𝔹₁ : ∀ {M N} → βif-true : ∀ {M N} →
if true then M else N ⟹ M if true then M else N ⟹ M
β𝔹₂ : ∀ {M N} → βif-false : ∀ {M N} →
if false then M else N ⟹ N if false then M else N ⟹ N
γ𝔹 : ∀ {L L' M N} → ξif : ∀ {L L′ M N} →
L ⟹ L' → L ⟹ L′ →
if L then M else N ⟹ if L' then M else N if L then M else N ⟹ if L′ then M else N
\end{code} \end{code}
## Reflexive and transitive closure ## Reflexive and transitive closure
@ -117,26 +117,26 @@ data _⟹*_ : Term → Term → Set where
reduction₁ : not · true ⟹* false reduction₁ : not · true ⟹* false
reduction₁ = reduction₁ =
not · true not · true
⟹⟨ β⇒ value-true ⟩ ⟹⟨ βλ· value-true ⟩
if true then false else true if true then false else true
⟹⟨ β𝔹₁ ⟩ ⟹⟨ βif-true ⟩
false false
∎ ∎
reduction₂ : two · not · true ⟹* true reduction₂ : two · not · true ⟹* true
reduction₂ = reduction₂ =
two · not · true two · not · true
⟹⟨ γ⇒₁ (β⇒ value-λ) ⟩ ⟹⟨ ξ·₁ (βλ· value-λ) ⟩
(λ[ x ∶ 𝔹 ] not · (not · var x)) · true (λ[ x ∶ 𝔹 ] not · (not · ` x)) · true
⟹⟨ β⇒ value-true ⟩ ⟹⟨ βλ· value-true ⟩
not · (not · true) not · (not · true)
⟹⟨ γ⇒₂ value-λ (β⇒ value-true) ⟩ ⟹⟨ ξ·₂ value-λ (βλ· value-true) ⟩
not · (if true then false else true) not · (if true then false else true)
⟹⟨ γ⇒₂ value-λ β𝔹₁ ⟩ ⟹⟨ ξ·₂ value-λ βif-true ⟩
not · false not · false
⟹⟨ β⇒ value-false ⟩ ⟹⟨ βλ· value-false ⟩
if false then false else true if false then false else true
⟹⟨ β𝔹₂ ⟩ ⟹⟨ βif-false ⟩
true true
∎ ∎
\end{code} \end{code}
@ -156,7 +156,7 @@ infix 10 _⊢_∶_
data _⊢_∶_ : Context → Term → Type → Set where data _⊢_∶_ : Context → Term → Type → Set where
Ax : ∀ {Γ x A} → Ax : ∀ {Γ x A} →
Γ x ≡ just A → Γ x ≡ just A →
Γ ⊢ var x ∶ A Γ ⊢ ` x ∶ A
⇒-I : ∀ {Γ x N A B} → ⇒-I : ∀ {Γ x N A B} →
Γ , x ∶ A ⊢ N ∶ B → Γ , x ∶ A ⊢ N ∶ B →
Γ ⊢ λ[ x ∶ A ] N ∶ A ⇒ B Γ ⊢ λ[ x ∶ A ] N ∶ A ⇒ B
@ -201,19 +201,19 @@ the outermost term in `not` in a `λ`, which is typed using `⇒-I`. The
`⇒-I` rule in turn takes one argument, which Agda leaves as a hole. `⇒-I` rule in turn takes one argument, which Agda leaves as a hole.
typing₁ = ⇒-I { }0 typing₁ = ⇒-I { }0
?0 : ∅ , x ∶ 𝔹 ⊢ if var x then false else true ∶ 𝔹 ?0 : ∅ , x ∶ 𝔹 ⊢ if ` x then false else true ∶ 𝔹
Again we fill in the hole by typing C-c C-r. Agda observes that the Again we fill in the hole by typing C-c C-r. Agda observes that the
outermost term is now `if_then_else_`, which is typed using `𝔹-E`. The outermost term is now `if_then_else_`, which is typed using `𝔹-E`. The
`𝔹-E` rule in turn takes three arguments, which Agda leaves as holes. `𝔹-E` rule in turn takes three arguments, which Agda leaves as holes.
typing₁ = ⇒-I (𝔹-E { }0 { }1 { }2) typing₁ = ⇒-I (𝔹-E { }0 { }1 { }2)
?0 : ∅ , x ∶ 𝔹 ⊢ var x ∶ ?0 : ∅ , x ∶ 𝔹 ⊢ ` x ∶
?1 : ∅ , x ∶ 𝔹 ⊢ false ∶ 𝔹 ?1 : ∅ , x ∶ 𝔹 ⊢ false ∶ 𝔹
?2 : ∅ , x ∶ 𝔹 ⊢ true ∶ 𝔹 ?2 : ∅ , x ∶ 𝔹 ⊢ true ∶ 𝔹
Again we fill in the three holes by typing C-c C-r in each. Agda observes Again we fill in the three holes by typing C-c C-r in each. Agda observes
that `var x`, `false`, and `true` are typed using `Ax`, `𝔹-I₂`, and that `\` x`, `false`, and `true` are typed using `Ax`, `𝔹-I₂`, and
`𝔹-I₁` respectively. The `Ax` rule in turn takes an argument, to show `𝔹-I₁` respectively. The `Ax` rule in turn takes an argument, to show
that `(∅ , x ∶ 𝔹) x = just 𝔹`, which can in turn be specified with a that `(∅ , x ∶ 𝔹) x = just 𝔹`, which can in turn be specified with a
hole. After filling in all holes, the term is as above. hole. After filling in all holes, the term is as above.

249
src/StlcProp.lagda
View file

@ -81,32 +81,32 @@ _Proof_: By induction on the derivation of `∅ ⊢ M ∶ A`.
hypotheses. By the first induction hypothesis, either `L` hypotheses. By the first induction hypothesis, either `L`
can take a step or is a value. can take a step or is a value.
- If `L` can take a step, then so can `L · M` by `γ⇒₁`. - If `L` can take a step, then so can `L · M` by `ξ·₁`.
- If `L` is a value then consider `M`. By the second induction - If `L` is a value then consider `M`. By the second induction
hypothesis, either `M` can take a step or is a value. hypothesis, either `M` can take a step or is a value.
- If `M` can take a step, then so can `L · M` by `γ⇒₂`. - If `M` can take a step, then so can `L · M` by `ξ·₂`.
- If `M` is a value, then since `L` is a value with a - If `M` is a value, then since `L` is a value with a
function type we know from the canonical forms lemma function type we know from the canonical forms lemma
that it must be a lambda abstraction, that it must be a lambda abstraction,
and hence `L · M` can take a step by `β⇒`. and hence `L · M` can take a step by `βλ·`.
- If the last rule of the derivation is `𝔹-E`, then the term has - If the last rule of the derivation is `𝔹-E`, then the term has
the form `if L then M else N` where `L` has type `𝔹`. the form `if L then M else N` where `L` has type `𝔹`.
By the induction hypothesis, either `L` can take a step or is By the induction hypothesis, either `L` can take a step or is
a value. a value.
- If `L` can take a step, then so can `if L then M else N` by `γ𝔹`. - If `L` can take a step, then so can `if L then M else N` by `ξif`.
- If `L` is a value, then since it has type boolean we know from - If `L` is a value, then since it has type boolean we know from
the canonical forms lemma that it must be either `true` or the canonical forms lemma that it must be either `true` or
`false`. `false`.
- If `L` is `true`, then `if L then M else N` steps by `β𝔹₁` - If `L` is `true`, then `if L then M else N` steps by `βif-true`
- If `L` is `false`, then `if L then M else N` steps by `β𝔹₂` - If `L` is `false`, then `if L then M else N` steps by `βif-false`
This completes the proof. This completes the proof.
@ -114,26 +114,26 @@ This completes the proof.
progress (Ax ()) progress (Ax ())
progress (⇒-I ⊢N) = done value-λ progress (⇒-I ⊢N) = done value-λ
progress (⇒-E ⊢L ⊢M) with progress ⊢L progress (⇒-E ⊢L ⊢M) with progress ⊢L
... | steps L⟹L′ = steps (γ⇒₁ L⟹L′) ... | steps L⟹L′ = steps (ξ·₁ L⟹L′)
... | done valueL with progress ⊢M ... | done valueL with progress ⊢M
... | steps M⟹M′ = steps (γ⇒₂ valueL M⟹M′) ... | steps M⟹M′ = steps (ξ·₂ valueL M⟹M′)
... | done valueM with canonicalFormsLemma ⊢L valueL ... | done valueM with canonicalFormsLemma ⊢L valueL
... | canonical-λ = steps (β⇒ valueM) ... | canonical-λ = steps (βλ· valueM)
progress 𝔹-I₁ = done value-true progress 𝔹-I₁ = done value-true
progress 𝔹-I₂ = done value-false progress 𝔹-I₂ = done value-false
progress (𝔹-E ⊢L ⊢M ⊢N) with progress ⊢L progress (𝔹-E ⊢L ⊢M ⊢N) with progress ⊢L
... | steps L⟹L′ = steps (γ𝔹 L⟹L′) ... | steps L⟹L′ = steps (ξif L⟹L′)
... | done valueL with canonicalFormsLemma ⊢L valueL ... | done valueL with canonicalFormsLemma ⊢L valueL
... | canonical-true = steps β𝔹₁ ... | canonical-true = steps βif-true
... | canonical-false = steps β𝔹₂ ... | canonical-false = steps βif-false
\end{code} \end{code}
This code reads neatly in part because we look at the This code reads neatly in part because we consider the
`steps` option before the `done` option. We could, of course, `steps` option before the `done` option. We could, of course,
look at it the other way around, but then the `...` abbreviation do it the other way around, but then the `...` abbreviation
no longer works, and we will need to write out all the arguments no longer works, and we will need to write out all the arguments
in full. In general, the rule of thumb is to look at the easy case in full. In general, the rule of thumb is to consider the easy case
(here `steps`) before the hard case (her `done`). (here `steps`) before the hard case (here `done`).
If you have two hard cases, you will have to expand out `...` If you have two hard cases, you will have to expand out `...`
or introduce subsidiary functions. or introduce subsidiary functions.
@ -158,20 +158,20 @@ technical lemmas), the story goes like this:
- The _preservation theorem_ is proved by induction on a typing - The _preservation theorem_ is proved by induction on a typing
derivation, pretty much as we did in the [Types]({{ "Types" | relative_url }}) derivation, pretty much as we did in the [Types]({{ "Types" | relative_url }})
chapter. The one case that is significantly different is the one for the chapter. The one case that is significantly different is the one for the
`β⇒` rule, whose definition uses the substitution operation. To see that `βλ·` rule, whose definition uses the substitution operation. To see that
this step preserves typing, we need to know that the substitution itself this step preserves typing, we need to know that the substitution itself
does. So we prove a ... does. So we prove a ...
- _substitution lemma_, stating that substituting a (closed) - _substitution lemma_, stating that substituting a (closed) term
term `V` for a variable `x` in a term `N` preserves the type `V` for a variable `x` in a term `N` preserves the type of `N`.
of `N`. The proof goes by induction on the form of `N` and The proof goes by induction on the form of `N` and requires
requires looking at all the different cases in the definition looking at all the different cases in the definition of
of substitition. The tricky cases are the ones for substitition. The lemma does not require that `V` be a value,
variables and for function abstractions. In both cases, we though in practice we only substitute values. The tricky cases
discover that we need to take a term `V` that has been shown are the ones for variables and for function abstractions. In both
to be well-typed in some context `Γ` and consider the same cases, we discover that we need to take a term `V` that has been
term in a different context `Γ′`. For this shown to be well-typed in some context `Γ` and consider the same
we prove a... term in a different context `Γ′`. For this we prove a ...
- _context invariance_ lemma, showing that typing is preserved - _context invariance_ lemma, showing that typing is preserved
under "inessential changes" to the context---a term `M` under "inessential changes" to the context---a term `M`
@ -180,8 +180,8 @@ technical lemmas), the story goes like this:
And finally, for this, we need a careful definition of ... And finally, for this, we need a careful definition of ...
- _free variables_ of a term---i.e., those variables - _free variables_ of a term---i.e., those variables
mentioned in a term and not in the scope of an enclosing mentioned in a term and not bound in an enclosing
function abstraction binding a variable of the same name. lambda abstraction.
To make Agda happy, we need to formalize the story in the opposite To make Agda happy, we need to formalize the story in the opposite
order. order.
@ -190,19 +190,19 @@ order.
### Free Occurrences ### Free Occurrences
A variable `x` appears _free_ in a term `M` if `M` contains an A variable `x` appears _free_ in a term `M` if `M` contains an
occurrence of `x` that is not bound in an outer lambda abstraction. occurrence of `x` that is not bound in an enclosing lambda abstraction.
For example: For example:
- `x` appears free, but `f` does not, in `λ[ f ∶ (𝔹 ⇒ 𝔹) ] var f · var x` - `x` appears free, but `f` does not, in `λ[ f ∶ (𝔹 ⇒ 𝔹) ] ` f · ` x`
- both `f` and `x` appear free in `(λ[ f ∶ (𝔹 ⇒ 𝔹) ] var f · var x) · var f`; - both `f` and `x` appear free in `(λ[ f ∶ (𝔹 ⇒ 𝔹) ] ` f · ` x) · ` f`;
note that `f` appears both bound and free in this term indeed, `f` appears both bound and free in this term
- no variables appear free in `λ[ f ∶ (𝔹 ⇒ 𝔹) ] λ[ x ∶ 𝔹 ] var f · var x` - no variables appear free in `λ[ f ∶ (𝔹 ⇒ 𝔹) ] λ[ x ∶ 𝔹 ] ` f · ` x`
Formally: Formally:
\begin{code} \begin{code}
data _∈_ : Id → Term → Set where data _∈_ : Id → Term → Set where
free-var : ∀ {x} → x ∈ var x free-` : ∀ {x} → x ∈ ` x
free-λ : ∀ {x y A N} → y ≢ x → x ∈ N → x ∈ (λ[ y ∶ A ] N) free-λ : ∀ {x y A N} → y ≢ x → x ∈ N → x ∈ (λ[ y ∶ A ] N)
free-·₁ : ∀ {x L M} → x ∈ L → x ∈ (L · M) free-·₁ : ∀ {x L M} → x ∈ L → x ∈ (L · M)
free-·₂ : ∀ {x L M} → x ∈ M → x ∈ (L · M) free-·₂ : ∀ {x L M} → x ∈ M → x ∈ (L · M)
@ -227,10 +227,10 @@ Here are proofs corresponding to the first two examples above.
f≢x : f ≢ x f≢x : f ≢ x
f≢x () f≢x ()
example-free₁ : x ∈ (λ[ f ∶ (𝔹 ⇒ 𝔹) ] var f · var x) example-free₁ : x ∈ (λ[ f ∶ (𝔹 ⇒ 𝔹) ] ` f · ` x)
example-free₁ = free-λ f≢x (free-·₂ free-var) example-free₁ = free-λ f≢x (free-·₂ free-`)
example-free₂ : f ∉ (λ[ f ∶ (𝔹 ⇒ 𝔹) ] var f · var x) example-free₂ : f ∉ (λ[ f ∶ (𝔹 ⇒ 𝔹) ] ` f · ` x)
example-free₂ (free-λ f≢f _) = f≢f refl example-free₂ (free-λ f≢f _) = f≢f refl
\end{code} \end{code}
@ -240,76 +240,75 @@ Prove formally the remaining examples given above.
\begin{code} \begin{code}
postulate postulate
example-free₃ : x ∈ ((λ[ f ∶ (𝔹 ⇒ 𝔹) ] var f · var x) · var f) example-free₃ : x ∈ ((λ[ f ∶ (𝔹 ⇒ 𝔹) ] ` f · ` x) · ` f)
example-free₄ : f ∈ ((λ[ f ∶ (𝔹 ⇒ 𝔹) ] var f · var x) · var f) example-free₄ : f ∈ ((λ[ f ∶ (𝔹 ⇒ 𝔹) ] ` f · ` x) · ` f)
example-free₅ : x ∉ (λ[ f ∶ (𝔹 ⇒ 𝔹) ] λ[ x ∶ 𝔹 ] var f · var x) example-free₅ : x ∉ (λ[ f ∶ (𝔹 ⇒ 𝔹) ] λ[ x ∶ 𝔹 ] ` f · ` x)
example-free₆ : f ∉ (λ[ f ∶ (𝔹 ⇒ 𝔹) ] λ[ x ∶ 𝔹 ] var f · var x) example-free₆ : f ∉ (λ[ f ∶ (𝔹 ⇒ 𝔹) ] λ[ x ∶ 𝔹 ] ` f · ` x)
\end{code} \end{code}
Although `_∈_` may apperar to be a low-level technical definition, Although `_∈_` may appear to be a low-level technical definition,
understanding it is crucial to understanding the properties of understanding it is crucial to understanding the properties of
substitution, which are really the crux of the lambda calculus. substitution, which are really the crux of the lambda calculus.
### Substitution ### Substitution
To prove that substitution preserves typing, we first need a To prove that substitution preserves typing, we first need a technical
technical lemma connecting free variables and typing contexts: If lemma connecting free variables and typing contexts. If variable `x`
a variable `x` appears free in a term `M`, and if we know `M` is appears free in term `M`, and if `M` is well typed in context `Γ`,
well typed in context `Γ`, then it must be the case that then `Γ` must assign a type to `x`.
`Γ` assigns a type to `x`.
\begin{code} \begin{code}
freeLemma : ∀ {x M A Γ} → x ∈ M → Γ ⊢ M ∶ A → ∃ λ B → Γ x ≡ just B freeLemma : ∀ {x M A Γ} → x ∈ M → Γ ⊢ M ∶ A → ∃ λ B → Γ x ≡ just B
\end{code} \end{code}
_Proof_: We show, by induction on the proof that `x` appears _Proof_: We show, by induction on the proof that `x` appears
free in `P`, that, for all contexts `Γ`, if `P` is well free in `M`, that, for all contexts `Γ`, if `M` is well
typed under `Γ`, then `Γ` assigns some type to `x`. typed under `Γ`, then `Γ` assigns some type to `x`.
- If the last rule used was `free-var`, then `P = x`, and from - If the last rule used was `free-\``, then `M = \` x`, and from
the assumption that `M` is well typed under `Γ` we have the assumption that `M` is well typed under `Γ` we have
immediately that `Γ` assigns a type to `x`. immediately that `Γ` assigns a type to `x`.
- If the last rule used was `free-·₁`, then `P = L · M` and `x` - If the last rule used was `free-·₁`, then `M = L · M` and `x`
appears free in `L`. Since `L` is well typed under `\Gamma`, appears free in `L`. Since `L` is well typed under `Γ`,
we can see from the typing rules that `L` must also be, and we can see from the typing rules that `L` must also be, and
the IH then tells us that `Γ` assigns `x` a type. the IH then tells us that `Γ` assigns `x` a type.
- Almost all the other cases are similar: `x` appears free in a - Almost all the other cases are similar: `x` appears free in a
subterm of `P`, and since `P` is well typed under `Γ`, we subterm of `M`, and since `M` is well typed under `Γ`, we
know the subterm of `M` in which `x` appears is well typed know the subterm of `M` in which `x` appears is well typed
under `Γ` as well, and the IH gives us exactly the under `Γ` as well, and the IH yields the desired conclusion.
conclusion we want.
- The only remaining case is `free-λ`. In this case `P = - The only remaining case is `free-λ`. In this case `M =
λ[ y ∶ A ] N`, and `x` appears free in `N`; we also know that λ[ y ∶ A ] N`, and `x` appears free in `N`; we also know that
`x` is different from `y`. The difference from the previous `x` is different from `y`. The difference from the previous
cases is that whereas `P` is well typed under `\Gamma`, its cases is that whereas `M` is well typed under `Γ`, its
body `N` is well typed under `(Γ , y ∶ A)`, so the IH body `N` is well typed under `(Γ , y ∶ A)`, so the IH
allows us to conclude that `x` is assigned some type by the allows us to conclude that `x` is assigned some type by the
extended context `(Γ , y ∶ A)`. To conclude that `Γ` extended context `(Γ , y ∶ A)`. To conclude that `Γ`
assigns a type to `x`, we appeal the decidable equality for names assigns a type to `x`, we appeal the decidable equality for names
`_≟_`, noting that `x` and `y` are different variables. `_≟_`, and note that `x` and `y` are different variables.
\begin{code} \begin{code}
freeLemma free-var (Ax Γx≡justA) = (_ , Γx≡justA) freeLemma free-` (Ax Γx≡A) = (_ , Γx≡A)
freeLemma (free-·₁ x∈L) (⇒-E ⊢L ⊢M) = freeLemma x∈L ⊢L freeLemma (free-·₁ x∈L) (⇒-E ⊢L ⊢M) = freeLemma x∈L ⊢L
freeLemma (free-·₂ x∈M) (⇒-E ⊢L ⊢M) = freeLemma x∈M ⊢M freeLemma (free-·₂ x∈M) (⇒-E ⊢L ⊢M) = freeLemma x∈M ⊢M
freeLemma (free-if₁ x∈L) (𝔹-E ⊢L ⊢M ⊢N) = freeLemma x∈L ⊢L freeLemma (free-if₁ x∈L) (𝔹-E ⊢L ⊢M ⊢N) = freeLemma x∈L ⊢L
freeLemma (free-if₂ x∈M) (𝔹-E ⊢L ⊢M ⊢N) = freeLemma x∈M ⊢M freeLemma (free-if₂ x∈M) (𝔹-E ⊢L ⊢M ⊢N) = freeLemma x∈M ⊢M
freeLemma (free-if₃ x∈N) (𝔹-E ⊢L ⊢M ⊢N) = freeLemma x∈N ⊢N freeLemma (free-if₃ x∈N) (𝔹-E ⊢L ⊢M ⊢N) = freeLemma x∈N ⊢N
freeLemma (free-λ {x} {y} y≢x x∈N) (⇒-I ⊢N) with freeLemma x∈N ⊢N freeLemma (free-λ {x} {y} y≢x x∈N) (⇒-I ⊢N) with freeLemma x∈N ⊢N
... | Γx=justC with y ≟ x ... | Γx≡C with y ≟ x
... | yes y≡x = ⊥-elim (y≢x y≡x) ... | yes y≡x = ⊥-elim (y≢x y≡x)
... | no _ = Γx=justC ... | no _ = Γx≡C
\end{code} \end{code}
[A subtle point: if the first argument of `free-λ` was of type A subtle point: if the first argument of `free-λ` was of type
`x ≢ y` rather than of type `y ≢ x`, then the type of the `x ≢ y` rather than of type `y ≢ x`, then the type of the
term `Γx=justC` would not simplify properly.] term `Γx≡C` would not simplify properly; instead, one would need
to rewrite with the symmetric equivalence.
Next, we'll need the fact that any term `M` which is well typed in As a second technical lemma, we need that any term `M` which is well
the empty context is closed (it has no free variables). typed in the empty context is closed (has no free variables).
#### Exercise: 2 stars, optional (∅⊢-closed) #### Exercise: 2 stars, optional (∅⊢-closed)
@ -325,16 +324,16 @@ contradiction ()
∅⊢-closed′ : ∀ {M A} → ∅ ⊢ M ∶ A → closed M ∅⊢-closed′ : ∀ {M A} → ∅ ⊢ M ∶ A → closed M
∅⊢-closed′ {M} {A} ⊢M {x} x∈M with freeLemma x∈M ⊢M ∅⊢-closed′ {M} {A} ⊢M {x} x∈M with freeLemma x∈M ⊢M
... | (B , ∅x≡justB) = contradiction (trans (sym ∅x≡justB) (apply-∅ x)) ... | (B , ∅x≡B) = contradiction (trans (sym ∅x≡B) (apply-∅ x))
\end{code} \end{code}
</div> </div>
Sometimes, when we have a proof `Γ ⊢ M ∶ A`, we will need to Sometimes, when we have a proof `Γ ⊢ M ∶ A`, we will need to
replace `Γ` by a different context `Γ′`. When is it safe replace `Γ` by a different context `Γ′`. When is it safe
to do this? Intuitively, it must at least be the case that to do this? Intuitively, the only variables we care about
`Γ′` assigns the same types as `Γ` to all the variables in the context are those that appear free in `M`. So long
that appear free in `M`. In fact, this is the only condition that as the two contexts agree on those variables, one can be
is needed. exchanged for the other.
\begin{code} \begin{code}
contextLemma : ∀ {Γ Γ′ M A} contextLemma : ∀ {Γ Γ′ M A}
@ -343,50 +342,52 @@ contextLemma : ∀ {Γ Γ′ M A}
→ Γ′ ⊢ M ∶ A → Γ′ ⊢ M ∶ A
\end{code} \end{code}
_Proof_: By induction on the derivation of _Proof_: By induction on the derivation of `Γ ⊢ M ∶ A`.
`Γ ⊢ M ∶ A`.
- If the last rule in the derivation was `var`, then `t = x` - If the last rule in the derivation was `Ax`, then `M = x`
and `\Gamma x = T`. By assumption, `\Gamma' x = T` as well, and and `Γ x ≡ just A`. By assumption, `Γ′ x = just A` as well, and
hence `\Gamma' \vdash t : T` by `var`. hence `Γ′ ⊢ M : A` by `Ax`.
- If the last rule was `abs`, then `t = \lambda y:A. t'`, with - If the last rule was `⇒-I`, then `M = λ[ y : A] N`, with
`T = A\to B` and `\Gamma, y : A \vdash t' : B`. The `A = A ⇒ B` and `Γ , y ∶ A ⊢ N ∶ B`. The
induction hypothesis is that, for any context `\Gamma''`, if induction hypothesis is that, for any context `Γ″`, if
`\Gamma, y:A` and `\Gamma''` assign the same types to all the `Γ , y : A` and `Γ″` assign the same types to all the
free variables in `t'`, then `t'` has type `B` under free variables in `N`, then `N` has type `B` under
`\Gamma''`. Let `\Gamma'` be a context which agrees with `Γ″`. Let `Γ′` be a context which agrees with
`\Gamma` on the free variables in `t`; we must show `Γ` on the free variables in `N`; we must show
`\Gamma' \vdash \lambda y:A. t' : A\to B`. `Γ′ ⊢ λ[ y ∶ A] N ∶ A ⇒ B`.
By `abs`, it suffices to show that `\Gamma', y:A \vdash t' : t'`. By `⇒-I`, it suffices to show that `Γ′ , y:A ⊢ N ∶ B`.
By the IH (setting `\Gamma'' = \Gamma', y:A`), it suffices to show By the IH (setting `Γ″ = Γ′ , y : A`), it suffices to show
that `\Gamma, y:A` and `\Gamma', y:A` agree on all the variables that `Γ , y : A` and `Γ′ , y : A` agree on all the variables
that appear free in `t'`. that appear free in `N`.
Any variable occurring free in `t'` must be either `y` or Any variable occurring free in `N` must be either `y` or
some other variable. `\Gamma, y:A` and `\Gamma', y:A` some other variable. Clearly, `Γ , y : A` and `Γ′ , y : A`
clearly agree on `y`. Otherwise, note that any variable other agree on `y`. Otherwise, any variable other
than `y` that occurs free in `t'` also occurs free in than `y` that occurs free in `N` also occurs free in
`t = \lambda y:A. t'`, and by assumption `\Gamma` and `λ[ y : A] N`, and by assumption `Γ` and
`\Gamma'` agree on all such variables; hence so do `\Gamma, y:A` and `Γ′` agree on all such variables; hence so do
`\Gamma', y:A`. `Γ , y : A` and `Γ′ , y : A`.
- If the last rule was `app`, then `t = t_1\;t_2`, with - If the last rule was `⇒-E`, then `M = L · M`, with `Γ ⊢ L ∶ A ⇒ B`
`\Gamma \vdash t_1:A\to T` and `\Gamma \vdash t_2:A`. and `Γ ⊢ M ∶ B`. One induction hypothesis states that for all
One induction hypothesis states that for all contexts `\Gamma'`, contexts `Γ′`, if `Γ′` agrees with `Γ` on the free variables in
if `\Gamma'` agrees with `\Gamma` on the free variables in `t_1`, `L` then `L` has type `A ⇒ B` under `Γ′`; there is a similar IH
then `t_1` has type `A\to T` under `\Gamma'`; there is a similar IH for `M`. We must show that `L · M` also has type `B` under `Γ′`,
for `t_2`. We must show that `t_1\;t_2` also has type `T` under given the assumption that `Γ′` agrees with `Γ` on all the free
`\Gamma'`, given the assumption that `\Gamma'` agrees with variables in `L · M`. By `⇒-E`, it suffices to show that `L` and
`\Gamma` on all the free variables in `t_1\;t_2`. By `app`, it `M` each have the same type under `Γ′` as under `Γ`. But all free
suffices to show that `t_1` and `t_2` each have the same type variables in `L` are also free in `L · M`; in the proof, this is
under `\Gamma'` as under `\Gamma`. But all free variables in expressed by composing `free-·₁ : ∀ {x} → x ∈ L → x ∈ L · M` with
`t_1` are also free in `t_1\;t_2`, and similarly for `t_2`; `Γ~Γ′ : (∀ {x} → x ∈ L · M → Γ x ≡ Γ′ x)` to yield `Γ~Γ′ ∘ free-·₁
hence the desired result follows from the induction hypotheses. : ∀ {x} → x ∈ L → Γ x ≡ Γ′ x`. Similarly for `M`; hence the
desired result follows from the induction hypotheses.
- The remaining cases are similar to `⇒-E`.
\begin{code} \begin{code}
contextLemma Γ~Γ′ (Ax Γx≡justA) rewrite (Γ~Γ′ free-var) = Ax Γx≡justA contextLemma Γ~Γ′ (Ax Γx≡A) rewrite (Γ~Γ′ free-`) = Ax Γx≡A
contextLemma {Γ} {Γ′} {λ[ x ∶ A ] N} Γ~Γ′ (⇒-I ⊢N) = ⇒-I (contextLemma Γx~Γ′x ⊢N) contextLemma {Γ} {Γ′} {λ[ x ∶ A ] N} Γ~Γ′ (⇒-I ⊢N) = ⇒-I (contextLemma Γx~Γ′x ⊢N)
where where
Γx~Γ′x : ∀ {y} → y ∈ N → (Γ , x ∶ A) y ≡ (Γ′ , x ∶ A) y Γx~Γ′x : ∀ {y} → y ∈ N → (Γ , x ∶ A) y ≡ (Γ′ , x ∶ A) y
@ -398,26 +399,6 @@ contextLemma Γ~Γ′ 𝔹-I₁ = 𝔹-I₁
contextLemma Γ~Γ′ 𝔹-I₂ = 𝔹-I₂ contextLemma Γ~Γ′ 𝔹-I₂ = 𝔹-I₂
contextLemma Γ~Γ′ (𝔹-E ⊢L ⊢M ⊢N) contextLemma Γ~Γ′ (𝔹-E ⊢L ⊢M ⊢N)
= 𝔹-E (contextLemma (Γ~Γ′ ∘ free-if₁) ⊢L) (contextLemma (Γ~Γ′ ∘ free-if₂) ⊢M) (contextLemma (Γ~Γ′ ∘ free-if₃) ⊢N) = 𝔹-E (contextLemma (Γ~Γ′ ∘ free-if₁) ⊢L) (contextLemma (Γ~Γ′ ∘ free-if₂) ⊢M) (contextLemma (Γ~Γ′ ∘ free-if₃) ⊢N)
{-
replaceCtxt f (var x x∶A
) rewrite f var = var x x∶A
replaceCtxt f (app t₁∶A⇒B t₂∶A)
= app (replaceCtxt (f ∘ app1) t₁∶A⇒B) (replaceCtxt (f ∘ app2) t₂∶A)
replaceCtxt {Γ} {Γ′} f (abs {.Γ} {x} {A} {B} {t′} t′∶B)
= abs (replaceCtxt f′ t′∶B)
where
f′ : ∀ {y} → y ∈ t′ → (Γ , x ∶ A) y ≡ (Γ′ , x ∶ A) y
f′ {y} y∈t′ with x ≟ y
... | yes _ = refl
... | no x≠y = f (abs x≠y y∈t′)
replaceCtxt _ true = true
replaceCtxt _ false = false
replaceCtxt f (if t₁∶bool then t₂∶A else t₃∶A)
= if replaceCtxt (f ∘ if1) t₁∶bool
then replaceCtxt (f ∘ if2) t₂∶A
else replaceCtxt (f ∘ if3) t₃∶A
-}
\end{code} \end{code}
@ -590,18 +571,18 @@ _Proof_: By induction on the derivation of `\vdash t : T`.
follows directly from the induction hypothesis. follows directly from the induction hypothesis.
\begin{code} \begin{code}
preservation (Ax x₁) () preservation (Ax Γx≡A) ()
preservation (⇒-I ⊢N) () preservation (⇒-I ⊢N) ()
preservation (⇒-E (⇒-I ⊢N) ⊢V) (β⇒ valueV) = preservation-[∶=] ⊢N ⊢V preservation (⇒-E (⇒-I ⊢N) ⊢V) (βλ· valueV) = preservation-[∶=] ⊢N ⊢V
preservation (⇒-E ⊢L ⊢M) (γ⇒₁ L⟹L′) with preservation ⊢L L⟹L′ preservation (⇒-E ⊢L ⊢M) (ξ·₁ L⟹L′) with preservation ⊢L L⟹L′
...| ⊢L′ = ⇒-E ⊢L′ ⊢M ...| ⊢L′ = ⇒-E ⊢L′ ⊢M
preservation (⇒-E ⊢L ⊢M) (γ⇒₂ valueL M⟹M′) with preservation ⊢M M⟹M′ preservation (⇒-E ⊢L ⊢M) (ξ·₂ valueL M⟹M′) with preservation ⊢M M⟹M′
...| ⊢M′ = ⇒-E ⊢L ⊢M′ ...| ⊢M′ = ⇒-E ⊢L ⊢M′
preservation 𝔹-I₁ () preservation 𝔹-I₁ ()
preservation 𝔹-I₂ () preservation 𝔹-I₂ ()
preservation (𝔹-E 𝔹-I₁ ⊢M ⊢N) β𝔹₁ = ⊢M preservation (𝔹-E 𝔹-I₁ ⊢M ⊢N) βif-true = ⊢M
preservation (𝔹-E 𝔹-I₂ ⊢M ⊢N) β𝔹₂ = ⊢N preservation (𝔹-E 𝔹-I₂ ⊢M ⊢N) βif-false = ⊢N
preservation (𝔹-E ⊢L ⊢M ⊢N) (γ𝔹 L⟹L′) with preservation ⊢L L⟹L′ preservation (𝔹-E ⊢L ⊢M ⊢N) (ξif L⟹L′) with preservation ⊢L L⟹L′
...| ⊢L′ = 𝔹-E ⊢L′ ⊢M ⊢N ...| ⊢L′ = 𝔹-E ⊢L′ ⊢M ⊢N
\end{code} \end{code}