@@ -3170,891 +3170,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 ↦ w) ≡ (ρ , y ↦ w , x ↦ v)
update-permute′ {A} ρ x v y w x≢y = extensionality lemma
where
lemma : ∀ z → (ρ , x ↦ v , y ↦ w) z ≡ (ρ , y ↦ w , x ↦ v) z
lemma z with x ≟ z | y ≟ z
... | yes refl | yes refl = ⊥-elim (x≢y refl)
... | no x≢z | yes refl = sym (update-eq′ ρ z w)
... | yes refl | no y≢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 %}
@@ -4062,595 +4062,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 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 +4663,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 10015 _,_↦_
_,_↦_ : :∀ ∀ {A} (ρ : : PartialMap A) (x : : Id) (v : : A) → → PartialMap A
ρ , ,x x↦ ↦v v= = TotalMap._,_↦_ ρ ρx x (just v)
{% endraw %}
@@ -4930,1161 +4930,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 x↦ ↦ v) x x≡ ≡ just v
update-eq ρ ρx xv v= = TotalMap.update-eq ρ ρx x (just v)
{% endraw %}
{% raw %}
- update-neq : :∀ ∀ {A} (ρ : : PartialMap A) (x : : Id) (v : : A) (y : : Id)
→ x x≢ ≢y y→ → (ρ , ,x x↦ ↦ v) y y≡ ≡ρ ρ y
update-neq ρ ρx xv vy y x≢y = = TotalMap.update-neq ρ ρx x (just v) y y x≢y
{% endraw %}
{% raw %}
- update-shadow : :∀ ∀ {A} (ρ : : PartialMap A) (x : : Id) (v w w: : A)
→ (ρ , ,x x↦ ↦v v, ,x x↦ ↦ w) ≡ ≡ (ρ , ,x x↦ ↦ w)
update-shadow ρ ρx xv vw w= = TotalMap.update-shadow ρ ρx x (just v) (just w)
{% endraw %}
{% raw %}
- update-same : :∀ ∀ {A} (ρ : : PartialMap A) (x : : Id) (v : : A)
→ ρ ρx x≡ ≡ just v
→ (ρ , ,x x↦ ↦ v) ≡ ≡ ρ
update-same ρ ρx xv 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 x≢ ≢y y→ → (ρ , ,x x↦ ↦v v, ,y y↦ ↦ w) ≡ ≡ (ρ , ,y y↦ ↦w w, ,x x↦ ↦ v)
update-permute ρ ρx xv vy yw w x≢y = = TotalMap.update-permute ρ ρx x (just v) y y (just w) x≢y
{% endraw %}
diff --git a/out/Stlc.md b/out/Stlc.md
index ad4fa3d3..2603053a 100644
--- a/out/Stlc.md
+++ b/out/Stlc.md
@@ -7,8 +7,7 @@ permalink : /Stlc
This chapter defines the simply-typed lambda calculus.
## Imports
-
-
+{% raw %}
open; PartialMap;module PartialMap)open PartialMap (∅;) _,_↦_)
-openrenaming import(_,_↦_ to Data.String_,_∶_)
+open usingimport Data.String using (String)
open import Data.Empty using (⊥; ⊥-elim)
-open import Data.Maybe using (Maybe; just; nothing)
open import Data.NatRelation.Nullary using (ℕDec; sucyes; zero; _+_no)
open import Data.BoolRelation.Binary.PropositionalEquality using (Bool_≡_; true; false_≢_; if_then_else_)
-open import Relation.Nullary using (Dec; yes; no)
-open import Relation.Nullary.Decidable using (⌊_⌋)
-open import Relation.Binary.PropositionalEquality as P using (_≡_; _≢_; refl)
-open import Relation.Binary using (Preorder)
-import Relation.Binary.PreorderReasoning as PreorderReasoning
-
-
-
-
-
+{% endraw %}
## Syntax
-Syntax of types and terms. All source terms are labeled with $ᵀ$.
+Syntax of types and terms.
-
-
-{% raw %}
+infixr 10020 _⇒_
-infixl 100 _·ᵀ_
data Type : Set where
𝔹 : Type
_⇒_ : Type → Type → Type
infixl 20 _·_
+infix 15 λ[_∶_]_
+infix 15 if_then_else_
+
+data Term : Set where
varᵀvar : Id → Term
λᵀ_∈_⇒_λ[_∶_]_ : Id → Type → Term → Term
_·ᵀ__·_ : Term → Term → Term
trueᵀtrue : Term
falseᵀfalse : Term
ifᵀ_then_else_if_then_else_ : Term → Term → Term → Term
+{% endraw %}
-
-
-Some examples.
-
-
-{% raw %}
+f x y : Id
f = id "f"
x = id "x"
-y = id "y"
I[𝔹]not I[𝔹⇒𝔹]two K[𝔹][𝔹] not[𝔹] : Term
I[𝔹] not = (λᵀλ[ x ∈∶ 𝔹 ⇒] (varᵀif var x))
-I[𝔹⇒𝔹] = (λᵀ f ∈ (𝔹 ⇒ 𝔹) ⇒ (λᵀ x ∈ 𝔹 ⇒ ((varᵀ f) ·ᵀ (varᵀ x))))
-K[𝔹][𝔹] = (λᵀ x ∈ 𝔹 ⇒ (λᵀ y ∈ 𝔹 ⇒ (varᵀ x)))
-not[𝔹] = (λᵀ x ∈ 𝔹 ⇒ (ifᵀ (varᵀ x) then falseᵀfalse else trueᵀ))true)
-
-
+
two = λ[ f ∶ 𝔹 ⇒ 𝔹 ] λ[ x ∶ 𝔹 ] var f · (var f · var x)
+{% endraw %}
## Values
-
-
-{% raw %}
+data valueValue : Term → Set where
value-λᵀ value-λ : ∀ {x A N} → valueValue (λᵀλ[ x ∈∶ A ⇒] N)
value-trueᵀ value-true : valueValue (trueᵀ)true
value-falseᵀvalue-false : valueValue (falseᵀ)false
-
-
+{% endraw %}
## Substitution
-
-
-_[_:=_]{% raw %}
+_[_∶=_] : Term → Id → Term → Term
(varᵀvar x′) [ x :=∶= V ] with x ≟ x′
... | yes _ = V
... | no _ = varᵀvar x′
(λᵀλ[ x′ ∈∶ A′ ⇒ N′) [ x := V ] N′) [ x ∶= V ] with x ≟ x′
... | yes _ = λᵀλ[ x′ ∈∶ A′ ⇒] N′
... | no _ = λᵀλ[ x′ ∈∶ A′ ⇒ (N′ [ x := V ] (N′ [ x ∶= V ])
(L′ ·ᵀ· M′) [ x :=∶= V ] = (L′ [ x :=∶= V ]) ·ᵀ· (M′ [ x :=∶= V ])
(trueᵀtrue) [ x :=∶= V ] = trueᵀtrue
(falseᵀfalse) [ x :=∶= V ] = falseᵀfalse
(ifᵀif L′ then M′ else N′) [ x :=∶= V ] = ifᵀif (L′ [ x :=∶= V ]) then (M′ [ x :=∶= V ]) else (N′ [ x :=∶= V ])
-
-
+{% endraw %}
## Reduction rules
-
-
-data{% raw %}
+infix 10 _⟹_
+
+data _⟹_ : Term → Term → Set where
+ β⇒ : ∀ {x A N V} → Value V →
+ (λ[ x ∶ A ] N) · V ⟹ N [ x ∶= V ]
+ γ⇒₁ : ∀ {L L' M} →
+ L ⟹ L' →
+ L · M ⟹ L' · M
+ γ⇒₂ : ∀ {V M M'} →
+ Value V →
+ M ⟹ M' →
+ V · M ⟹ V · M'
+ β𝔹₁ : ∀ {M N} →
+ if true then M else N ⟹ M
+ β𝔹₂ : ∀ {M N} →
+ if false then M else N ⟹ N
+ γ𝔹 : ∀ {L L' M N} →
+ L ⟹ L' →
+ if L then M else N ⟹ if L' then M else N
+{% endraw %}
+
+## Reflexive and transitive closure
+
+
{% raw %}
+Rel : Set → Set₁
+Rel A = A → A → Set
+
+infixl 10 _>>_
+
+data _* {A : Set} (R : Rel A) : Rel A where
+ ⟨⟩ : ∀ {x Term: A} → Term(R →*) Setx wherex
β⇒⟨_⟩ : ∀ {x y : A N V} → R x →y value→ V(R *) →x y
- ((λᵀ_>>_ x: ∈∀ A{x ⇒y N)z ·ᵀ: V)A} ⟹→ (NR [*) x :=y V→ ](R *)
- γ⇒₁ y z :→ ∀(R {L*) L'x M} →z
- Linfix ⟹10 L' →_⟹*_
- (L_⟹*_ : ·ᵀRel M)Term
+_⟹*_ ⟹= (L' ·ᵀ M(_⟹_)
- γ⇒₂ *
+{% endraw %}
+
+## Notation for setting out reductions
+
+
{% raw %}
+infixr 2 _⟹⟨_⟩_
+infix 3 _∎
+
+_⟹⟨_⟩_ : ∀ {V M M'} →
- value V →
- M ⟹ M' →
- (V ·ᵀ M) ⟹ (V ·ᵀ M')
- β𝔹₁ : ∀ {M N} →
- (ifᵀ trueᵀ then ML else{M N} )→ ⟹L M⟹
- β𝔹₂ M → M :⟹* ∀N {M→ N}L →⟹* N
- (ifᵀL falseᵀ⟹⟨ thenL⟹M ⟩ M⟹*N = ⟨ M elseL⟹M N)⟩ ⟹>> NM⟹*N
- γ𝔹 :_∎ ∀: {L∀ L'M → M N}⟹* →M
- L ⟹ L' →
- (ifᵀ L then M else N) ⟹ (ifᵀ L' then M else N)
-
-
-
-## Reflexive and transitive closure of a relation
-
-
-
-Rel : Set → Set₁
RelM A ∎ = A → A → Set ⟨⟩
+{% endraw %}
-
infixl{% raw %}
+reduction₁ 100: _>>_not · true ⟹* false
-
datareduction₁ _*=
+ not {A· : Set} (R : Rel A) : Rel A wheretrue
⟨⟩⟹⟨ β⇒ value-true ⟩
+ if true then false else true
+ ⟹⟨ β𝔹₁ ⟩
+ false
+ ∎
+
+reduction₂ : ∀two {x· :not A}· true ⟹* true
+reduction₂ →=
(R *) x
+
two x·
- ⟨_⟩ not · :true
+ ⟹⟨ ∀ {x y : A}γ⇒₁ → R(
β⇒ x y → (Rvalue-λ) *) x y⟩
- _>>_(λ[ x ∶ :𝔹 ∀] {xnot y· z : A} → (Rnot · var *) x)) y· →true
+ ⟹⟨ (R *) y zβ⇒ →value-true ⟩
+ not · (Rnot *· true) x z
-
-
-
-
-
-infix⟹⟨ 80γ⇒₂ _⟹*_
-
-_⟹*_value-λ (β⇒ : Term → Term → Set
-_⟹*_ = (_⟹_value-true) ⟩
+ not · (if true *then false else true)
-
-
-
-
-
-⟹*-Preorder⟹⟨ γ⇒₂ value-λ :β𝔹₁ Preorder _ _ _⟩
-⟹*-Preordernot =· recordfalse
{⟹⟨ β⇒ value-false Carrier = Term⟩
- ;if _≈_false then false = _≡_
- ; _∼_ = _⟹*_
- ; isPreorder = record
- { isEquivalence = P.isEquivalence
- ; reflexive = λ {refl → ⟨⟩}
- ; trans = _>>_
- }
- }
-
-open PreorderReasoning ⟹*-Preorder
- using (begin_; _∎) renaming (_≈⟨_⟩_ to _≡⟨_⟩_; _∼⟨_⟩_ to _⟹*⟨_⟩_)
-
-
-
-Example evaluation.
-
-
-
-example₀′ : not[𝔹] ·ᵀ trueᵀ ⟹* falseᵀ
-example₀′ =
- begin
- not[𝔹] ·ᵀ trueᵀ
- ⟹*⟨ ⟨ β⇒ value-trueᵀ ⟩ ⟩
- ifᵀ trueᵀ then falseᵀ else trueᵀtrue
⟹*⟨⟹⟨ ⟨ β𝔹₁ ⟩ ⟩
- falseᵀ
- ∎
-
-example₀ : (not[𝔹] ·ᵀ trueᵀ) ⟹* falseᵀ
-example₀ = ⟨ step₀ ⟩ >> ⟨ step₁ ⟩
- where
- M₀ M₁ M₂ : Term
- M₀ = (not[𝔹] ·ᵀ trueᵀ)
- M₁ = (ifᵀ trueᵀ then falseᵀ else trueᵀ)
- M₂ = falseᵀ
- step₀ : M₀ ⟹ M₁
- step₀ = β⇒ value-trueᵀ
- step₁ : M₁ ⟹ M₂
- step₁ = β𝔹₁
-
-example₁ : (I[𝔹⇒𝔹] ·ᵀ I[𝔹] ·ᵀ (not[𝔹] ·ᵀ falseᵀ)) ⟹* trueᵀ
-example₁ = ⟨ step₀ ⟩ >> ⟨ step₁ ⟩ >> ⟨ step₂ ⟩ >> ⟨ step₃ ⟩ >> ⟨ step₄ ⟩
- where
- M₀ M₁ M₂ M₃ M₄ M₅ : Term
- M₀ = (I[𝔹⇒𝔹] ·ᵀ I[𝔹] ·ᵀ (not[𝔹] ·ᵀ falseᵀ))
- M₁ = ((λᵀ x ∈ 𝔹 ⇒ (I[𝔹] ·ᵀ varᵀ x)) ·ᵀ (not[𝔹] ·ᵀ falseᵀ))
- M₂ = ((λᵀ x ∈ 𝔹 ⇒ (I[𝔹] ·ᵀ varᵀ x)) ·ᵀ (ifᵀ falseᵀ then falseᵀ else trueᵀ))
- M₃ = ((λᵀ x ∈ 𝔹 ⇒ (I[𝔹] ·ᵀ varᵀ x)) ·ᵀ trueᵀ)
- M₄ = I[𝔹] ·ᵀ trueᵀ
- M₅ = trueᵀ
- step₀ : M₀ ⟹ M₁
- step₀ = γ⇒₁ (β⇒ value-λᵀ)
- step₁ : M₁ ⟹ M₂
- step₁ = γ⇒₂ value-λᵀ (β⇒ value-falseᵀ)
- step₂ : M₂ ⟹ M₃
- step₂ = γ⇒₂ value-λᵀ β𝔹₂ ⟩
+ true
step₃ : M₃ ⟹ M₄∎
-
step₃ = β⇒ value-trueᵀ
- step₄ : M₄ ⟹ M₅
- step₄ = β⇒ value-trueᵀ
-
-
+{% endraw %}
## Type rules
-
-
-{% raw %}
+Context : Set
Context = PartialMap Type
infix 5010 _⊢_∈__⊢_∶_
data _⊢_∈__⊢_∶_ : Context → Term → Type → Set where
Ax : ∀ {Γ x A} →
Γ x ≡ just A →
Γ ⊢ varᵀ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ᵀtrue ∈∶ 𝔹
𝔹-I₂ : ∀ {Γ} →
Γ ⊢ falseᵀfalse ∈∶ 𝔹
𝔹-E : ∀ {Γ L M N A} →
Γ ⊢ L ∈∶ 𝔹 →
Γ ⊢ M ∈∶ A →
Γ ⊢ N ∈∶ A →
Γ ⊢ (ifᵀif L then M else N) ∈∶ A
+{% endraw %}
+
+## 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 %}
+
+Construction of a type derivation is best done interactively.
+We start with the declaration:
+
+ `typing₁ : ∅ ⊢ not ∶ 𝔹 ⇒ 𝔹`
+ `typing₁ = ?`
+
+Typing control-L causes Agda to create a hole and tell us its expected type.
+
+ `typing₁ = { }0`
+ `?0 : ∅ ⊢ not ∶ 𝔹 ⇒ 𝔹`
+
+Now we fill in the hole, observing that the outermost term in `not` in a `λ`,
+which is typed using `⇒-I`. The `⇒-I` rule in turn takes one argument, which
+we again specify with a hole.
+
+ `typing₁ = ⇒-I { }0`
+ `?0 : ∅ , x ∶ 𝔹 ⊢ if var x then false else true ∶ 𝔹`
+
+Again we fill in the hole, observing that the outermost term is now
+`if_then_else_`, which is typed using `𝔹-E`. The `𝔹-E` rule in turn takes
+three arguments, which we again specify with holes.
+
+ `typing₁ = ⇒-I (𝔹-E { }0 { }1 { }2)`
+ `?0 : ∅ , x ∶ 𝔹 ⊢ var x ∶ 𝔹`
+ `?1 : ∅ , x ∶ 𝔹 ⊢ false ∶ 𝔹`
+ `?2 : ∅ , x ∶ 𝔹 ⊢ true ∶ 𝔹`
+
+Again we fill in the three holes, observing 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 computed with a hole.
+
+Filling in the three holes gives the derivation above.
+
+
-
diff --git a/out/StlcProp.md b/out/StlcProp.md
index 15722646..5dce75b7 100644
--- a/out/StlcProp.md
+++ b/out/StlcProp.md
@@ -75,67 +75,73 @@ theorem.
>import
Data.BoolData.Maybe using (BoolMaybe; truejust; falsenothing)
open import Data.Maybe usingData.Product (Maybe;using just(∃; ∃₂; nothing_,_; ,_)import Data.ProductData.Sum using (∃_⊎_; ∃₂inj₁; _,_; ,_)
-open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl; trans; sym)
open import Maps
open Maps.PartialMap using (∅; apply-∅; update-permute) renaming (_,_↦_ to _,_∶_)
open import Stlc
{% endraw %}
@@ -353,441 +360,413 @@ theorem.
## Canonical Forms
-As we saw for the simple calculus in the [Stlc]
-chapter, the first step in establishing basic properties of reduction and types
+As we saw for the simple calculus in Chapter [Types]({{ "Types" | relative_url }}),
+the first step in establishing basic properties of reduction and typing
is to identify the possible _canonical forms_ (i.e., well-typed closed values)
-belonging to each type. For `bool`, these are the boolean values `true` and
-`false`. For arrow types, the canonical forms are lambda-abstractions.
+belonging to each type. For function types the canonical forms are lambda-abstractions,
+while for boolean types they are values `true` and `false`.
{% raw %}
-data canonical_for_ : Term → Type → Set where
canonical-λᵀ : ∀ {x A N B} → canonical (λᵀ x ∈ A ⇒ N)canonical-λ for: ∀ (A{x ⇒A N B)
- canonical-trueᵀ} → canonical (λ[ :x canonical∶ trueᵀA ] N) for (A for⇒ 𝔹B)
canonical-falseᵀcanonical-true : canonical falseᵀtrue for 𝔹
-
-
-
-canonical-false : canonical false for 𝔹
canonicalFormsLemma : ∀ {L A} → ∅ ⊢ L ∶ A → Value L → canonical L for A
+canonicalFormsLemma (Ax ⊢x) ()
+canonicalFormsLemma (⇒-I ⊢N) value-λ A}= →canonical-λ
+canonicalFormsLemma ∅ ⊢ L ∈ A → value L → canonical L(⇒-E for⊢L A⊢M) ()
canonicalFormsLemma (Ax ⊢x)𝔹-I₁ ()
-canonicalFormsLemmavalue-true (⇒-I ⊢N) value-λᵀ = canonical-λᵀ canonical-true
canonicalFormsLemma 𝔹-I₂ value-false = canonical-false
+canonicalFormsLemma (⇒-E ⊢L ⊢M)𝔹-E ()
-canonicalFormsLemma 𝔹-I₁ value-trueᵀ = canonical-trueᵀ
-canonicalFormsLemma 𝔹-I₂ value-falseᵀ = canonical-falseᵀ
-canonicalFormsLemma (𝔹-E ⊢L ⊢M ⊢N) ()
{% endraw %}
@@ -796,857 +775,863 @@ belonging to each type. For `bool`, these are the boolean values `true` and
As before, the _progress_ theorem tells us that closed, well-typed
terms are not stuck: either a well-typed term is a value, or it
-can take a reduction step. The proof is a relatively
-straightforward extension of the progress proof we saw in the
-[Stlc]({{ "Stlc" | relative_url }}) chapter. We'll give the proof in English
-first, then the formal version.
+can take a reduction step.
{% raw %}
-progress : ∀ {M A} → ∅ ⊢ M ∈∶ A → valueValue M ⊎ ∃ λ N → M ⟹ N
{% endraw %}
-_Proof_: By induction on the derivation of `\vdash t : A`.
+The proof is a relatively
+straightforward extension of the progress proof we saw in
+[Types]({{ "Types" | relative_url }}).
+We give the proof in English
+first, then the formal version.
- - The last rule of the derivation cannot be `var`,
+_Proof_: By induction on the derivation of `∅ ⊢ M ∶ A`.
+
+ - The last rule of the derivation cannot be `Ax`,
since a variable is never well typed in an empty context.
- - The `true`, `false`, and `abs` cases are trivial, since in
- each of these cases we can see by inspecting the rule that `t`
- is a value.
+ - If the last rule of the derivation is `⇒-I`, `𝔹-I₁`, or `𝔹-I₂`
+ then, trivially, the term is a value.
- - If the last rule of the derivation is `app`, then `t` has the
- form `t_1\;t_2` for som e`t_1` and `t_2`, where we know that
- `t_1` and `t_2` are also well typed in the empty context; in particular,
- there exists a type `B` such that `\vdash t_1 : A\to T` and
- `\vdash t_2 : B`. By the induction hypothesis, either `t_1` is a
- value or it can take a reduction step.
+ - If the last rule of the derivation is `⇒-E`, then the term has the
+ form `L · M` for some `L` and `M`, where we know that `L` and `M`
+ are also well typed in the empty context, giving us two induction
+ hypotheses. By the first induction hypothesis, either `L` is a
+ value or it can take a step.
- - If `t_1` is a value, then consider `t_2`, which by the other
- induction hypothesis must also either be a value or take a step.
+ - If `L` is a value then consider `M`. By the second induction
+ hypothesis, either `M` is a value or it can take a step.
- - Suppose `t_2` is a value. Since `t_1` is a value with an
- arrow type, it must be a lambda abstraction; hence `t_1\;t_2`
- can take a step by `red`.
+ - If `M` is a value, then since `L` is a value with a
+ function type we know it must be a lambda abstraction,
+ and hence `L · M` can take a step by `β⇒`.
- - Otherwise, `t_2` can take a step, and hence so can `t_1\;t_2`
- by `app2`.
+ - If `M` can take a step, then so can `L · M` by `γ⇒₂`.
- - If `t_1` can take a step, then so can `t_1 t_2` by `app1`.
+ - If `L` can take a step, then so can `L · M` by `γ⇒₁`.
- - If the last rule of the derivation is `if`, then `t = \text{if }t_1
- \text{ then }t_2\text{ else }t_3`, where `t_1` has type `bool`. By
- the IH, `t_1` either is a value or takes a step.
+ - 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 `𝔹`.
+ By the induction hypothesis, either `L` is a value or it can
+ take a step.
- - If `t_1` is a value, then since it has type `bool` it must be
- either `true` or `false`. If it is `true`, then `t` steps
- to `t_2`; otherwise it steps to `t_3`.
+ - If `L` is a value, then since it has type boolean it must be
+ either `true` or `false`.
- - Otherwise, `t_1` takes a step, and therefore so does `t` (by `if`).
+ - If `L` is `true`, then then term steps by `β𝔹₁`
+
+ - If `L` is `false`, then then term steps by `β𝔹₂`
+
+ - If `L` can take a step, then so can `if L then M else N` by `γ𝔹`.
+
+This completes the proof.
{% raw %}
-progress (Ax ())
progress (⇒-I ⊢N) = inj₁ value-λ
+progress (⇒-E {Γ} {L} {M} {A} {B} ⊢L ⊢M) with progress ⊢L
+... | inj₂ (L′ , L⟹L′) = inj₂ (L′ · M , γ⇒₁ L⟹L′)
+... | inj₁ valueL with progress ⊢M
+... | inj₂ (M′ , M⟹M′) = inj₂ (L · M′ , γ⇒₂ valueL M⟹M′)
+... | inj₁ valueM ⊢N)with =canonicalFormsLemma inj₁⊢L value-λᵀvalueL
progress... (⇒-E| canonical-λ {Γ} {L} {M} {A} {B} ⊢Lx} ⊢M){.A} with{N} progress{.B} ⊢L= inj₂
- ...((N |[ inj₂x ∶= (L′ , L⟹L′) = inj₂ (L′ ·ᵀ M ]) , γ⇒₁β⇒ valueM)
+progress 𝔹-I₁ = L⟹L′)
-... | inj₁ valueL with progress ⊢Mvalue-true
...progress |𝔹-I₂ inj₂= (M′inj₁ ,value-false
+progress M⟹M′)(𝔹-E ={Γ} inj₂{L} (L{M} ·ᵀ{N} M′{A} , γ⇒₂⊢L valueL⊢M ⊢N) M⟹M′)with progress ⊢L
... | inj₁inj₂ valueM(L′ with, canonicalFormsLemmaL⟹L′) ⊢L= inj₂ ((if valueLL′ then M else N) , γ𝔹 L⟹L′)
... | canonical-λᵀ {x} {.A}| {N}inj₁ {.B}valueL =with inj₂ ((N [ x := M ]) , β⇒canonicalFormsLemma valueM)⊢L valueL
progress... 𝔹-I₁| canonical-true = inj₁inj₂ value-trueᵀ(M
-progress 𝔹-I₂ = inj₁ value-falseᵀ
-progress (𝔹-E {Γ} {L} {M} {N} {A} ⊢L ⊢M ⊢N) with progress ⊢L
-... | inj₂ (L′ , L⟹L′) = inj₂ ((ifᵀ L′ then M else N) , γ𝔹 L⟹L′)
-... | inj₁ valueL with canonicalFormsLemma ⊢L valueL
-... | canonical-trueᵀ = inj₂ (M , β𝔹₁)
... | canonical-falseᵀcanonical-false = inj₂ (N , β𝔹₂)
{% endraw %}
@@ -1656,100 +1641,100 @@ Show that progress can also be proved by induction on terms
instead of induction on typing derivations.
{% raw %}
-postulate
progress′ : ∀ {M A} → ∅ ⊢ M ∈∶ A → valueValue M ⊎ ∃ λ N → M ⟹ N
{% endraw %}
@@ -1802,609 +1787,609 @@ A variable `x` _appears free in_ a term `M` if `M` contains some
occurrence of `x` that is not under an abstraction over `x`.
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)`
+ - `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)`
Formally:
{% raw %}
-data _FreeIn__∈_ : Id → Term → Set where
free-varᵀ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 {x}∈ M → x FreeIn∈ (varᵀif L then xM else N)
free-λᵀ : ∀ {xfree-if₃ y: A∀ N}{x →L yM ≢N} x → x FreeIn∈ N → x N∈ → x(if FreeInL then (λᵀ y ∈ A ⇒ N)
- free-·ᵀ₁ : ∀ {x L M} → x FreeIn L → x FreeIn (L ·ᵀ M)
- free-·ᵀ₂ : ∀ {x L M} → x FreeIn M → x FreeIn (L ·ᵀ M)
- free-ifᵀ₁ : ∀ {x L M N} → x FreeIn L → x FreeIn (ifᵀ L then M else N)
- free-ifᵀ₂ : ∀ {x L M N} → x FreeIn M → x FreeIn (ifᵀ L then M else N)
- free-ifᵀ₃ : ∀ {x L M N} → x FreeIn N → x FreeIn (ifᵀ L then M else N)
{% endraw %}
@@ -2412,78 +2397,78 @@ Formally:
A term in which no variables appear free is said to be _closed_.
{% raw %}
-closed : Term → Set
closed M = ∀ {x} → ¬ (x FreeIn∈ M)
{% endraw %}
#### Exercise: 1 star (free-in)
-If the definition of `_FreeIn_` is not crystal clear to
+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
@@ -2498,115 +2483,115 @@ well typed in context `Γ`, then it must be the case that
`Γ` assigns a type to `x`.
{% raw %}
-freeLemma : ∀ {x M A Γ} → x FreeIn M → Γ ⊢ M ∈ AM → ∃ λ B → Γ ⊢ M ∶ A → ∃ λ B → Γ x ≡ just B
{% endraw %}
@@ -2615,11 +2600,11 @@ _Proof_: We show, by induction on the proof that `x` appears
free in `P`, that, for all contexts `Γ`, if `P` is well
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-var`, then `P = x`, and from
the assumption that `M` is well typed under `Γ` we have
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 `P = L · M` and `x`
appears free in `L`. Since `L` is well typed under `\Gamma`,
we can see from the typing rules that `L` must also be, and
the IH then tells us that `Γ` assigns `x` a type.
@@ -2630,470 +2615,470 @@ _Proof_: We show, by induction on the proof that `x` appears
under `Γ` as well, and the IH gives us exactly the
conclusion we want.
- - The only remaining case is `free-λᵀ`. In this case `P =
- λᵀ y ∈ A ⇒ N`, and `x` appears free in `N`; we also know that
+ - The only remaining case is `free-λ`. In this case `P =
+ λ[ y ∶ A ] N`, and `x` appears free in `N`; we also know that
`x` is different from `y`. The difference from the previous
cases is that whereas `P` is well typed under `\Gamma`, 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
- 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
`_≟_`, noting that `x` and `y` are different variables.
{% raw %}
-freeLemma free-varᵀfree-var (Ax Γx≡justA) = (_ , Γx≡justA)
freeLemma (free-·ᵀ₁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 ≟ (⇒-Ex
+... ⊢L| ⊢M)yes y≡x = freeLemma⊥-elim x∈L(y≢x ⊢Ly≡x)
freeLemma... | (free-·ᵀ₂no _ = 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 %}
-[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
term `Γx=justC` would not simplify properly.]
@@ -3103,368 +3088,368 @@ 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 %}
-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
to do this? Intuitively, it must at least be the case that
`Γ′` assigns the same types as `Γ` to all the variables
@@ -3472,150 +3457,150 @@ that appear free in `M`. In fact, this is the only condition that
is needed.
{% raw %}
-weakencontextLemma : ∀ {Γ Γ′ M A}
→ (∀ {x} → x FreeIn∈ M → Γ x ≡ Γ′ x)
→ Γ ⊢ M ∈∶ A
→ Γ′ ⊢ M ∈∶ A
{% endraw %}
_Proof_: By induction on the derivation of
-`Γ ⊢ M ∈ A`.
+`Γ ⊢ M ∶ A`.
- If the last rule in the derivation was `var`, then `t = x`
and `\Gamma x = T`. By assumption, `\Gamma' x = T` as well, and
@@ -3657,604 +3642,604 @@ _Proof_: By induction on the derivation of
hence the desired result follows from the induction hypotheses.
{% raw %}
-weakencontextLemma Γ~Γ′ (Ax Γx≡justA) rewrite (Γ~Γ′ free-varᵀ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-·₂) Γx≡justA
-weaken {Γ} {Γ′} {λᵀ x ∈ A ⇒ N} Γ~Γ′ (⇒-I ⊢N) = ⇒-I (weaken Γx~Γ′x ⊢N)
- where
- Γx~Γ′x : ∀ {y} → y FreeIn 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)
-weaken Γ~Γ′ (⇒-E ⊢L ⊢M) = ⇒-E (weaken (Γ~Γ′ ∘ free-·ᵀ₁) ⊢L) (weaken (Γ~Γ′ ∘ free-·ᵀ₂) ⊢M)
weakencontextLemma Γ~Γ′ 𝔹-I₁ = 𝔹-I₁
weakencontextLemma Γ~Γ′ 𝔹-I₂ = 𝔹-I₂
weakencontextLemma Γ~Γ′ (𝔹-E ⊢L ⊢M ⊢N)
= 𝔹-E (weakencontextLemma (Γ~Γ′ ∘ free-ifᵀ₁free-if₁) ⊢L) (weakencontextLemma (Γ~Γ′ ∘ free-ifᵀ₂free-if₂) ⊢M) (weakencontextLemma (Γ~Γ′ ∘ free-ifᵀ₃free-if₃) ⊢N)
⊢ → y FreeIn (λᵀ x′ ∈ A′ ⇒ N′) →[ (Γx ,∶= x′V ↦] A)∶ yB′
+ ⊢N′V = preservation-[∶=] ≡x′x⊢N′ Γ y⊢V
- Γ′~Γpreservation-[∶=] {y} (free-λᵀ⇒-E x′≢y⊢L y∈N′⊢M) with⊢V x′= ≟ y⇒-E
- ...| yes x′≡y =(preservation-[∶=] ⊥-elim⊢L ⊢V) (x′≢y x′≡y)
- ...|preservation-[∶=] no⊢M _ = refl⊢V)
...| nopreservation-[∶=] x≢x′ =𝔹-I₁ ⊢V ⇒-I= ⊢N′V𝔹-I₁
- where
- x′x⊢N′preservation-[∶=] : Γ𝔹-I₂ ,⊢V x′= ↦ A′𝔹-I₂ , x ↦ A ⊢ N′ ∈ B′
+preservation-[∶=]
- x′x⊢N′ rewrite update-permute Γ x A x′ A′ x≢x′ = ⊢N′
- ⊢N′V : (Γ𝔹-E ,⊢L x′⊢M ↦⊢N) ⊢V =
+ 𝔹-E (preservation-[∶=] ⊢L ⊢V) (preservation-[∶=] ⊢M A′⊢V) ⊢ N′ [ x := V ] ∈ B′
- ⊢N′V = preservation-[:=] x′x⊢N′ ⊢V
-preservation-[:=] (⇒-Epreservation-[∶=] ⊢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 %}
@@ -5864,95 +5849,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 %}
@@ -5974,7 +5959,7 @@ _Proof_: By induction on the derivation of `\vdash t : T`.
- The `Sapp2` case is similar.
- If `t_1 t_2` takes a step by `Sred`, then `t_1 =
- \lambda x:t_{11}.t_{12}` and `t_1 t_2` steps to ``x:=t_2`t_{12}`; the
+ \lambda x:t_{11}.t_{12}` and `t_1 t_2` steps to ``x∶=t_2`t_{12}`; the
desired result now follows from the fact that substitution
preserves types.
@@ -5989,20 +5974,276 @@ _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 (⇒-I𝔹-E ⊢N)𝔹-I₁ ()⊢M ⊢N) β𝔹₁ = ⊢M
preservation (⇒-E (⇒-I ⊢N) ⊢V) (β⇒𝔹-E valueV)𝔹-I₂ =⊢M preservation-[:=] ⊢N) β𝔹₂ = ⊢N
+preservation ⊢V(𝔹-E ⊢L ⊢M ⊢N) (γ𝔹 L⟹L′) with preservation ⊢L L⟹L′
preservation...| (⇒-E ⊢L ⊢M) (γ⇒₁ L⟹L′) with preservation ⊢L⊢L′ L⟹L′
-...|= 𝔹-E ⊢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 %}
@@ -6468,7 +6437,7 @@ Put progress and preservation together and show that a well-typed
term can _never_ reach a stuck state.
Definition stuck (t:tm) : Prop :=
- (normal_form step) t /\ ~ value t.
+ (normal_form step) t /\ ~ Value t.
Corollary soundness : forall t t' T,
empty \vdash t : T →