From 36e38db1fc85c8d61d6e137e91218177986f47fe Mon Sep 17 00:00:00 2001 From: wadler Date: Wed, 28 Jun 2017 17:24:16 +0100 Subject: [PATCH] updated Stlc to new syntax --- out/StlcProp.md | 8252 ++++++++++++++++++++++---------------------- src/Maps.lagda | 4 +- src/Stlc.lagda | 183 +- src/StlcProp.lagda | 23 +- 4 files changed, 4214 insertions(+), 4248 deletions(-) diff --git a/out/StlcProp.md b/out/StlcProp.md index 45a6b18f..15722646 100644 --- a/out/StlcProp.md +++ b/out/StlcProp.md @@ -4,795 +4,793 @@ 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. +## Imports + +
{% raw %}
+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
+{% endraw %}
+ ## Canonical Forms -As we saw for the simple calculus in the [Stlc]({{ "Stlc" | relative_url }}) +As we saw for the simple calculus in the [Stlc] 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. -
-
-{% raw %}
+data canonical_for_ : canonical_for_ : Term → Type → Set where
   canonical-λᵀ : ∀ {x A N B} → canonical N B} → canonical (λᵀ x ∈ A ⇒ N) for (A ⇒ B)
   canonical-trueᵀ : canonical trueᵀ for 𝔹
   canonical-falseᵀ : 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 → 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ᵀ 𝔹-I₁ value-trueᵀ = canonical-trueᵀ    -- inj₁ refl
 canonicalFormsLemma 𝔹-I₂ value-falseᵀ = canonical-falseᵀ  -- inj₂ refl
 canonicalFormsLemma (𝔹-E ⊢L ⊢M ⊢N) ()
-
-
+{% endraw %} ## Progress @@ -803,101 +801,99 @@ 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. -
-
-{% raw %}
+progress : ∀ {M A} → ∅ ⊢ M ∈ A → A} → ∅ ⊢ M ∈ A → value M ⊎ ∃ λ N → M ⟹ N
-
-
+{% endraw %} _Proof_: By induction on the derivation of `\vdash t : A`. @@ -937,830 +933,826 @@ _Proof_: By induction on the derivation of `\vdash t : A`. - Otherwise, `t_1` takes a step, and therefore so does `t` (by `if`). -
-
-{% raw %}
+progress (Ax ())
+progress (Ax ())
-progress (⇒-I ⊢N) = inj₁ value-λᵀ
 progress (⇒-E {Γ} {L} {M} (⇒-E {Γ} {L} {M} {A} {B} ⊢L ⊢M) with progress ⊢L
 ... | inj₂ (L′ , L⟹L′) = inj₂ (L′ , L⟹L′) = inj₂ (L′ ·ᵀ M , γ⇒₁ L⟹L′)
+... | inj₁ L⟹L′)
-...valueL |with inj₁ valueL with progress ⊢M
 ... | inj₂ (M′ , M⟹M′) inj₂ (M′ , M⟹M′) = inj₂ (L ·ᵀ M′ , γ⇒₂ valueL M⟹M′)
+... valueL| inj₁ M⟹M′)
-...valueM |with inj₁ valueM with canonicalFormsLemma ⊢L valueL
 ... | canonical-λᵀ {x} canonical-λᵀ {x} {.A} {N} {.B} = inj₂ ((N [ x := M ]) , β⇒ [ x := M ]valueM) , β⇒
+progress valueM)
-progress 𝔹-I₁ = inj₁ value-trueᵀ
 progress 𝔹-I₂ = inj₁ value-falseᵀ
 progress (𝔹-E {Γ} {L} {M} (𝔹-E {Γ} {L} {M} {N} {A} ⊢L ⊢M ⊢N) with progress ⊢L
 ... | inj₂ (L′ , L⟹L′) inj₂ (L′ , L⟹L′) = inj₂ ((ifᵀ L′ then M else N) , thenγ𝔹 M else NL⟹L′)
+... | , γ𝔹inj₁ L⟹L′)
-...valueL |with inj₁ valueL with canonicalFormsLemma ⊢L valueL
 ... | canonical-trueᵀ = inj₂ (M , β𝔹₁)
 ... | canonical-falseᵀ canonical-falseᵀ = inj₂ (N , β𝔹₂)
