diff --git a/Makefile b/Makefile index cdba6b11..2b486f6b 100644 --- a/Makefile +++ b/Makefile @@ -8,7 +8,7 @@ out/: mkdir out out/%.md: src/%.lagda out/ - agda2html --link-to-agda-stdlib --link-local -i $< -o $@ + agda2html --verbose --link-to-agda-stdlib --link-local -i $< -o $@ .phony: serve diff --git a/out/Maps.md b/out/Maps.md new file mode 100644 index 00000000..869200f1 --- /dev/null +++ b/out/Maps.md @@ -0,0 +1,7375 @@ +--- +title : "Maps: Total and Partial Maps" +layout : page +permalink : /Maps +--- + +Maps (or dictionaries) are ubiquitous data structures, both in software +construction generally and in the theory of programming languages in particular; +we're going to need them in many places in the coming chapters. They also make +a nice case study using ideas we've seen in previous chapters, including +building data structures out of higher-order functions (from [Basics]({{ +"Basics" | relative_url }}) and [Poly]({{ "Poly" | relative_url }}) and the use +of reflection to streamline proofs (from [IndProp]({{ "IndProp" | relative_url +}})). + +We'll define two flavors of maps: _total_ maps, which include a +"default" element to be returned when a key being looked up +doesn't exist, and _partial_ maps, which return an `Maybe` to +indicate success or failure. The latter is defined in terms of +the former, using `nothing` as the default element. + +## The Agda Standard Library + +One small digression before we start. + +Unlike the chapters we have seen so far, this one does not +import the chapter before it (and, transitively, all the +earlier chapters). Instead, in this chapter and from now, on +we're going to import the definitions and theorems we need +directly from Agda's standard library. You should not notice +much difference, though, because we've been careful to name our +own definitions and theorems the same as their counterparts in the +standard library, wherever they overlap. + +
+
+open import Data.Nat         using (ℕ)
+open import Data.Empty       using (⊥; ⊥-elim)
+open import Data.Maybe       using (Maybe; just; nothing)
+open import Data.String      using (String)
+open import Relation.Nullary using (¬_; Dec; yes; no)
+open import Relation.Binary.PropositionalEquality
+                             using (_≡_; refl; _≢_; trans; sym)
+
+
+ +Documentation for the standard library can be found at +. + +## Identifiers + +First, we need a type for the keys that we use to index into our +maps. For this purpose, we again use the type `Id` from the +[Lists](sf/Lists.html) chapter. To make this chapter self contained, +we repeat its definition here. + +
+
+data Id : Set where
+  id : String → Id
+
+
+ +We recall a standard fact of logic. + +
+
+contrapositive : ∀ {ℓ₁ ℓ₂} {P : Set ℓ₁} {Q : Set ℓ₂} → (P → Q) → (¬ Q → ¬ P)
+contrapositive p→q ¬q p = ¬q (p→q p)
+
+
+ +Using the above, we can decide equality of two identifiers +by deciding equality on the underlying strings. + +
+
+_≟_ : (x y : Id) → Dec (x ≡ y)
+id x ≟ id y with x Data.String.≟ y
+id x ≟ id y | yes refl  =  yes refl
+id x ≟ id y | no  x≢y   =  no (contrapositive id-inj x≢y)
+  where
+    id-inj : ∀ {x y} → id x ≡ id y → x ≡ y
+    id-inj refl  =  refl
+
+
+ +We define some identifiers for future use. + +
+
+x y z : Id
+x = id "x"
+y = id "y"
+z = id "z"
+
+
+ +## Extensionality + +## Total Maps + +Our main job in this chapter will be to build a definition of +partial maps that is similar in behavior to the one we saw in the +[Lists](sf/Lists.html) chapter, plus accompanying lemmas about their +behavior. + +This time around, though, we're going to use _functions_, rather +than lists of key-value pairs, to build maps. The advantage of +this representation is that it offers a more _extensional_ view of +maps, where two maps that respond to queries in the same way will +be represented as literally the same thing (the same function), +rather than just "equivalent" data structures. This, in turn, +simplifies proofs that use maps. + +We build partial maps in two steps. First, we define a type of +_total maps_ that return a default value when we look up a key +that is not present in the map. + +
+
+TotalMap : Set → Set
+TotalMap A = Id → A
+
+
+ +Intuitively, a total map over anfi element type $$A$$ _is_ just a +function that can be used to look up ids, yielding $$A$$s. + +
+
+module TotalMap where
+
+
+ +The function `always` yields a total map given a +default element; this map always returns the default element when +applied to any id. + +
+
+  always : ∀ {A} → A → TotalMap A
+  always v x = v
+
+
+ +More interesting is the update function, which (as before) takes +a map $$ρ$$, a key $$x$$, and a value $$v$$ and returns a new map that +takes $$x$$ to $$v$$ and takes every other key to whatever $$ρ$$ does. + +
+
+  _,_↦_ : ∀ {A} → TotalMap A → Id → A → TotalMap A
+  (ρ , x ↦ v) y with x ≟ y
+  ... | yes x=y = v
+  ... | no  x≠y = ρ y
+
+
+ +This definition is a nice example of higher-order programming. +The update function takes a _function_ $$ρ$$ and yields a new +function that behaves like the desired map. + +We define handy abbreviations for updating a map two, three, or four times. + + + +
+
+  _,_↦_,_↦_ : ∀ {A} → TotalMap A → Id → A → Id → A → TotalMap A
+  ρ , x₁ ↦ v₁ , x₂ ↦ v₂  =  (ρ , x₁ ↦ v₁), x₂ ↦ v₂
+
+  _,_↦_,_↦_,_↦_ : ∀ {A} → TotalMap A → Id → A → Id → A → Id → A → TotalMap A
+  ρ , x₁ ↦ v₁ , x₂ ↦ v₂ , x₃ ↦ v₃  =  ((ρ , x₁ ↦ v₁), x₂ ↦ v₂), x₃ ↦ v₃
+
+  _,_↦_,_↦_,_↦_,_↦_ : ∀ {A} → TotalMap A → Id → A → Id → A → Id → A → Id → A → TotalMap A
+  ρ , x₁ ↦ v₁ , x₂ ↦ v₂ , x₃ ↦ v₃ , x₄ ↦ v₄ =  (((ρ , x₁ ↦ v₁), x₂ ↦ v₂), x₃ ↦ v₃), x₄ ↦ v₄
+
+
+ +For example, we can build a map taking ids to naturals, where $$x$$ +maps to 42, $$y$$ maps to 69, and every other key maps to 0, as follows: + +
+
+  ρ₀ : TotalMap ℕ
+  ρ₀ = always 0 , x ↦ 42 , y ↦ 69
+
+
+ +This completes the definition of total maps. Note that we don't +need to define a `find` operation because it is just function +application! + +
+
+  test₁ : ρ₀ x ≡ 42
+  test₁ = refl
+
+  test₂ : ρ₀ y ≡ 69
+  test₂ = refl
+
+  test₃ : ρ₀ z ≡ 0
+  test₃ = refl
+
+
+ +To use maps in later chapters, we'll need several fundamental +facts about how they behave. Even if you don't work the following +exercises, make sure you understand the statements of +the lemmas! + +#### Exercise: 1 star, optional (apply-always) +The `always` map returns its default element for all keys: + +
+
+  postulate
+    apply-always : ∀ {A} (v : A) (x : Id) → always v x ≡ v
+
+
+ + + +#### Exercise: 2 stars, optional (update-eq) +Next, if we update a map $$ρ$$ at a key $$x$$ with a new value $$v$$ +and then look up $$x$$ in the map resulting from the update, we get +back $$v$$: + +
+
+  postulate
+    update-eq : ∀ {A} (ρ : TotalMap A) (x : Id) (v : A)
+              → (ρ , x ↦ v) x ≡ v
+
+
+ + + +#### Exercise: 2 stars, optional (update-neq) +On the other hand, if we update a map $$m$$ at a key $$x$$ and +then look up a _different_ key $$y$$ in the resulting map, we get +the same result that $$m$$ would have given: + +
+
+  update-neq : ∀ {A} (ρ : TotalMap A) (x : Id) (v : A) (y : Id)
+             → x ≢ y → (ρ , x ↦ v) y ≡ ρ y
+  update-neq ρ x v y x≢y with x ≟ y
+  ... | yes x≡y = ⊥-elim (x≢y x≡y)
+  ... | no  _   = refl
+
+
+ +For the following lemmas, since maps are represented by functions, to +show two maps equal we will need to postulate extensionality. + +
+
+  postulate
+    extensionality : ∀ {A : Set} {ρ ρ′ : TotalMap A} → (∀ x → ρ x ≡ ρ′ x) → ρ ≡ ρ′
+
+
+ +#### Exercise: 2 stars, optional (update-shadow) +If we update a map $$ρ$$ at a key $$x$$ with a value $$v$$ and then +update again with the same key $$x$$ and another value $$w$$, the +resulting map behaves the same (gives the same result when applied +to any key) as the simpler map obtained by performing just +the second update on $$ρ$$: + +
+
+  postulate
+    update-shadow : ∀ {A} (ρ : TotalMap A) (x : Id) (v w : A) 
+                  → (ρ , x ↦ v , x ↦ w) ≡ (ρ , x ↦ w)
+
+
+ + + +#### Exercise: 2 stars (update-same) +Prove the following theorem, which states that if we update a map $$ρ$$ to +assign key $$x$$ the same value as it already has in $$ρ$$, then the +result is equal to $$ρ$$: + +
+
+  postulate
+    update-same : ∀ {A} (ρ : TotalMap A) (x : Id) → (ρ , x ↦ ρ x) ≡ ρ
+
+
+ + + +#### Exercise: 3 stars, recommended (update-permute) +Prove one final property of the `update` function: If we update a map +$$m$$ at two distinct keys, it doesn't matter in which order we do the +updates. + +
+
+  postulate
+    update-permute : ∀ {A} (ρ : TotalMap A) (x : Id) (v : A) (y : Id) (w : A)
+                   → x ≢ y → (ρ , x ↦ v , y ↦ w) ≡ (ρ , y ↦ w , x ↦ v)
+
+
+ + + +## Partial maps + +Finally, we define _partial maps_ on top of total maps. A partial +map with elements of type `A` is simply a total map with elements +of type `Maybe A` and default element `nothing`. + +
+
+PartialMap : Set → Set
+PartialMap A = TotalMap (Maybe A)
+
+
+ +
+
+module PartialMap where
+
+
+ +
+
+  ∅ : ∀ {A} → PartialMap A
+  ∅ = TotalMap.always nothing
+
+
+ +
+
+  _,_↦_ : ∀ {A} (ρ : PartialMap A) (x : Id) (v : A) → PartialMap A
+  ρ , x ↦ v = TotalMap._,_↦_ ρ x (just v)
+
+
+As before, we define handy abbreviations for updating a map two, three, or four times. + +
+
+  _,_↦_,_↦_ : ∀ {A} → PartialMap A → Id → A → Id → A → PartialMap A
+  ρ , x₁ ↦ v₁ , x₂ ↦ v₂  =  (ρ , x₁ ↦ v₁), x₂ ↦ v₂
+
+  _,_↦_,_↦_,_↦_ : ∀ {A} → PartialMap A → Id → A → Id → A → Id → A → PartialMap A
+  ρ , x₁ ↦ v₁ , x₂ ↦ v₂ , x₃ ↦ v₃  =  ((ρ , x₁ ↦ v₁), x₂ ↦ v₂), x₃ ↦ v₃
+
+  _,_↦_,_↦_,_↦_,_↦_ : ∀ {A} → PartialMap A → Id → A → Id → A → Id → A → Id → A → PartialMap A
+  ρ , x₁ ↦ v₁ , x₂ ↦ v₂ , x₃ ↦ v₃ , x₄ ↦ v₄ =  (((ρ , x₁ ↦ v₁), x₂ ↦ v₂), x₃ ↦ v₃), x₄ ↦ v₄
+
+
+ +We now lift all of the basic lemmas about total maps to partial maps. + +
+
+  apply-∅ : ∀ {A} → (x : Id) → (∅ {A} x) ≡ nothing
+  apply-∅ x  = TotalMap.apply-always nothing x
+
+
+ +
+
+  update-eq : ∀ {A} (ρ : PartialMap A) (x : Id) (v : A)
+            → (ρ , x ↦ v) x ≡ just v
+  update-eq ρ x v = TotalMap.update-eq ρ x (just v)
+
+
+ +
+
+  update-neq : ∀ {A} (ρ : PartialMap A) (x : Id) (v : A) (y : Id)
+             → x ≢ y → (ρ , x ↦ v) y ≡ ρ y
+  update-neq ρ x v y x≢y = TotalMap.update-neq ρ x (just v) y x≢y
+
+
+ +
+
+  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)
+
+
+ +
+
+  update-same : ∀ {A} (ρ : PartialMap A) (x : Id) (v : A) 
+              → ρ x ≡ just v
+              → (ρ , x ↦ v) ≡ ρ
+  update-same ρ x v ρx≡v rewrite sym ρx≡v = TotalMap.update-same ρ x
+
+
+ +
+
+  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
+
+
diff --git a/out/Stlc.md b/out/Stlc.md new file mode 100644 index 00000000..0a083313 --- /dev/null +++ b/out/Stlc.md @@ -0,0 +1,4453 @@ +--- +title : "Stlc: The Simply Typed Lambda-Calculus" +layout : page +permalink : /Stlc +--- + +This chapter defines the simply-typed lambda calculus. + +## Imports +
+
+open import Maps using (Id; id; _≟_; PartialMap; module PartialMap)
+open PartialMap using (∅; _,_↦_)
+open import Data.String using (String)
+open import Data.Empty using (⊥; ⊥-elim)
+open import Data.Maybe using (Maybe; just; nothing)
+open import Data.Nat using (ℕ; suc; zero; _+_)
+open import Data.Bool 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 using (_≡_; _≢_; refl)
+-- open import Relation.Binary.Core using (Rel)
+-- open import Data.Product using (∃; ∄; _,_)
+-- open import Function using (_∘_; _$_)
+
+
+ + +## Syntax + +Syntax of types and terms. All source terms are labeled with $ᵀ$. + +
+
+infixr 100 _⇒_
+infixl 100 _·ᵀ_
+
+data Type : Set where
+  𝔹 : Type
+  _⇒_ : Type → Type → Type
+
+data Term : Set where
+  varᵀ : Id → Term
+  λᵀ_∈_⇒_ : Id → Type → Term → Term
+  _·ᵀ_ : Term → Term → Term
+  trueᵀ : Term
+  falseᵀ : Term
+  ifᵀ_then_else_ : Term → Term → Term → Term
+
+
+ +Some examples. +
+
+f x y : Id
+f  =  id "f"
+x  =  id "x"
+y  =  id "y"
+
+I[𝔹] I[𝔹⇒𝔹] K[𝔹][𝔹] not[𝔹] : Term 
+I[𝔹]  =  (λᵀ x ∈ 𝔹 ⇒ (varᵀ x))
+I[𝔹⇒𝔹]  =  (λᵀ f ∈ (𝔹 ⇒ 𝔹) ⇒ (λᵀ x ∈ 𝔹 ⇒ ((varᵀ f) ·ᵀ (varᵀ x))))
+K[𝔹][𝔹]  =  (λᵀ x ∈ 𝔹 ⇒ (λᵀ y ∈ 𝔹 ⇒ (varᵀ x)))
+not[𝔹]  =  (λᵀ x ∈ 𝔹 ⇒ (ifᵀ (varᵀ x) then falseᵀ else trueᵀ))
+
+
+ +## Values + +
+
+data value : Term → Set where
+  value-λᵀ : ∀ {x A N} → value (λᵀ x ∈ A ⇒ N)
+  value-trueᵀ : value (trueᵀ)
+  value-falseᵀ : value (falseᵀ)
+
+
+ +## Substitution + +
+
+_[_:=_] : Term → Id → Term → Term
+(varᵀ x′) [ x := V ] with x ≟ x′
+... | yes _ = V
+... | no  _ = varᵀ x′
+(λᵀ x′ ∈ A′ ⇒ N′) [ x := V ] with x ≟ x′
+... | yes _ = λᵀ x′ ∈ A′ ⇒ N′
+... | no  _ = λᵀ x′ ∈ A′ ⇒ (N′ [ x := V ])
+(L′ ·ᵀ M′) [ x := V ] =  (L′ [ x := V ]) ·ᵀ (M′ [ x := V ])
+(trueᵀ) [ x := V ] = trueᵀ
+(falseᵀ) [ x := V ] = falseᵀ
+(ifᵀ L′ then M′ else N′) [ x := V ] = ifᵀ (L′ [ x := V ]) then (M′ [ x := V ]) else (N′ [ x := V ])
+
+
+ +## Reduction rules + +
+
+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)
+
+
+ +## Reflexive and transitive closure of a relation + +
+
+Rel : Set → Set₁
+Rel A = A → A → Set
+
+infixl 100 _>>_
+
+data _* {A : Set} (R : Rel A) : Rel A where
+  ⟨⟩ : ∀ {x : A} → (R *) x x
+  ⟨_⟩ : ∀ {x y : A} → R x y → (R *) x y
+  _>>_ : ∀ {x y z : A} → (R *) x y → (R *) y z → (R *) x z
+
+
+ +
+
+_⟹*_ : Term → Term → Set
+_⟹*_ = (_⟹_) *
+
+
+ +Example evaluation. + +
+
+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-λᵀ β𝔹₂
+  step₃ : M₃ ⟹ M₄
+  step₃ = β⇒ value-trueᵀ         
+  step₄ : M₄ ⟹ M₅
+  step₄ = β⇒ value-trueᵀ
+
+
+ +## Type rules + +
+
+Context : Set
+Context = PartialMap Type
+
+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₁ : ∀ {Γ} →
+    Γ ⊢ trueᵀ ∈ 𝔹
+  𝔹-I₂ : ∀ {Γ} →
+    Γ ⊢ falseᵀ ∈ 𝔹
+  𝔹-E : ∀ {Γ L M N A} →
+    Γ ⊢ L ∈ 𝔹 →
+    Γ ⊢ M ∈ A →
+    Γ ⊢ N ∈ A →
+    Γ ⊢ (ifᵀ L then M else N) ∈ A
+
+
diff --git a/out/StlcProp.md b/out/StlcProp.md new file mode 100644 index 00000000..6ab715d0 --- /dev/null +++ b/out/StlcProp.md @@ -0,0 +1,6823 @@ +--- +title : "StlcProp: Properties of STLC" +layout : page +permalink : /StlcProp +--- + +
+
+open import Function using (_∘_)
+open import Data.Empty using (⊥; ⊥-elim)
+open import Data.Bool using (Bool; true; false)
+open import Data.Maybe using (Maybe; just; nothing)
+open import Data.Product using (∃; ∃₂; _,_; ,_)
+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
+open import Stlc
+
+
+ +In this chapter, we develop the fundamental theory of the Simply +Typed Lambda Calculus---in particular, the type safety +theorem. + + +## Canonical Forms + +As we saw for the simple calculus in the [Stlc]({{ "Stlc" | relative_url }}) +chapter, the first step in establishing basic properties of reduction and types +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. + +
+
+data canonical_for_ : Term → Type → Set where
+  canonical-λᵀ : ∀ {x A N B} → canonical (λᵀ x ∈ A ⇒ N) for (A ⇒ B)
+  canonical-trueᵀ : canonical trueᵀ for 𝔹
+  canonical-falseᵀ : canonical falseᵀ for 𝔹
+  
+-- canonical_for_ : Term → Type → Set
+-- canonical L for 𝔹       = L ≡ trueᵀ ⊎ L ≡ falseᵀ
+-- canonical L for (A ⇒ B) = ∃₂ λ x N → L ≡ λᵀ x ∈ A ⇒ N
+
+canonicalFormsLemma : ∀ {L A} → ∅ ⊢ L ∈ A → value L → canonical L for A
+canonicalFormsLemma (Ax ⊢x) ()
+canonicalFormsLemma (⇒-I ⊢N) value-λᵀ = canonical-λᵀ      -- _ , _ , refl
+canonicalFormsLemma (⇒-E ⊢L ⊢M) ()
+canonicalFormsLemma 𝔹-I₁ value-trueᵀ = canonical-trueᵀ    -- inj₁ refl
+canonicalFormsLemma 𝔹-I₂ value-falseᵀ = canonical-falseᵀ  -- inj₂ refl
+canonicalFormsLemma (𝔹-E ⊢L ⊢M ⊢N) ()
+
+
+ +## Progress + +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. + +
+
+progress : ∀ {M A} → ∅ ⊢ M ∈ A → value M ⊎ ∃ λ N → M ⟹ N
+
+
+ +_Proof_: By induction on the derivation of $$\vdash t : A$$. + + - The last rule of the derivation cannot be `var`, + 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 `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 $$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. + + - 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`. + + - Otherwise, $$t_2$$ can take a step, and hence so can $$t_1\;t_2$$ + by `app2`. + + - If $$t_1$$ can take a step, then so can $$t_1 t_2$$ by `app1`. + + - 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 $$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$$. + + - Otherwise, $$t_1$$ takes a step, and therefore so does $$t$$ (by `if`). + +
+
+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 with canonicalFormsLemma ⊢L valueL
+... | canonical-λᵀ {x} {.A} {N} {.B} = inj₂ ((N [ x := M ]) , β⇒ valueM)
+progress 𝔹-I₁ = inj₁ value-trueᵀ
+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ᵀ = inj₂ (N , β𝔹₂)
+
+
+ +#### 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. + +
+
+postulate
+  progress′ : ∀ {M A} → ∅ ⊢ M ∈ A → value M ⊎ ∃ λ N → M ⟹ N
+
+
+ +## Preservation + +The other half of the type soundness property is the preservation +of types during reduction. For this, we need to develop some +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: + + - The _preservation theorem_ is proved by induction on a typing + derivation, pretty much as we did in the [Stlc]({{ "Stlc" | 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 + this step preserves typing, we need to know that the substitution itself + 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 + requires looking at all the different cases in the definition + of substitition. This time, 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 + 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... + + - the _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... + + +### 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$$. +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)$$ + +Formally: + +
+
+data _FreeIn_ : Id → Term → Set where
+  free-varᵀ  : ∀ {x} → x FreeIn (varᵀ x)
+  free-λᵀ  : ∀ {x y A N} → y ≢ x → x FreeIn N → x FreeIn (λᵀ 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)
+
+
+ +A term in which no variables appear free is said to be _closed_. + +
+
+closed : Term → Set
+closed M = ∀ {x} → ¬ (x FreeIn M)
+
+
+ +#### Exercise: 1 star (free-in) +If the definition of `_FreeIn_` 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.) + +### 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 +well typed in context $$Γ$$, then it must be the case that +$$Γ$$ assigns a type to $$x$$. + +
+
+freeLemma : ∀ {x M A Γ} → x FreeIn M → Γ ⊢ M ∈ A → ∃ λ B → Γ x ≡ just B
+
+
+ +_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 + 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$$ + 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. + + - Almost all the other cases are similar: $$x$$ appears free in a + subterm of $$P$$, and since $$P$$ is well typed under $$Γ$$, we + know the subterm of $$M$$ in which $$x$$ appears is well typed + 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 + $$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 + allows us to conclude that $$x$$ is assigned some type by the + 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. + +
+
+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
+
+
+ +[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.] + +Next, we'll need the fact that any term $$M$$ which is well typed in +the empty context is closed (it has no free variables). + +#### Exercise: 2 stars, optional (∅⊢-closed) + +
+
+postulate
+  ∅⊢-closed : ∀ {M A} → ∅ ⊢ M ∈ A → closed M
+
+
+ + + +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 +that appear free in $$M$$. In fact, this is the only condition that +is needed. + +
+
+weaken : ∀ {Γ Γ′ M A}
+        → (∀ {x} → x FreeIn M → Γ x ≡ Γ′ x)
+        → Γ  ⊢ M ∈ A
+        → Γ′ ⊢ M ∈ A
+
+
+ +_Proof_: By induction on the derivation of +$$Γ ⊢ 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 + hence $$\Gamma' \vdash t : T$$ by `var`. + + - If the last rule was `abs`, then $$t = \lambda y:A. t'$$, with + $$T = A\to B$$ and $$\Gamma, y : A \vdash t' : B$$. The + induction hypothesis is that, for any context $$\Gamma''$$, if + $$\Gamma, y:A$$ and $$\Gamma''$$ assign the same types to all the + free variables in $$t'$$, then $$t'$$ has type $$B$$ under + $$\Gamma''$$. Let $$\Gamma'$$ be a context which agrees with + $$\Gamma$$ on the free variables in $$t$$; we must show + $$\Gamma' \vdash \lambda y:A. t' : A\to B$$. + + By $$abs$$, it suffices to show that $$\Gamma', y:A \vdash t' : t'$$. + By the IH (setting $$\Gamma'' = \Gamma', y:A$$), it suffices to show + that $$\Gamma, y:A$$ and $$\Gamma', y:A$$ agree on all the variables + that appear free in $$t'$$. + + Any variable occurring free in $$t'$$ must be either $$y$$ or + some other variable. $$\Gamma, y:A$$ and $$\Gamma', y:A$$ + clearly agree on $$y$$. Otherwise, note that any variable other + than $$y$$ that occurs free in $$t'$$ also occurs free in + $$t = \lambda y:A. t'$$, and by assumption $$\Gamma$$ and + $$\Gamma'$$ agree on all such variables; hence so do $$\Gamma, y:A$$ and + $$\Gamma', y:A$$. + + - If the last rule was `app`, then $$t = t_1\;t_2$$, with + $$\Gamma \vdash t_1:A\to T$$ and $$\Gamma \vdash t_2:A$$. + One induction hypothesis states that for all contexts $$\Gamma'$$, + if $$\Gamma'$$ agrees with $$\Gamma$$ on the free variables in $$t_1$$, + then $$t_1$$ has type $$A\to T$$ under $$\Gamma'$$; there is a similar IH + for $$t_2$$. We must show that $$t_1\;t_2$$ also has type $$T$$ under + $$\Gamma'$$, given the assumption that $$\Gamma'$$ agrees with + $$\Gamma$$ on all the free variables in $$t_1\;t_2$$. By `app`, it + suffices to show that $$t_1$$ and $$t_2$$ each have the same type + under $$\Gamma'$$ as under $$\Gamma$$. But all free variables in + $$t_1$$ are also free in $$t_1\;t_2$$, and similarly for $$t_2$$; + hence the desired result follows from the induction hypotheses. + +
+
+weaken Γ~Γ′ (Ax Γx≡justA) rewrite (Γ~Γ′ free-varᵀ) = Ax Γ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) 
+weaken Γ~Γ′ 𝔹-I₁ = 𝔹-I₁
+weaken Γ~Γ′ 𝔹-I₂ = 𝔹-I₂
+weaken Γ~Γ′ (𝔹-E ⊢L ⊢M ⊢N)
+  = 𝔹-E (weaken (Γ~Γ′ ∘ free-ifᵀ₁) ⊢L) (weaken (Γ~Γ′ ∘ free-ifᵀ₂) ⊢M) (weaken (Γ~Γ′ ∘ 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 FreeIn 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
+-}
+
+
+ + +Now we come to the conceptual heart of the proof that reduction +preserves types---namely, the observation that _substitution_ +preserves types. + +Formally, the so-called _Substitution Lemma_ says this: Suppose we +have a term $$N$$ with a free variable $$x$$, and suppose we've been +able to assign a type $$B$$ to $$N$$ under the assumption that $$x$$ has +some type $$A$$. Also, suppose that we have some other term $$V$$ and +that we've shown that $$V$$ has type $$A$$. Then, since $$V$$ satisfies +the assumption we made about $$x$$ when typing $$N$$, we should be +able to substitute $$V$$ for each of the occurrences of $$x$$ in $$N$$ +and obtain a new term that still has type $$B$$. + +_Lemma_: If $$Γ , x ↦ A ⊢ N ∈ B$$ and $$∅ ⊢ V ∈ A$$, then +$$Γ ⊢ (N [ x := V ]) ∈ B$$. + +
+
+preservation-[:=] : ∀ {Γ x A N B V}
+                 → (Γ , x ↦ A) ⊢ N ∈ B
+                 → ∅ ⊢ V ∈ A
+                 → Γ ⊢ (N [ x := V ]) ∈ B
+
+
+ +One technical subtlety in the statement of the lemma is that +we assign $$V$$ the type $$A$$ in the _empty_ context---in other +words, we assume $$V$$ is closed. This assumption considerably +simplifies the $$λᵀ$$ case of the proof (compared to assuming +$$Γ ⊢ V ∈ A$$, which would be the other reasonable assumption +at this point) because the context invariance lemma then tells us +that $$V$$ has type $$A$$ in any context at all---we don't have to +worry about free variables in $$V$$ clashing with the variable being +introduced into the context by $$λᵀ$$. + +The substitution lemma can be viewed as a kind of "commutation" +property. Intuitively, it says that substitution and typing can +be done in either order: we can either assign types to the terms +$$N$$ and $$V$$ separately (under suitable contexts) and then combine +them using substitution, or we can substitute first and then +assign a type to $$N [ x := V ]$$---the result is the same either +way. + +_Proof_: We show, by induction on $$N$$, that for all $$A$$ and +$$Γ$$, if $$Γ , x ↦ A \vdash N ∈ B$$ and $$∅ ⊢ V ∈ A$$, then +$$Γ \vdash N [ x := V ] ∈ B$$. + + - If $$N$$ is a variable there are two cases to consider, + depending on whether $$N$$ is $$x$$ or some other variable. + + - If $$N = varᵀ x$$, then from the fact that $$Γ , x ↦ A ⊢ N ∈ B$$ + we conclude that $$A = B$$. We must show that $$x [ x := V] = + V$$ has type $$A$$ under $$Γ$$, given the assumption that + $$V$$ has type $$A$$ under the empty context. This + follows from context invariance: if a closed term has type + $$A$$ in the empty context, it has that type in any context. + + - If $$N$$ is some variable $$x′$$ different from $$x$$, then + we need only note that $$x′$$ has the same type under $$Γ , x ↦ A$$ + as under $$Γ$$. + + - If $$N$$ is an abstraction $$λᵀ x′ ∈ A′ ⇒ N′$$, then the IH tells us, + for all $$Γ′$$́ and $$B′$$, that if $$Γ′ , x ↦ A ⊢ N′ ∈ B′$$ + and $$∅ ⊢ V ∈ A$$, then $$Γ′ ⊢ N′ [ x := V ] ∈ B′$$. + + The substitution in the conclusion behaves differently + depending on whether $$x$$ and $$x′$$ are the same variable. + + First, suppose $$x ≡ x′$$. Then, by the definition of + substitution, $$N [ x := V] = N$$, so we just need to show $$Γ ⊢ N ∈ B$$. + But we know $$Γ , x ↦ A ⊢ N ∈ B$$ and, since $$x ≡ x′$$ + does not appear free in $$λᵀ x′ ∈ A′ ⇒ N′$$, the context invariance + lemma yields $$Γ ⊢ N ∈ B$$. + + Second, suppose $$x ≢ x′$$. We know $$Γ , x ↦ A , x′ ↦ A′ ⊢ N′ ∈ B′$$ + by inversion of the typing relation, from which + $$Γ , x′ ↦ A′ , x ↦ A ⊢ N′ ∈ B′$$ follows by update permute, + so the IH applies, giving us $$Γ , x′ ↦ A′ ⊢ N′ [ x := V ] ∈ B′$$ + By $$⇒-I$$, we have $$Γ ⊢ λᵀ x′ ∈ A′ ⇒ (N′ [ x := V ]) ∈ A′ ⇒ B′$$ + and the definition of substitution (noting $$x ≢ x′$$) gives + $$Γ ⊢ (λᵀ x′ ∈ A′ ⇒ N′) [ x := V ] ∈ A′ ⇒ B′$$ as required. + + - If $$N$$ is an application $$L′ ·ᵀ M′$$, the result follows + straightforwardly from the definition of substitution and the + induction hypotheses. + + - The remaining cases are similar to the application case. + +We need a couple of lemmas. A closed term can be weakened to any context, and just is injective. +
+
+weaken-closed : ∀ {V A Γ} → ∅ ⊢ V ∈ A → Γ ⊢ V ∈ A
+weaken-closed {V} {A} {Γ} ⊢V = weaken Γ~Γ′ ⊢V
+  where
+  Γ~Γ′ : ∀ {x} → x FreeIn V → ∅ x ≡ Γ x
+  Γ~Γ′ {x} x∈V = ⊥-elim (x∉V x∈V)
+    where
+    x∉V : ¬ (x FreeIn V)
+    x∉V = ∅⊢-closed ⊢V {x}
+
+just-injective : ∀ {X : Set} {x y : X} → _≡_ {A = Maybe X} (just x) (just y) → x ≡ y
+just-injective refl = refl
+
+
+ +
+
+preservation-[:=] {_} {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} {varᵀ x′} {B} {V} (Ax {.(Γ , x ↦ A)} {.x′} {.B} Γx′≡B) ⊢V with x ≟ x′
+...| yes x≡x′ rewrite just-injective Γx′≡B  =  weaken-closed ⊢V
+...| no  x≢x′  =  Ax {Γ} {x′} {B} Γx′≡B
+-}
+preservation-[:=] {Γ} {x} {A} {λᵀ x′ ∈ A′ ⇒ N′} {.A′ ⇒ B′} {V} (⇒-I {.(Γ , x ↦ A)} {.x′} {.N′} {.A′} {.B′} ⊢N′) ⊢V with x ≟ x′
+...| yes x≡x′ rewrite x≡x′ = weaken Γ′~Γ (⇒-I ⊢N′)
+  where
+  Γ′~Γ : ∀ {y} → y FreeIn (λᵀ 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
+{-
+...| yes x′≡x rewrite x′≡x | update-shadow Γ x A A′  =  {!!}
+  -- ⇒-I ⊢N′
+...| no  x′≢x rewrite update-permute Γ x′ A′ x A x′≢x  =  {!!}
+  --  ⇒-I {Γ} {x′} {N′} {A′} {B′} (preservation-[:=] {(Γ , x′ ↦ A′)} {x} {A} ⊢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)
+
+{-
+[:=]-preserves-⊢ {Γ} {x} v∶A (var y y∈Γ) with x ≟ y
+... | yes x=y = {!!}
+... | no  x≠y = {!!}
+[:=]-preserves-⊢ v∶A (abs t′∶B) = {!!}
+[:=]-preserves-⊢ v∶A (app t₁∶A⇒B t₂∶A) =
+  app ([:=]-preserves-⊢ v∶A t₁∶A⇒B) ([:=]-preserves-⊢ v∶A t₂∶A)
+[:=]-preserves-⊢ v∶A true  = true
+[:=]-preserves-⊢ v∶A false = false
+[:=]-preserves-⊢ v∶A (if t₁∶bool then t₂∶B else t₃∶B) =
+  if   [:=]-preserves-⊢ v∶A t₁∶bool
+  then [:=]-preserves-⊢ v∶A t₂∶B
+  else [:=]-preserves-⊢ v∶A t₃∶B
+-}
+
+
+ + +### Main Theorem + +We now have the tools we need to prove preservation: if a closed +term $$M$$ has type $$A$$ and takes a step to $$N$$, then $$N$$ +is also a closed term with type $$A$$. In other words, small-step +reduction preserves types. + +
+
+preservation : ∀ {M N A} → ∅ ⊢ M ∈ A → M ⟹ N → ∅ ⊢ N ∈ A
+
+
+ +_Proof_: By induction on the derivation of $$\vdash t : T$$. + +- We can immediately rule out $$var$$, $$abs$$, $$T_True$$, and + $$T_False$$ as the final rules in the derivation, since in each of + these cases $$t$$ cannot take a step. + +- If the last rule in the derivation was $$app$$, then $$t = t_1 + t_2$$. There are three cases to consider, one for each rule that + could have been used to show that $$t_1 t_2$$ takes a step to $$t'$$. + + - If $$t_1 t_2$$ takes a step by $$Sapp1$$, with $$t_1$$ stepping to + $$t_1'$$, then by the IH $$t_1'$$ has the same type as $$t_1$$, and + hence $$t_1' t_2$$ has the same type as $$t_1 t_2$$. + + - 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 + desired result now follows from the fact that substitution + preserves types. + + - If the last rule in the derivation was $$if$$, then $$t = if t_1 + then t_2 else t_3$$, and there are again three cases depending on + how $$t$$ steps. + + - If $$t$$ steps to $$t_2$$ or $$t_3$$, the result is immediate, since + $$t_2$$ and $$t_3$$ have the same type as $$t$$. + + - Otherwise, $$t$$ steps by $$Sif$$, and the desired conclusion + follows directly from the induction hypothesis. + +
+
+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
+
+-- Writing out implicit parameters in full
+-- preservation (⇒-E {Γ} {λᵀ x ∈ A ⇒ N} {M} {.A} {B} (⇒-I {.Γ} {.x} {.N} {.A} {.B} ⊢N) ⊢M) (β⇒ {.x} {.A} {.N} {.M} valueM)
+--  =  preservation-[:=] {Γ} {x} {A} {M} {N} {B} ⊢M ⊢N
+
+
+ +Proof with eauto. + remember (@empty ty) as Gamma. + intros t t' T HT. generalize dependent t'. + induction HT; + intros t' HE; subst Gamma; subst; + try solve $$inversion HE; subst; auto$$. + - (* app + inversion HE; subst... + (* Most of the cases are immediate by induction, + and $$eauto$$ takes care of them + + (* Sred + apply substitution_preserves_typing with t_{11}... + inversion HT_1... +Qed. + +#### Exercise: 2 stars, recommended (subject_expansion_stlc) +An exercise in the [Stlc]({{ "Stlc" | relative_url }}) chapter asked about the +subject expansion property for the simple language of arithmetic and boolean +expressions. Does this property hold for STLC? That is, is it always the case +that, if $$t ==> t'$$ and $$has_type t' T$$, then $$empty \vdash t : T$$? If +so, prove it. If not, give a counter-example not involving conditionals. + + +## Type Soundness + +#### Exercise: 2 stars, optional (type_soundness) +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. + +Corollary soundness : forall t t' T, + empty \vdash t : T → + t ==>* t' → + ~(stuck t'). +Proof. + intros t t' T Hhas_type Hmulti. unfold stuck. + intros $$Hnf Hnot_val$$. unfold normal_form in Hnf. + induction Hmulti. + + +## Uniqueness of Types + +#### Exercise: 3 stars (types_unique) +Another nice property of the STLC is that types are unique: a +given term (in a given context) has at most one type. +Formalize this statement and prove it. + + +## Additional Exercises + +#### Exercise: 1 star (progress_preservation_statement) +Without peeking at their statements above, write down the progress +and preservation theorems for the simply typed lambda-calculus. +$$$$ + +#### Exercise: 2 stars (stlc_variation1) +Suppose we add a new term $$zap$$ with the following reduction rule + + --------- (ST_Zap) + t ==> zap + +and the following typing rule: + + ---------------- (T_Zap) + Gamma \vdash zap : T + +Which of the following properties of the STLC remain true in +the presence of these rules? For each property, write either +"remains true" or "becomes false." If a property becomes +false, give a counterexample. + + - Determinism of $$step$$ + + - Progress + + - Preservation + + +#### Exercise: 2 stars (stlc_variation2) +Suppose instead that we add a new term $$foo$$ with the following +reduction rules: + + ----------------- (ST_Foo1) + (\lambda x:A. x) ==> foo + + ------------ (ST_Foo2) + foo ==> true + +Which of the following properties of the STLC remain true in +the presence of this rule? For each one, write either +"remains true" or else "becomes false." If a property becomes +false, give a counterexample. + + - Determinism of $$step$$ + + - Progress + + - Preservation + +#### Exercise: 2 stars (stlc_variation3) +Suppose instead that we remove the rule $$Sapp1$$ from the $$step$$ +relation. Which of the following properties of the STLC remain +true in the presence of this rule? For each one, write either +"remains true" or else "becomes false." If a property becomes +false, give a counterexample. + + - Determinism of $$step$$ + + - Progress + + - Preservation + +#### Exercise: 2 stars, optional (stlc_variation4) +Suppose instead that we add the following new rule to the +reduction relation: + + ---------------------------------- (ST_FunnyIfTrue) + (if true then t_1 else t_2) ==> true + +Which of the following properties of the STLC remain true in +the presence of this rule? For each one, write either +"remains true" or else "becomes false." If a property becomes +false, give a counterexample. + + - Determinism of $$step$$ + + - Progress + + - Preservation + + + +#### Exercise: 2 stars, optional (stlc_variation5) +Suppose instead that we add the following new rule to the typing +relation: + + Gamma \vdash t_1 : bool→bool→bool + Gamma \vdash t_2 : bool + ------------------------------ (T_FunnyApp) + Gamma \vdash t_1 t_2 : bool + +Which of the following properties of the STLC remain true in +the presence of this rule? For each one, write either +"remains true" or else "becomes false." If a property becomes +false, give a counterexample. + + - Determinism of $$step$$ + + - Progress + + - Preservation + + + +#### Exercise: 2 stars, optional (stlc_variation6) +Suppose instead that we add the following new rule to the typing +relation: + + Gamma \vdash t_1 : bool + Gamma \vdash t_2 : bool + --------------------- (T_FunnyApp') + Gamma \vdash t_1 t_2 : bool + +Which of the following properties of the STLC remain true in +the presence of this rule? For each one, write either +"remains true" or else "becomes false." If a property becomes +false, give a counterexample. + + - Determinism of $$step$$ + + - Progress + + - Preservation + + + +#### Exercise: 2 stars, optional (stlc_variation7) +Suppose we add the following new rule to the typing relation +of the STLC: + + ------------------- (T_FunnyAbs) + \vdash \lambda x:bool.t : bool + +Which of the following properties of the STLC remain true in +the presence of this rule? For each one, write either +"remains true" or else "becomes false." If a property becomes +false, give a counterexample. + + - Determinism of $$step$$ + + - Progress + + - Preservation + + +### Exercise: STLC with Arithmetic + +To see how the STLC might function as the core of a real +programming language, let's extend it with a concrete base +type of numbers and some constants and primitive +operators. + +To types, we add a base type of natural numbers (and remove +booleans, for brevity). + +Inductive ty : Type := + | TArrow : ty → ty → ty + | TNat : ty. + +To terms, we add natural number constants, along with +successor, predecessor, multiplication, and zero-testing. + +Inductive tm : Type := + | tvar : id → tm + | tapp : tm → tm → tm + | tabs : id → ty → tm → tm + | tnat : nat → tm + | tsucc : tm → tm + | tpred : tm → tm + | tmult : tm → tm → tm + | tif0 : tm → tm → tm → tm. + +#### Exercise: 4 stars (stlc_arith) +Finish formalizing the definition and properties of the STLC extended +with arithmetic. Specifically: + + - Copy the whole development of STLC that we went through above (from + the definition of values through the Type Soundness theorem), and + paste it into the file at this point. + + - Extend the definitions of the $$subst$$ operation and the $$step$$ + relation to include appropriate clauses for the arithmetic operators. + + - Extend the proofs of all the properties (up to $$soundness$$) of + the original STLC to deal with the new syntactic forms. Make + sure Agda accepts the whole file. +