@@ -3170,891 +3157,891 @@ Prove one final property of the `update` function: If we update a map
updates.
{% raw %}
- update-permute′ : ∀ {A} (ρ : TotalMap A) (x : Id) (v : A) (y : Id) (w : A)
+ → x ≢ y → (ρ , x ↦ v , y ↦ : TotalMap Aw) ≡ (ρ , y ↦ (x : Id) (v : A) (y : Id) (w , x ↦ v)
+ update-permute′ : {A)
- →} x ≢ y → (ρ x v y w x≢y = extensionality , x ↦lemma v , y ↦ w) ≡ (ρ , y
+ where
+ lemma ↦: w∀ ,z x→ ↦(ρ v),
- update-permute′ {A}x ↦ v , y ↦ w) z ≡ (ρ ρ, xy v↦ yw w, x≢y = extensionality lemma
- where
- lemma : ∀ z → (ρ , x ↦ v , y ↦ w) z
+ lemma ≡z with x ≟ z | y ≟ z
+ ... | yes refl | yes refl = ⊥-elim (ρ ,x≢y y ↦ w , x ↦ vrefl) z
lemma... | no x≢z | zyes with xrefl ≟ z | y = sym ≟ z
- ...(update-eq′ |ρ yes reflz w)
+ |... yes| yes refl | no y≢z = ⊥-elim (x≢y refl)
- ...update-eq′ |ρ no x≢z | yes refl = sym (update-eq′ ρ z v
+ ... | no x≢z | no y≢z = trans w(update-neq ρ x v z x≢z)
- ... |(sym yes(update-neq reflρ |y no y≢z = update-eq′w ρz z v
- ... | no x≢z | no y≢z = trans (update-neq ρ x v z x≢z) (sym (update-neq ρ y w z y≢z))
{% endraw %}
@@ -4062,595 +4049,595 @@ updates.
And a slightly different version of the same proof.
{% raw %}
- update-permute′′ : ∀ {A} (ρ : TotalMap A) (x : Id) (v : A) (y : Id) (w : A) (z : Id)
→ x ≢ y → (ρ , x ↦ v , y ↦ w) z ≡ (ρ , y ↦ w , x ↦ v) z
+ update-permute′′ {A} ρ x v y w z x≢y with yx →≟ (ρ , x ↦ v , y ↦ w) z | y ≟ z
+ ... | yes ≡x≡z | yes y≡z = ⊥-elim (ρx≢y ,(trans yx≡z ↦(sym w , x ↦ v) zy≡z)))
update-permute′′ {A} ρ x v y w... z| x≢y with x ≟ z | y ≟ z
- ... | yes x≡z | yes y≡z = ⊥-elim (x≢y (trans x≡z (sym y≡z)))
- ... | no x≢z | yes y≡z rewrite y≡z = sym (update-eq′ ρ z w)
... | yes x≡z | no y≢z rewrite x≡z = update-eq′ ρ z v
... | no x≢z | no y≢z = trans (update-neq ρ x v z x≢z) (sym (update-neq ρ y w z y≢z))
{% endraw %}
@@ -4663,266 +4650,266 @@ map with elements of type `A` is simply a total map with elements
of type `Maybe A` and default element `nothing`.
{% raw %}
-PartialMap : Set → Set
PartialMap A = TotalMap (Maybe A)
{% endraw %}
{% raw %}
-module PartialMap where
{% endraw %}
{% raw %}
- ∅ : ∀ {A} → PartialMap A
∅ = TotalMap.always nothing
{% endraw %}
{% raw %}
- infixl 15 _,_↦_
_,_↦_ : ∀ {A} (ρ : PartialMap A) (x : Id) (v : A) → PartialMap A
ρ , x ↦ v = TotalMap._,_↦_ ρ x (just v)
{% endraw %}
@@ -4930,1161 +4917,1161 @@ of type `Maybe A` and default element `nothing`.
We now lift all of the basic lemmas about total maps to partial maps.
{% raw %}
- apply-∅ : ∀ {A} → (x : Id) → (∅ {A} x) ≡ nothing
apply-∅ x = TotalMap.apply-always nothing x
{% endraw %}
{% raw %}
- update-eq : ∀ {A} (ρ : PartialMap A) (x : Id) (v : A)
+ → (ρ , x ↦ v) x ≡ just v
+ update-eq ρ x v = TotalMap.update-eq ρ x : Id)(just (v : A)
- →
+
+{% raw %}
+ update-neq (ρ , x ↦ v) x ≡ just: v∀
- update-eq {A} (ρ x: v =PartialMap TotalMap.update-eqA) ρ (x : Id) (v : A) (y (just: vId)
-{% endraw %}
-
-{% raw %}
- update-neq→ x ≢ y → (ρ , x ↦ v) y ≡ ρ :y
+ update-neq ∀ {A} (ρ :x PartialMapv A)y x≢y (x= : Id) (v : A) (y :TotalMap.update-neq Id)ρ x
- → x ≢ y → (ρ , x ↦ v) y ≡ ρ y
- update-neq ρ x v y x≢y = TotalMap.update-neq ρ x (just v) y x≢y
{% endraw %}
{% raw %}
- update-shadow : ∀ {A} (ρ : PartialMap A) (x : Id) (v w : A)
→ (ρ , x ↦ v , x ↦ w) ≡ (ρ , x ↦ w)
update-shadow ρ x v w = TotalMap.update-shadow ρ x (just v) (just w)
+{% endraw %}
+
+{% raw %}
+ update-same ρ: x∀ v w{A} = TotalMap.update-shadow (ρ x (just v) (just w)
-{% endraw %}
-
-{% raw %}
- update-same : ∀PartialMap {A) (x : Id) (v : A)
+ → ρ x ≡ just v
+ → (ρ , x ↦ v}) (≡ ρ
+ update-same :ρ PartialMap A) (x :v Id) (v : A)
- → ρ x ≡ just v
- → (ρ , x ↦ v) ≡ ρ
- update-same ρ x v ρx≡v rewrite sym ρx≡v = TotalMap.update-same ρ x
{% endraw %}
{% raw %}
- update-permute : ∀ {A} (ρ : PartialMap A) (x : Id) (v : A) (y : Id) (w : A)
→ x ≢ y → (ρ , x ↦ v , y ↦ w) ≡ (ρ , y ↦ w , x ↦ v)
update-permute ρ x v y w x≢y = TotalMap.update-permute ρ x (just v) y (just w) x≢y
{% endraw %}
diff --git a/out/Stlc.md b/out/Stlc.md
index 249d5263..5a3194d0 100644
--- a/out/Stlc.md
+++ b/out/Stlc.md
@@ -7,233 +7,234 @@ permalink : /Stlc
This chapter defines the simply-typed lambda calculus.
## Imports
+
{% raw %}
-open import Maps using (Id; id; _≟_; PartialMap; module PartialMap)
open PartialMap using (∅) renaming (_,_↦_ to _,_∶_)
open import Data.StringData.Nat using (Stringℕ)
open import import Data.Maybe using (Maybe; just; nothing)
open import import Relation.Nullary using (Dec; yes; no)
open import import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl)
{% endraw %}
@@ -244,63 +245,71 @@ This chapter defines the simply-typed lambda calculus.
Syntax of types and terms.
{% raw %}
-infixr 20 _⇒_
data Type : Type : Set where
𝔹 : Type
_⇒_ : Type :→ Type → Type → Type
infixl 20 _·_
infix 15 λ[_∶_]_
infix 15 if_then_else_
data Term : Term : Set where
var : Id → : Id → Term
λ[_∶_]_ : Id → : IdType → TypeTerm → Term → Term
_·_ : Term :→ Term → Term → Term
true : Term : Term
false : Term
if_then_else_ : Term :→ Term → Term → Term → Term
{% endraw %}
Example terms.
{% raw %}
-f x : Id
f = id "f"0
x = id "x"1
not two : Term
not = λ[ x ∶ 𝔹 ] (if var x then var xfalse thenelse false else true)
two = λ[ f ∶ 𝔹 ⇒ 𝔹 ] λ[ 𝔹x ⇒∶ 𝔹 ] λ[ x ∶ 𝔹 ] var f · (var f f· · (var f · var x)
{% endraw %}
@@ -761,130 +762,130 @@ Example terms.
## Values
{% raw %}
-data Value : Term → Set Term → Set where
value-λ : ∀ {x A N} → Value N} → Value (λ[ x ∶ A ] N)
value-true : Value true
value-false : Value false
{% endraw %}
@@ -892,645 +893,645 @@ Example terms.
## Substitution
{% raw %}
-_[_∶=_] : Term → Id → Term → Term
(var x′) [ x ∶= x′)V ] [with x ∶= V≟ ] withx′
+... x| ≟ x′
-... | yes _ = V
... | no _ = var x′
+(λ[ var x′
-(λ[ x′∶ A′ ] N′) ∶[ A′x ]∶= N′)V ] [with x ∶= V≟ ] withx′
+... x| ≟yes x′
-..._ |= λ[ yesx′ _∶ =A′ λ[ x′ ∶ A′ ] N′
... | no _ = λ[ nox′ _ =∶ A′ λ[] x′(N′ ∶[ A′x ]∶= (N′ [ x ∶= V ])
(L′ · M′) [ x ∶= M′)V ] [= x ∶= (L′ V[ ]x = (L′ [ x ∶= V ]) · (M′ V[ ])x ·∶= (M′ [ x ∶= V ])
(true) [ x ∶= V ] [= x ∶= V ] = true
(false) [ x ∶= V ] [= x ∶= V ] = false
(if L′ then M′ L′else thenN′) M′[ elsex ∶= N′)V ] [= xif ∶= V(L′ ][ =x if∶= (L′ [ x ∶= V ]) then (M′ [ thenx ∶= (M′ [ x ∶= V ]) else (N′ [ elsex ∶= (N′ [ x ∶= V ])
{% endraw %}
@@ -1538,1818 +1539,1879 @@ Example terms.
## Reduction rules
{% raw %}
-infix 10 _⟹_
data _⟹_ : Term _⟹_ : Term → Term → Set Term → Setwhere
+ β⇒ where
- β⇒: ∀ {x A N :V} ∀→ {x A NValue V} → Value V →
(λ[ x ∶ A ] N) x· ∶V A⟹ ]N N)[ ·x V∶= ⟹V N [ x ∶= V ]
γ⇒₁ : ∀ {L L' M} ∀→ {
+ L L' M}⟹ →L' →
L ⟹ L'· →
- LM ⟹ L' · ·M M ⟹ L' · M
γ⇒₂ : ∀ {V M M'} ∀→ {V M M'} →
Value V →
M ⟹ M' →
+ V M' →
- V · M ⟹ V · M'
+ β𝔹₁ ·: M'
- β𝔹₁ : ∀ {M N} →
if true then M else N ⟹ M else N ⟹ M
β𝔹₂ : ∀ {M N} →
if false then falseM thenelse N ⟹ MN else N ⟹ N
γ𝔹 : ∀ {L L' M N} {L L' M N} →
L ⟹ L' →
if L then M else N ⟹ Mif elseL' N ⟹then if L' then M else N
{% endraw %}
## Reflexive and transitive closure
+
{% raw %}
-Relinfix 10 _⟹*_ : Set →
+infixr Set₁
-Rel2 _⟹⟨_⟩_ A = A
+infix 3 → A →_∎ Set
infixl 10 _>>_
-
-data _*_⟹*_ {A : Term → Term → Set} (Rwhere
+ _∎ : Rel∀ M A)→ :M Rel⟹* M A where
⟨⟩_⟹⟨_⟩_ : ∀ :L ∀ {M x : AN} → L →⟹ (RM *)→ M x⟹* x
- ⟨_⟩N :→ L ⟹* ∀N {x y : A} → R
+
+reduction₁ x: y →not (R· *)true x y⟹* false
+reduction₁ =
+ not · true
_>>_⟹⟨ :β⇒ ∀value-true {x y z : A} → (R *) x y → (R *) y z → (R *)⟩
+ if xtrue zthen false else true
+ ⟹⟨ β𝔹₁ ⟩
+ false
+ ∎
infixreduction₂ 10 _⟹*_
-
-_⟹*_ : Reltwo Term· not · true ⟹* true
_⟹*_reduction₂ =
+ two · not · true
+ ⟹⟨ γ⇒₁ (_⟹_) *
-{% endraw %}
-
-## Notation for setting out reductions
-
-
{% raw %}
-infixr 2 _⟹⟨_⟩_
-infix 3 _∎β⇒ value-λ) ⟩
-
-_⟹⟨_⟩_(λ[ :x ∀∶ L𝔹 {M] N}not →· L(not ⟹· M → M ⟹* N → L ⟹*var N
-Lx)) ⟹⟨· L⟹Mtrue
+ ⟹⟨ ⟩β⇒ M⟹*N = ⟨ L⟹M ⟩value-true >> M⟹*N⟩
-
-_∎not · :(not ∀· M → M ⟹*true) M
-M⟹⟨ ∎ =γ⇒₂ ⟨⟩
-{% endraw %}
-
-## Example reduction derivations
-
-
{% raw %}
-reduction₁ :value-λ (β⇒ value-true) ⟩
+ not · (if true then false else true)
+ ⟹⟨ γ⇒₂ notvalue-λ · true ⟹* false
-reduction₁ =β𝔹₁ ⟩
not · truefalse
⟹⟨ β⇒ value-truevalue-false ⟩
if true then false then false else true
+ ⟹⟨ else true
- ⟹⟨ β𝔹₁ ⟩
- false
- ∎
-
-reduction₂ : two · not · true ⟹* true
-reduction₂ =
- two · not · true
- ⟹⟨ γ⇒₁ (β⇒ value-λ) ⟩
- (λ[ x ∶ 𝔹 ] not · (not · var x)) · true
- ⟹⟨ β⇒ value-true ⟩
- not · (not · true)
- ⟹⟨ γ⇒₂ value-λ (β⇒ value-true) ⟩
- not · (if true then false else true)
- ⟹⟨ γ⇒₂ value-λ β𝔹₁ ⟩
- not · false
- ⟹⟨ β⇒ value-false ⟩
- if false then false else true
- ⟹⟨ β𝔹₂ ⟩
true
∎
{% endraw %}
+Much of the above, though not all, can be filled in using C-c C-r and C-c C-s.
+
+
+
## Type rules
{% raw %}
-Context : Set
+Context = PartialMap Type
+
+infix 10 _⊢_∶_
+
+data _⊢_∶_ : Context → Term → Type → Set where
+ Ax : ∀ {Γ x A} →
+ Γ x ≡ just A →
+ Γ ⊢ var x ∶ A
+ ⇒-I : ∀ {Γ x N A B} →
+ Γ , x ∶ A ⊢ N ∶ B →
+ Γ ⊢ λ[ x ∶ A ] N ∶ A ⇒ B
+ ⇒-E : ∀ {Γ L M A B} →
+ Γ ⊢ L ∶ A ⇒ B →
+ Γ ⊢ M ∶ A →
+ Γ ⊢ L · M ∶ B
+ 𝔹-I₁ : Set
-Context∀ ={Γ} →
+ Γ PartialMap⊢ true ∶ 𝔹 Type
-
-infix𝔹-I₂ 10: ∀ {Γ} _⊢_∶_→
-
-dataΓ _⊢_∶_⊢ false ∶ :𝔹
+ 𝔹-E Context: →∀ Term{Γ L →M TypeN A} → Set where
- AxΓ :⊢ ∀L {∶ 𝔹 →
+ Γ x⊢ A}M ∶ A →
Γ x⊢ ≡N just∶ A
Γ ⊢ var x ∶ A
- ⇒-I : ∀ {Γ x N A B} →
- Γ , x ∶ A ⊢ N ∶ B →
- Γ ⊢ λ[ x ∶ A ] N ∶ A ⇒ B
- ⇒-E : ∀ {Γ L M A B} →
- Γ ⊢ L ∶ A ⇒ B →
- Γ ⊢ M ∶ A →
- Γ ⊢ L · M ∶ B
- 𝔹-I₁ : ∀ {Γ} →
- Γ ⊢ true ∶ 𝔹
- 𝔹-I₂ : ∀ {Γ} →
- Γ ⊢ false ∶ 𝔹
- 𝔹-E : ∀ {Γ L M N A} →
- Γ ⊢ L ∶ 𝔹 →
- Γ ⊢ M ∶ A →
- Γ ⊢ N ∶ A →
- Γ ⊢ if L then M else N ∶ A
{% endraw %}
@@ -3894,205 +3464,205 @@ Example terms.
## Example type derivations
{% raw %}
-typing₁ : ∅ ⊢ not ∶ 𝔹 ⇒ 𝔹
typing₁ = ⇒-I (𝔹-E (Ax refl) 𝔹-I₂ 𝔹-I₁)
typing₂ : ∅ ⊢ two ∶ (𝔹 ⇒ 𝔹) ⇒ 𝔹 ⇒ 𝔹
typing₂ = ⇒-I (⇒-I (⇒-E (Ax refl) (⇒-E (Ax refl) (Ax refl))))
{% endraw %}
@@ -4103,20 +3673,19 @@ We start with the declaration:
typing₁ : ∅ ⊢ not ∶ 𝔹 ⇒ 𝔹
typing₁ = ?
-Typing C-L (control L) causes Agda to create a hole and tell us its
-expected type.
+Typing C-l causes Agda to create a hole and tell us its expected type.
typing₁ = { }0
?0 : ∅ ⊢ not ∶ 𝔹 ⇒ 𝔹
-Now we fill in the hole by typing C-R (control R). Agda observes that
+Now we fill in the hole by typing C-c C-r. Agda observes that
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.
typing₁ = ⇒-I { }0
?0 : ∅ , x ∶ 𝔹 ⊢ if var x then false else true ∶ 𝔹
-Again we fill in the hole by typing 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
`𝔹-E` rule in turn takes three arguments, which Agda leaves as holes.
@@ -4125,10 +3694,12 @@ outermost term is now `if_then_else_`, which is typed using `𝔹-E`. The
?1 : ∅ , x ∶ 𝔹 ⊢ false ∶ 𝔹
?2 : ∅ , x ∶ 𝔹 ⊢ true ∶ 𝔹
-Again we fill in the three holes by typing 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
`𝔹-I₁` respectively. The `Ax` rule in turn takes an argument, to show
that `(∅ , x ∶ 𝔹) x = just 𝔹`, which can in turn be specified with a
hole. After filling in all holes, the term is as above.
+The entire process can be automated using Agsy, invoked with C-c C-a.
+
diff --git a/out/StlcProp.md b/out/StlcProp.md
index cf7cf557..165f4eef 100644
--- a/out/StlcProp.md
+++ b/out/StlcProp.md
@@ -295,7 +295,7 @@ theorem.
>
Maps.PartialMap (∅; apply-∅; update-permute) (_,_↦_ to
_,_∶_):
Term →
Type (λ[ x
∶ A
] A
⇒ canonical
true for
𝔹
@@ -530,7 +530,7 @@ while for boolean types they are values `true` and `false`.
>canonical false for
𝔹
@@ -572,11 +572,11 @@ while for boolean types they are values `true` and `false`.
>→ ∅ ⊢ L
∶ →
Value (Ax (⇒-I )
value-λ (⇒-E canonicalFormsLemma
𝔹-I₁ value-true canonicalFormsLemma
𝔹-I₂ value-false (𝔹-E :
Term M
⟹ →
Value →
∅ ⊢ M
∶ (Ax (⇒-I done
value-λ
@@ -1065,7 +1065,7 @@ This completes the proof.
> (⇒-E (γ⇒₁ (γ⇒₂ (β⇒ progress
𝔹-I₁ done
value-true
@@ -1290,7 +1290,7 @@ This completes the proof.
>progress 𝔹-I₂ done
value-false
@@ -1313,7 +1313,7 @@ This completes the proof.
> (𝔹-E (γ𝔹 steps
β𝔹₁
@@ -1459,78 +1459,87 @@ This completes the proof.
>steps β𝔹₂
{% endraw %}
+This code reads neatly in part because we look at the
+`steps` option before the `done` option. We could, of course,
+look at it the other way around, but then the `...` abbreviation
+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
+(here `steps`) before the hard case (her `done`).
+If you have two hard cases, you will have to expand out `...`
+or introduce subsidiary functions.
+
#### Exercise: 3 stars, optional (progress_from_term_ind)
Show that progress can also be proved by induction on terms
instead of induction on typing derivations.
{% raw %}
-postulate
progress′ : ∀ M {A} → ∅ ⊢ M ∶ A → Progress M
{% endraw %}
@@ -1538,654 +1547,650 @@ instead of induction on typing derivations.
## Preservation
The other half of the type soundness property is the preservation
-of types during reduction. For this, we need to develop some
+of types during reduction. For this, we need to develop
technical machinery for reasoning about variables and
substitution. Working from top to bottom (from the high-level
property we are actually interested in to the lowest-level
-technical lemmas that are needed by various cases of the more
-interesting proofs), the story goes like this:
+technical lemmas), the story goes like this:
- The _preservation theorem_ is proved by induction on a typing
- derivation, pretty much as we did in the [Stlc]({{ "Stlc" | 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
- `red` 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
- does. So we prove a...
+ does. So we prove a ...
- _substitution lemma_, stating that substituting a (closed)
- term `s` for a variable `x` in a term `t` preserves the type
- of `t`. The proof goes by induction on the form of `t` and
+ term `V` for a variable `x` in a term `N` preserves the type
+ of `N`. The proof goes by induction on the form of `N` and
requires looking at all the different cases in the definition
- of substitition. This time, the tricky cases are the ones for
+ of substitition. The tricky cases are the ones for
variables and for function abstractions. In both cases, we
- discover that we need to take a term `s` that has been shown
- to be well-typed in some context `\Gamma` and consider the same
- term `s` in a slightly different context `\Gamma'`. For this
+ discover that we need to take a term `V` that has been shown
+ to be well-typed in some context `Γ` and consider the same
+ term in a different context `Γ′`. For this
we prove a...
- _context invariance_ lemma, showing that typing is preserved
- under "inessential changes" to the context `\Gamma`---in
- particular, changes that do not affect any of the free
- variables of the term. And finally, for this, we need a
- careful definition of...
+ under "inessential changes" to the context---a term `M`
+ well typed in `Γ` is also well typed in `Γ′`, so long as
+ all the free variables of `M` appear in both contexts.
+ And finally, for this, we need a careful definition of ...
- - the _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
function abstraction binding a variable of the same name.
To make Agda happy, we need to formalize the story in the opposite
-order...
+order.
### Free Occurrences
-A variable `x` _appears free in_ a term `M` if `M` contains some
-occurrence of `x` that is not under an abstraction over `x`.
+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.
For example:
- - `y` appears free, but `x` does not, in `λ[ x ∶ (A ⇒ B) ] x · y`
- - both `x` and `y` appear free in `(λ[ x ∶ (A ⇒ B) ] x · y) · x`
- - no variables appear free in `λ[ x ∶ (A ⇒ B) ] (λ[ y ∶ A ] x · y)`
+ - `x` appears free, but `f` does not, in `λ[ f ∶ (𝔹 ⇒ 𝔹) ] var f · var x`
+ - both `f` and `x` appear free in `(λ[ f ∶ (𝔹 ⇒ 𝔹) ] var f · var x) · var f`;
+ note that `f` appears both bound and free in this term
+ - no variables appear free in `λ[ f ∶ (𝔹 ⇒ 𝔹) ] λ[ x ∶ 𝔹 ] var f · var x`
Formally:
{% raw %}
-data _∈_ : Id → Term → Set where
free-var : ∀ {x} → x ∈ (var x)
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 ∈ M → x ∈ (L · M)
free-if₁ : ∀ {x L M N} → x ∈ L → x ∈ (if L then M else N)
free-if₂ : ∀ {x L M N} → x ∈ M → x ∈ (if L then M else N)
free-if₃ : ∀ {x L M N} → x ∈ N → x ∈ (if L then M else N)
{% endraw %}
@@ -2193,85 +2198,752 @@ Formally:
A term in which no variables appear free is said to be _closed_.
{% raw %}
-closed_∉_ : TermId → Term → Set
closedx ∉ M = ∀ {x} → ¬ (x ∈ M)
+
+closed : Term → Set
+closed M = ∀ {x} → x ∉ M
+{% endraw %}
+
+Here are proofs corresponding to the first two examples above.
+
+
{% raw %}
+f≢x : f ≢ x
+f≢x ()
+
+example-free₁ : x ∈ (λ[ f ∶ (𝔹 ⇒ 𝔹) ] var f · var x)
+example-free₁ = free-λ f≢x (free-·₂ free-var)
+
+example-free₂ : f ∉ (λ[ f ∶ (𝔹 ⇒ 𝔹) ] var f · var x)
+example-free₂ (free-λ f≢f _) = f≢f refl
+{% endraw %}
+
+
+#### Exercise: 1 star (free-in)
+Prove formally the remaining examples given above.
+
+
{% raw %}
+postulate
+ example-free₃ : x ∈ ((λ[ f ∶ (𝔹 ⇒ 𝔹) ] var f · var x) · var f)
+ example-free₄ : f ∈ ((λ[ f ∶ (𝔹 ⇒ 𝔹) ] var f · var x) · var f)
+ example-free₅ : x ∉ (λ[ f ∶ (𝔹 ⇒ 𝔹) ] λ[ x ∶ 𝔹 ] var f · var x)
+ example-free₆ : f ∉ (λ[ f ∶ (𝔹 ⇒ 𝔹) ] λ[ x ∶ 𝔹 ] var f · var x)
{% endraw %}
-#### Exercise: 1 star (free-in)
-If the definition of `_∈_` is not crystal clear to
-you, it is a good idea to take a piece of paper and write out the
-rules in informal inference-rule notation. (Although it is a
-rather low-level, technical definition, understanding it is
-crucial to understanding substitution and its properties, which
-are really the crux of the lambda-calculus.)
+Although `_∈_` may apperar to be a low-level technical definition,
+understanding it is crucial to understanding the properties of
+substitution, which are really the crux of the lambda calculus.
### Substitution
+
To prove that substitution preserves typing, we first need a
technical lemma connecting free variables and typing contexts: If
a variable `x` appears free in a term `M`, and if we know `M` is
@@ -2279,115 +2951,115 @@ well typed in context `Γ`, then it must be the case that
`Γ` assigns a type to `x`.
{% raw %}
-freeLemma : ∀ {x M A Γ} → x ∈ M → Γ ⊢ M ∶ A → ∃ λ B → Γ x ≡ just B
{% endraw %}
@@ -2422,454 +3094,454 @@ _Proof_: We show, by induction on the proof that `x` appears
`_≟_`, noting that `x` and `y` are different variables.
{% raw %}
-freeLemma free-var (Ax Γx≡justA) = (_ , Γx≡justA)
freeLemma (free-·₁ x∈L) (⇒-E ⊢L ⊢M) = freeLemma x∈L ⊢L
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∈M) (𝔹-E ⊢L ⊢M ⊢N) = freeLemma x∈M ⊢M
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
... | Γx=justC with y ≟ x
... | yes y≡x = ⊥-elim (y≢x y≡x)
... | no _ = Γx=justC
{% endraw %}
@@ -2884,362 +3556,362 @@ the empty context is closed (it has no free variables).
#### Exercise: 2 stars, optional (∅⊢-closed)
{% raw %}
-postulate
∅⊢-closed : ∀ {M A} → ∅ ⊢ M ∶ A → closed M
{% endraw %}
{% raw %}
-contradiction : ∀ {X : Set} → ∀ {x : X} → ¬ (_≡_ {A = Maybe X} (just x) nothing)
contradiction ()
∅⊢-closed′ : ∀ {M A} → ∅ ⊢ M ∶ A → closed M
∅⊢-closed′ {M} {A} ⊢M {x} x∈M with freeLemma x∈M ⊢M
... | (B , ∅x≡justB) = contradiction (trans (sym ∅x≡justB) (apply-∅ x))
{% endraw %}
@@ -3253,144 +3925,144 @@ that appear free in `M`. In fact, this is the only condition that
is needed.
{% raw %}
-contextLemma : ∀ {Γ Γ′ M A}
→ (∀ {x} → x ∈ M → Γ x ≡ Γ′ x)
→ Γ ⊢ M ∶ A
→ Γ′ ⊢ M ∶ A
{% endraw %}
@@ -3438,604 +4110,604 @@ _Proof_: By induction on the derivation of
hence the desired result follows from the induction hypotheses.
{% raw %}
-contextLemma Γ~Γ′ (Ax Γx≡justA) rewrite (Γ~Γ′ free-var) = Ax Γx≡justA
contextLemma {Γ} {Γ′} {λ[ x ∶ A ] N} Γ~Γ′ (⇒-I ⊢N) = ⇒-I (contextLemma Γx~Γ′x ⊢N)
where
Γx~Γ′x : ∀ {y} → y ∈ N → (Γ , x ∶ A) y ≡ (Γ′ , x ∶ A) y
Γx~Γ′x {y} y∈N with x ≟ y
... | yes refl = refl
... | no x≢y = Γ~Γ′ (free-λ x≢y y∈N)
contextLemma Γ~Γ′ (⇒-E ⊢L ⊢M) = ⇒-E (contextLemma (Γ~Γ′ ∘ free-·₁) ⊢L) (contextLemma (Γ~Γ′ ∘ free-·₂) ⊢M)
contextLemma Γ~Γ′ 𝔹-I₁ = 𝔹-I₁
contextLemma Γ~Γ′ 𝔹-I₂ = 𝔹-I₂
contextLemma Γ~Γ′ (𝔹-E ⊢L ⊢M ⊢N)
= 𝔹-E (contextLemma (Γ~Γ′ ∘ free-if₁) ⊢L) (contextLemma (Γ~Γ′ ∘ free-if₂) ⊢M) (contextLemma (Γ~Γ′ ∘ free-if₃) ⊢N)
Γ~Γ′
-preservation-[∶=] 𝔹-I₁{x} ⊢Vx∈V = 𝔹-I₁
-preservation-[∶=]⊥-elim 𝔹-I₂ ⊢V = 𝔹-I₂
-preservation-[∶=] (𝔹-Ex∉V ⊢L ⊢M ⊢Nx∈V)
+ where
+ x∉V : ¬ (x ∈ V)
+ x∉V = ∅⊢-closed ⊢V {x}
+
+just-injective : =∀
- 𝔹-E {X : Set} {x y : X} → _≡_ {A = Maybe X} (preservation-[∶=]just ⊢L ⊢Vx) (preservation-[∶=]just ⊢M ⊢Vy) (→ x ≡ y
+just-injective refl = refl
+{% endraw %}
+
+
{% raw %}
+preservation-[∶=] ⊢N{_} {x} (Ax {_} {x′} [Γ,x∶A]x′≡B) ⊢V with x ≟ x′
+...| yes x≡x′ rewrite just-injective [Γ,x∶A]x′≡B = weaken-closed ⊢V
+...| no x≢x′ = Ax [Γ,x∶A]x′≡B
+preservation-[∶=] {Γ} {x} {A} {λ[ x′ ∶ A′ ] N′} {.A′ ⇒ B′} {V} (⇒-I ⊢N′) ⊢V with x ≟ x′
+...| yes x≡x′ rewrite x≡x′ = contextLemma Γ′~Γ (⇒-I ⊢N′)
+ where
+ Γ′~Γ : ∀ {y} → y ∈ (λ[ x′ ∶ A′ ] N′) → (Γ , x′ ∶ A) y ≡ Γ y
+ Γ′~Γ {y} (free-λ x′≢y y∈N′) with x′ ≟ y
+ ...| yes x′≡y = ⊥-elim (x′≢y x′≡y)
+ ...| no _ = refl
+...| no x≢x′ = ⇒-I ⊢N′V
+ where
+ x′x⊢N′ : Γ , x′ ∶ A′ , x ∶ A ⊢ N′ ∶ B′
+ x′x⊢N′ rewrite update-permute Γ x A x′ A′ x≢x′ = ⊢N′
+ ⊢N′V : (Γ , x′ ∶ A′) ⊢ N′ [ x ∶= V ] ∶ B′
+ ⊢N′V = preservation-[∶=] x′x⊢N′ ⊢V
+preservation-[∶=] (⇒-E ⊢L ⊢M) ⊢V = ⇒-E (preservation-[∶=] ⊢L ⊢V) (preservation-[∶=] ⊢M ⊢V)
+preservation-[∶=] 𝔹-I₁ ⊢V = 𝔹-I₁
+preservation-[∶=] 𝔹-I₂ ⊢V = 𝔹-I₂
+preservation-[∶=] (𝔹-E ⊢L ⊢M ⊢N) ⊢V =
+ 𝔹-E (preservation-[∶=] ⊢L ⊢V) (preservation-[∶=] ⊢M ⊢V) (preservation-[∶=] ⊢N ⊢V)
{% endraw %}
@@ -5645,95 +6317,95 @@ is also a closed term with type `A`. In other words, small-step
reduction preserves types.
{% raw %}
-preservation : ∀ {M N A} → ∅ ⊢ M ∶ A → M ⟹ N → ∅ ⊢ N ∶ A
{% endraw %}
@@ -5770,435 +6442,435 @@ _Proof_: By induction on the derivation of `\vdash t : T`.
follows directly from the induction hypothesis.
{% raw %}
-preservation (Ax x₁) ()
preservation (⇒-I ⊢N) ()
preservation (⇒-E (⇒-I ⊢N) ⊢V) (β⇒ valueV) = preservation-[∶=] ⊢N ⊢V
preservation (⇒-E ⊢L ⊢M) (γ⇒₁ L⟹L′) with preservation ⊢L L⟹L′
...| ⊢L′ = ⇒-E ⊢L′ ⊢M
preservation (⇒-E ⊢L ⊢M) (γ⇒₂ valueL M⟹M′) with preservation ⊢M M⟹M′
...| ⊢M′ = ⇒-E ⊢L ⊢M′
preservation 𝔹-I₁ ()
preservation 𝔹-I₂ ()
preservation (𝔹-E 𝔹-I₁ ⊢M ⊢N) β𝔹₁ = ⊢M
preservation (𝔹-E 𝔹-I₂ ⊢M ⊢N) β𝔹₂ = ⊢N
preservation (𝔹-E ⊢L ⊢M ⊢N) (γ𝔹 L⟹L′) with preservation ⊢L L⟹L′
...| ⊢L′ = 𝔹-E ⊢L′ ⊢M ⊢N
{% endraw %}