-
-
+{% endraw %} #### 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 → A} → ∅ ⊢ M ∈ A → value M ⊎ ∃ λ N → M ⟹ N
-
-
+{% endraw %} ## Preservation @@ -1816,683 +1808,679 @@ For example: Formally: -
-
-{% raw %}
+data _FreeIn_ : Id → Term → Set where
   free-varᵀ  : ∀ {x} → x FreeIn ∀ {x}(varᵀ → x FreeIn (varᵀ x)
   free-λᵀ  : ∀ {x y A N} → y ≢ x → yx A N} →FreeIn yN ≢→ x → x FreeIn (λᵀ Ny →∈ xA FreeIn (λᵀ y ∈ A ⇒ N)
   free-·ᵀ₁ : ∀ {x L M} → x FreeIn L → x → x FreeIn (L ·ᵀ → x FreeIn (LM)
+  free-·ᵀ₂ ·ᵀ M)
-  free-·ᵀ₂ : ∀ {x L M} → x FreeIn M → x → x FreeIn M(L ·ᵀ →M)
+  free-ifᵀ₁ x FreeIn (L ·ᵀ: M)
-  free-ifᵀ₁ : ∀ {x L M N} → x FreeIn L → x → x FreeIn L → x FreeIn (ifᵀ L then M else N)
+  free-ifᵀ₂ : N)
-  free-ifᵀ₂ : ∀ {x L M N} → x FreeIn M → x → x FreeIn M → x FreeIn (ifᵀ L then M else N)
   free-ifᵀ₃ : ∀ {x L M N} → x FreeIn N → x → x FreeIn N → x FreeIn (ifᵀ L then M else N)
-
-
+{% endraw %} A term in which no variables appear free is said to be _closed_. -
-
-{% raw %}
+closed : Term → Set
+closed M = →∀ Set{x}
-closed → ¬ (x M = ∀ {x} → ¬ (x FreeIn M)
-
-
+{% endraw %} #### Exercise: 1 star (free-in) If the definition of `_FreeIn_` is not crystal clear to @@ -2509,121 +2497,119 @@ 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`. -
-
-{% raw %}
+freeLemma : ∀ {x M A Γ} → x FreeIn M → Γ →⊢ xM FreeIn M → Γ ⊢ M ∈ A → ∃ λ B → Γ x ≡ just λ B → Γ x ≡ just B
-
-
+{% endraw %} _Proof_: We show, by induction on the proof that `x` appears free in `P`, that, for all contexts `Γ`, if `P` is well @@ -2654,460 +2640,458 @@ _Proof_: We show, by induction on the proof that `x` appears assigns a type to `x`, we appeal the decidable equality for names `_≟_`, noting that `x` and `y` are different variables. -
-
-{% raw %}
+freeLemma free-varᵀ (Ax Γx≡justA) = (_ , Γx≡justA) = (_ , Γx≡justA)
 freeLemma (free-·ᵀ₁ x∈L) (⇒-E ⊢L ⊢M) x∈L) (⇒-E ⊢L ⊢M) = freeLemma x∈L ⊢L
+freeLemma x∈L ⊢L
-freeLemma (free-·ᵀ₂ x∈M) (⇒-E ⊢L ⊢M) x∈M) (⇒-E ⊢L ⊢M) = freeLemma x∈M ⊢M
+freeLemma x∈M ⊢M
-freeLemma (free-ifᵀ₁ x∈L) (𝔹-E ⊢L ⊢M ⊢N) = (𝔹-EfreeLemma x∈L ⊢L ⊢M ⊢N) = 
+freeLemma x∈L ⊢L
-freeLemma (free-ifᵀ₂ x∈M) (𝔹-E ⊢L ⊢M ⊢N) = (𝔹-EfreeLemma ⊢Lx∈M ⊢M ⊢N) = 
+freeLemma x∈M ⊢M
-freeLemma (free-ifᵀ₃ x∈N) (𝔹-E ⊢L ⊢M ⊢N) = (𝔹-EfreeLemma ⊢Lx∈N ⊢M ⊢N) = 
+freeLemma x∈N(free-λᵀ ⊢N
-freeLemma{x} {y} (free-λᵀy≢x x∈N) {x} {y} y≢x x∈N) (⇒-I ⊢N) with freeLemma x∈N ⊢N
 ... | Γx=justC with y ≟ x
+... | withyes yy≡x ≟= x
-... |⊥-elim yes y≡x = ⊥-elim (y≢x y≡x)
 ... | no  _   = Γx=justC
-
-
+{% endraw %} [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 @@ -3118,370 +3102,366 @@ the empty context is closed (it has no free variables). #### Exercise: 2 stars, optional (∅⊢-closed) -
-
-{% raw %}
+postulate
   ∅⊢-closed : ∀ {M A} → ∅ ⊢ M ∈ A → A} → ∅closed ⊢ M ∈ A → closed M
-
-
+{% endraw %} Sometimes, when we have a proof `Γ ⊢ M ∈ A`, we will need to @@ -3491,150 +3471,148 @@ to do this? Intuitively, it must at least be the case that that appear free in `M`. In fact, this is the only condition that is needed. -
-
-{% raw %}
+weaken : ∀ {Γ Γ′ M A}
+        → (∀ {x}
-        → (∀→ x FreeIn M {x}→ Γ →x x≡ FreeIn M → Γ x ≡ Γ′ x)
         → Γ  ⊢ M ∈ A
+        → Γ′ ∈⊢ A
-        → Γ′ ⊢ M ∈ A
-
-
+{% endraw %} _Proof_: By induction on the derivation of `Γ ⊢ M ∈ A`. @@ -3678,202 +3656,233 @@ _Proof_: By induction on the derivation of `t_1` are also free in `t_1\;t_2`, and similarly for `t_2`; hence the desired result follows from the induction hypotheses. -
-
-{% raw %}
+weaken Γ~Γ′ (Ax Γx≡justA) rewrite (Γ~Γ′ free-varᵀ) (Γ~Γ′ free-varᵀ) = Ax Γx≡justA
 weaken {Γ} {Γ′} {λᵀ x ∈ {Γ}A ⇒ {Γ′N} {λᵀΓ~Γ′ x ∈(⇒-I A ⇒⊢N) N} Γ~Γ′ (⇒-I ⊢N) = ⇒-I (weaken Γx~Γ′x ⊢N)
   where
   Γx~Γ′x : ∀ {y} → y FreeIn ∀N {y→ } → y FreeIn N → (Γ , x ↦ A) y ≡ (Γ′ , x ↦ A) y ≡ (Γ′ , x ↦ A) y
   Γx~Γ′x {y} y∈N with x ≟ {y} y∈N
+  ... with x ≟ y
-  ... | yes refl = refl
   ... | no  x≢y  = Γ~Γ′ (free-λᵀ x≢y y∈N)
+weaken Γ~Γ′ y∈N)(⇒-E
-weaken ⊢L ⊢M) Γ~Γ′ (⇒-E ⊢L ⊢M) = ⇒-E (weaken (Γ~Γ′ ∘ free-·ᵀ₁)  ⊢L) ∘ free-·ᵀ₁)  ⊢L) (weaken (Γ~Γ′ ∘ free-·ᵀ₂) ⊢M) 
 weaken Γ~Γ′ 𝔹-I₁ = 𝔹-I₁
+weaken Γ~Γ′ 𝔹-I₁𝔹-I₂ = 𝔹-I₂
 weaken Γ~Γ′ 𝔹-I₂ = 𝔹-I₂
-weaken Γ~Γ′ (𝔹-E ⊢L ⊢M ⊢N)
   = 𝔹-E (weaken (Γ~Γ′ ∘ free-ifᵀ₁) ⊢L) ∘ free-ifᵀ₁) ⊢L) (weaken (Γ~Γ′ ∘ free-ifᵀ₂) ⊢M) ∘ free-ifᵀ₂) ⊢M) (weaken (Γ~Γ′ ∘ free-ifᵀ₃) ⊢N)
 
 {-
 replaceCtxt f (var x x∶A
 ) rewrite f var = var x x∶A
@@ -4298,8 +4275,7 @@ replaceCtxt f (if t₁∶bool then t₂∶A else t₃∶
     else replaceCtxt (f ∘ if3) t₃∶A
 -}
-
-
+{% endraw %} Now we come to the conceptual heart of the proof that reduction @@ -4318,168 +4294,166 @@ and obtain a new term that still has type `B`. _Lemma_: If `Γ , x ↦ A ⊢ N ∈ B` and `∅ ⊢ V ∈ A`, then `Γ ⊢ (N [ x := V ]) ∈ B`. -
-
-{% raw %}
+preservation-[:=] : ∀ {Γ x A N B V}
                  → (Γ , x ↦ A) ⊢ N ∈ B
                  → ∅ ⊢ V ∈ A
                  → Γ ⊢ (N [ x := V ]) ⊢∈ (N [ x := V ]) ∈ B
-
-
+{% endraw %} One technical subtlety in the statement of the lemma is that we assign `V` the type `A` in the _empty_ context---in other @@ -4545,1345 +4519,1341 @@ _Proof_: We show, by induction on `N`, that for all `A` and - 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. -
-
-{% raw %}
+weaken-closed : ∀ {V A Γ} → ∅ ⊢ V ∈ A A→ Γ} → ∅ ⊢ V ∈ A → Γ ⊢ V ∈ A
 weaken-closed {V} {A} {Γ} ⊢V = {V}weaken {A} {Γ}Γ~Γ′ ⊢V = weaken Γ~Γ′ ⊢V
   where
   Γ~Γ′ : ∀ {x} → x FreeIn ∀V {x}→ ∅ →x x≡ FreeIn V → ∅ x ≡ Γ x
   Γ~Γ′ {x} x∈V = ⊥-elim {x}(x∉V 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} :→ Set}_≡_ {xA y= : X}Maybe →X} _≡_ {A(just = Maybe X} (just x) (just y) → x ≡ y
+just-injective y
-just-injective refl = refl
+{% endraw %}
- - -
-
-{% raw %}
+preservation-[:=] {_} {x} (Ax {_} {x′} {x} (Ax {_} {x′} [Γ,x↦A]x′≡B) ⊢V with x ≟ x′
+...| withyes x ≟x≡x′ x′
-...|rewrite 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′ ∈ {x} {A} {λᵀ x′ ∈ A′ ⇒ N′} {.A′ ⇒ B′} ⇒ N′} {.A′ ⇒ B′V} (⇒-I ⊢N′) ⊢V {V}with (⇒-Ix ≟ ⊢N′) ⊢V with x ≟ x′
 ...| yes x≡x′ rewrite yes x≡x′ rewrite x≡x′ = weaken Γ′~Γ (⇒-I weaken Γ′~Γ (⇒-I ⊢N′)
   where
   Γ′~Γ : ∀ {y} → y FreeIn ∀ {y} → y FreeIn (λᵀ x′ ∈ A′ ⇒ N′) → (Γ , x′ ↦ A) y →≡ (Γ , x′ ↦ A) y
+  Γ′~Γ {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′ N′ ∈ B′
-  x′x⊢N′ rewrite update-permute Γ update-permutex A x′ A′ x≢x′ Γ= 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 = ⇒-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 %} ### Main Theorem @@ -5893,101 +5863,99 @@ 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. -
-
-{% raw %}
+preservation : ∀ {M N A} → ∅ ⊢ M ∈ A N→ A} → ∅ ⊢ M ∈ A → M ⟹ N → ∅ ⊢ N ∈ A
-
-
+{% endraw %} _Proof_: By induction on the derivation of `\vdash t : T`. @@ -6020,457 +5988,455 @@ _Proof_: By induction on the derivation of `\vdash t : T`. - Otherwise, `t` steps by `Sif`, and the desired conclusion follows directly from the induction hypothesis. -
-
-{% raw %}
+preservation (Ax x₁) ()
 preservation (⇒-I ⊢N) ()
 preservation (⇒-E (⇒-I ⊢N) ⊢V) (β⇒ (⇒-I ⊢N) ⊢V) (β⇒ valueV) = preservation-[:=] ⊢N ⊢V
 preservation (⇒-E ⊢L ⊢M) (γ⇒₁ (⇒-E ⊢L ⊢M) (γ⇒₁ L⟹L′) with preservation ⊢L L⟹L′
+...| ⊢L′ ⊢L L⟹L′
-...| ⊢L′ = ⇒-E ⊢L′ ⊢M
 preservation (⇒-E ⊢L ⊢M) (γ⇒₂ (⇒-E ⊢L ⊢M) (γ⇒₂ valueL M⟹M′) with preservation ⊢M M⟹M′
+...| ⊢M′ ⊢M= M⟹M′⇒-E ⊢L ⊢M′
 ...| ⊢M′ = ⇒-E ⊢Lpreservation ⊢M′
-preservation 𝔹-I₁ ()
 preservation 𝔹-I₂ ()
 preservation (𝔹-E 𝔹-I₁ ⊢M ⊢N) (𝔹-E 𝔹-I₁ ⊢M ⊢N) β𝔹₁ = ⊢M
 preservation (𝔹-E 𝔹-I₂ ⊢M ⊢N) (𝔹-E 𝔹-I₂ ⊢M ⊢N) β𝔹₂ = ⊢N
 preservation (𝔹-E ⊢L ⊢M ⊢N) (γ𝔹 L⟹L′) ⊢M ⊢N) (γ𝔹 L⟹L′) with preservation ⊢L L⟹L′
+...| ⊢L′ ⊢L= L⟹L′
-...|𝔹-E ⊢L′ ⊢M ⊢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
-
-
+{% endraw %} Proof with eauto. remember (@empty ty) as Gamma. diff --git a/src/Maps.lagda b/src/Maps.lagda index a8d8040d..08b2d397 100644 --- a/src/Maps.lagda +++ b/src/Maps.lagda @@ -131,7 +131,7 @@ 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. \begin{code} - infixl 100 _,_↦_ + infixl 15 _,_↦_ _,_↦_ : ∀ {A} → TotalMap A → Id → A → TotalMap A (ρ , x ↦ v) y with x ≟ y @@ -335,7 +335,7 @@ module PartialMap where \end{code} \begin{code} - infixl 100 _,_↦_ + infixl 15 _,_↦_ _,_↦_ : ∀ {A} (ρ : PartialMap A) (x : Id) (v : A) → PartialMap A ρ , x ↦ v = TotalMap._,_↦_ ρ x (just v) diff --git a/src/Stlc.lagda b/src/Stlc.lagda index 66dd686b..effbcf7d 100644 --- a/src/Stlc.lagda +++ b/src/Stlc.lagda @@ -14,7 +14,6 @@ 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 as P using (_≡_; _≢_; refl) @@ -28,23 +27,26 @@ import Relation.Binary.PreorderReasoning as PreorderReasoning ## Syntax -Syntax of types and terms. All source terms are labeled with $ᵀ$. +Syntax of types and terms. \begin{code} -infixr 100 _⇒_ -infixl 100 _·ᵀ_ +infixr 20 _⇒_ data Type : Set where 𝔹 : Type _⇒_ : Type → Type → Type +infixl 20 _·_ +infix 15 λ[_∶_]_ +infix 15 if_then_else_ + 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 + var : Id → Term + λ[_∶_]_ : Id → Type → Term → Term + _·_ : Term → Term → Term + true : Term + false : Term + if_then_else_ : Term → Term → Term → Term \end{code} Some examples. @@ -54,58 +56,63 @@ 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ᵀ)) +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) + +check : not ≡ λ[ x ∶ 𝔹 ] (if var x then false else true) +check = refl \end{code} ## Values \begin{code} -data value : Term → Set where - value-λᵀ : ∀ {x A N} → value (λᵀ x ∈ A ⇒ N) - value-trueᵀ : value (trueᵀ) - value-falseᵀ : value (falseᵀ) +data Value : Term → Set where + value-λ : ∀ {x A N} → Value (λ[ x ∶ A ] N) + value-true : Value true + value-false : Value false \end{code} ## Substitution \begin{code} -_[_:=_] : Term → Id → Term → Term -(varᵀ x′) [ x := V ] with x ≟ x′ +_[_∶=_] : 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 ]) +... | 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 ]) \end{code} ## Reduction rules \begin{code} +infix 10 _⟹_ + data _⟹_ : Term → Term → Set where - β⇒ : ∀ {x A N V} → value V → - ((λᵀ x ∈ A ⇒ N) ·ᵀ V) ⟹ (N [ x := V ]) + β⇒ : ∀ {x A N V} → Value V → + (λ[ x ∶ A ] N) · V ⟹ N [ x ∶= V ] γ⇒₁ : ∀ {L L' M} → L ⟹ L' → - (L ·ᵀ M) ⟹ (L' ·ᵀ M) + L · M ⟹ L' · M γ⇒₂ : ∀ {V M M'} → - value V → + Value V → M ⟹ M' → - (V ·ᵀ M) ⟹ (V ·ᵀ M') + V · M ⟹ V · M' β𝔹₁ : ∀ {M N} → - (ifᵀ trueᵀ then M else N) ⟹ M + if true then M else N ⟹ M β𝔹₂ : ∀ {M N} → - (ifᵀ falseᵀ then M else N) ⟹ 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) + if L then M else N ⟹ if L' then M else N \end{code} ## Reflexive and transitive closure of a relation @@ -114,7 +121,7 @@ data _⟹_ : Term → Term → Set where Rel : Set → Set₁ Rel A = A → A → Set -infixl 100 _>>_ +infixl 10 _>>_ data _* {A : Set} (R : Rel A) : Rel A where ⟨⟩ : ∀ {x : A} → (R *) x x @@ -123,9 +130,9 @@ data _* {A : Set} (R : Rel A) : Rel A where \end{code} \begin{code} -infix 80 _⟹*_ +infix 10 _⟹*_ -_⟹*_ : Term → Term → Set +_⟹*_ : Rel Term _⟹*_ = (_⟹_) * \end{code} @@ -143,54 +150,42 @@ _⟹*_ = (_⟹_) * } open PreorderReasoning ⟹*-Preorder - using (begin_; _∎) renaming (_≈⟨_⟩_ to _≡⟨_⟩_; _∼⟨_⟩_ to _⟹*⟨_⟩_) + using (_IsRelatedTo_; begin_; _∎) renaming (_≈⟨_⟩_ to _≡⟨_⟩_; _∼⟨_⟩_ to _⟹*⟨_⟩_) + +infixr 2 _⟹*⟪_⟫_ + +_⟹*⟪_⟫_ : ∀ x {y z} → x ⟹ y → y IsRelatedTo z → x IsRelatedTo z +x ⟹*⟪ x⟹y ⟫ yz = x ⟹*⟨ ⟨ x⟹y ⟩ ⟩ yz \end{code} Example evaluation. \begin{code} -example₀′ : not[𝔹] ·ᵀ trueᵀ ⟹* falseᵀ -example₀′ = +example₀ : not · true ⟹* false +example₀ = begin - not[𝔹] ·ᵀ trueᵀ - ⟹*⟨ ⟨ β⇒ value-trueᵀ ⟩ ⟩ - ifᵀ trueᵀ then falseᵀ else trueᵀ - ⟹*⟨ ⟨ β𝔹₁ ⟩ ⟩ - falseᵀ + not · true + ⟹*⟪ β⇒ value-true ⟫ + if true then false else 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-λᵀ β𝔹₂ - step₃ : M₃ ⟹ M₄ - step₃ = β⇒ value-trueᵀ - step₄ : M₄ ⟹ M₅ - step₄ = β⇒ value-trueᵀ +example₁ : I² · I · (not · false) ⟹* true +example₁ = + begin + I² · I · (not · false) + ⟹*⟪ γ⇒₁ (β⇒ value-λ) ⟫ + (λ[ x ∶ 𝔹 ] I · var x) · (not · false) + ⟹*⟪ γ⇒₂ value-λ (β⇒ value-false) ⟫ + (λ[ x ∶ 𝔹 ] I · var x) · (if false then false else true) + ⟹*⟪ γ⇒₂ value-λ β𝔹₂ ⟫ + (λ[ x ∶ 𝔹 ] I · var x) · true + ⟹*⟪ β⇒ value-true ⟫ + I · true + ⟹*⟪ β⇒ value-true ⟫ + true + ∎ \end{code} ## Type rules @@ -199,26 +194,26 @@ example₁ = ⟨ step₀ ⟩ >> ⟨ step₁ ⟩ >> ⟨ step₂ ⟩ >> ⟨ step Context : Set Context = PartialMap Type -infix 50 _⊢_∈_ +infix 10 _⊢_∶_ -data _⊢_∈_ : Context → Term → Type → Set where +data _⊢_∶_ : Context → Term → Type → Set where Ax : ∀ {Γ x A} → Γ x ≡ just A → - Γ ⊢ varᵀ x ∈ A + Γ ⊢ var x ∶ A ⇒-I : ∀ {Γ x N A B} → - (Γ , x ↦ A) ⊢ N ∈ B → - Γ ⊢ (λᵀ x ∈ A ⇒ 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 + Γ ⊢ 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ᵀ L then M else N) ∈ A + Γ ⊢ L ∶ 𝔹 → + Γ ⊢ M ∶ A → + Γ ⊢ N ∶ A → + Γ ⊢ if L then M else N ∶ A \end{code} diff --git a/src/StlcProp.lagda b/src/StlcProp.lagda index 14ba4032..4d2f503b 100644 --- a/src/StlcProp.lagda +++ b/src/StlcProp.lagda @@ -4,6 +4,12 @@ layout : page permalink : /StlcProp --- +In this chapter, we develop the fundamental theory of the Simply +Typed Lambda Calculus---in particular, the type safety +theorem. + +## Imports + \begin{code} open import Function using (_∘_) open import Data.Empty using (⊥; ⊥-elim) @@ -18,10 +24,6 @@ open Maps.PartialMap open import Stlc \end{code} -In this chapter, we develop the fundamental theory of the Simply -Typed Lambda Calculus---in particular, the type safety -theorem. - ## Canonical Forms @@ -54,16 +56,19 @@ canonicalFormsLemma (𝔹-E ⊢L ⊢M ⊢N) () 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. \begin{code} progress : ∀ {M A} → ∅ ⊢ M ∈ A → value M ⊎ ∃ λ N → M ⟹ N \end{code} -_Proof_: By induction on the derivation of `\vdash t : A`. +The proof is a relatively +straightforward extension of the progress proof we saw in the +[Types]({{ "Types" | relative_url }}) chapter. +We'll give the proof in English +first, then the formal version. + +_Proof_: By induction on the derivation of `∅ ⊢ M ∈ A`. - The last rule of the derivation cannot be `var`, since a variable is never well typed in an empty context.