From 4ea1d650a8ba36b1721d723c57aec0677d1a91ba Mon Sep 17 00:00:00 2001 From: Philip Wadler Date: Wed, 12 Jul 2017 17:14:37 +0100 Subject: [PATCH] introduction for Stlc --- out/Stlc.md | 98 +- out/StlcProp.md | 10498 ++++++++++++++++++++++++---------------------- src/Stlc.lagda | 41 +- 3 files changed, 5502 insertions(+), 5135 deletions(-) diff --git a/out/Stlc.md b/out/Stlc.md index 1836492b..ecc03cca 100644 --- a/out/Stlc.md +++ b/out/Stlc.md @@ -256,7 +256,7 @@ Syntax of types and terms. >20 _⇒_ @@ -283,41 +283,41 @@ Syntax of types and terms. > 𝔹 :_⇒_ : Type → Type → Type _⇒_ : Type → Type𝔹 →: ∶ 𝔹 ∶ 𝔹 ⇒ 𝔹 ∶ 𝔹 ∶ 𝔹 A ⇒ A ⇒ ∶ 𝔹 @@ -3314,7 +3314,7 @@ Much of the above, though not all, can be filled in using C-c C-r and C-c C-s. >∶ 𝔹 @@ -3376,7 +3376,7 @@ Much of the above, though not all, can be filled in using C-c C-r and C-c C-s. >∶ 𝔹 ∶ 𝔹 ⇒ 𝔹 @@ -3586,33 +3586,33 @@ Much of the above, though not all, can be filled in using C-c C-r and C-c C-s. > (𝔹 ⇒ 𝔹) ⇒ 𝔹 ⇒ 𝔹 diff --git a/out/StlcProp.md b/out/StlcProp.md index 9191fb82..54616b83 100644 --- a/out/StlcProp.md +++ b/out/StlcProp.md @@ -294,73 +294,118 @@ theorem. >Maps - open Maps.PartialMap using (∅Id; apply-∅_≟_; update-permutePartialMap) renaming (_,_↦_ to _,_∶_) open Maps.PartialMap using (∅; apply-∅; update-permute) renaming (_,_↦_ to _,_∶_) +open import Stlc +import Data.Nat using (ℕ) @@ -376,404 +421,404 @@ while for boolean types they are values `true` and `false`. 
 
-data canonical_for_ : Term → Type → Set where
-  canonical-λ : ∀ {x A N B} →: canonicalTerm (λ[→ Type → x ∶Set A ] N) for (A ⇒ B)where
   canonical-truecanonical-λ : ∀ {x A N B} → : canonical true(λ[ x ∶ A ] N) for 𝔹(A ⇒ B)
   canonical-falsecanonical-true : canonical falsetrue for 𝔹
+  canonical-false : canonical false for 𝔹
 
 canonical-forms : ∀ {L A} → ∅ ⊢ L ∶ A → Value L → canonical L for A
-canonical-forms (Ax⊢ L ())∶ A ()
-canonical-forms→ (⇒-IValue L → canonical L ⊢N)for value-λ = canonical-λA
 canonical-forms (⇒-EAx ⊢L()) ⊢M)()
+canonical-forms (⇒-I ()
-canonical-forms⊢N) 𝔹-I₁value-λ value-true = canonical-truecanonical-λ
 canonical-forms 𝔹-I₂(⇒-E ⊢L ⊢M) ()
+canonical-forms value-false𝔹-I₁ value-true = canonical-falsecanonical-true
 canonical-forms (𝔹-E ⊢L𝔹-I₂ value-false = canonical-false
+canonical-forms (𝔹-E ⊢L ⊢M ⊢N) ()
 
@@ -787,191 +832,191 @@ step or it is a value.
 
 
 
-data Progress : Term → Set where
-  steps : ∀ {M N} → M ⟹ N → Progress : MTerm → Set where
   done  steps : ∀ {M N} → Value M → Progress M⟹ N → Progress M
+  done  : ∀ {M} → Value M → Progress M
 
 progress : ∀ {M A} → ∅ ⊢ M ∶ A → Progress M
 
@@ -1028,451 +1073,451 @@ This completes the proof.
 
 
 
-progress (Ax ())
-progress (⇒-I ⊢N) = done value-λ
-progress (⇒-E ⊢L ⊢M)()) with progress ⊢L
 ...progress |(⇒-I steps⊢N) L⟹L′ = stepsdone value-λ
+progress (ξ·₁⇒-E L⟹L′)
-...⊢L |⊢M) with done valueL with progress ⊢M⊢L
 ... | steps M⟹M′L⟹L′ = steps (ξ·₁ L⟹L′)
+... | (ξ·₂done valueL M⟹M′)with progress ⊢M
 ... | done valueM withsteps canonical-formsM⟹M′ ⊢L valueL
-... | canonical-λ = steps (βλ·ξ·₂ valueMvalueL M⟹M′)
 progress... 𝔹-I₁| = done valueM with canonical-forms ⊢L valueL
+... | value-true
-progresscanonical-λ = steps 𝔹-I₂(βλ· = done value-false
-progress (𝔹-E ⊢L ⊢M ⊢NvalueM) with progress ⊢L
 ...progress |𝔹-I₁ steps L⟹L′ = stepsdone value-true
+progress 𝔹-I₂ = done value-false
+progress (ξif𝔹-E ⊢L L⟹L′)
-...⊢M |⊢N) with doneprogress valueL with canonical-forms ⊢L valueL
 ... | canonical-truesteps L⟹L′ = steps (ξif L⟹L′)
+... | done valueL stepswith βif-true
-... |canonical-forms canonical-false⊢L valueL
+... | canonical-true = steps βif-true
+... | canonical-false = steps βif-false
 
@@ -1493,68 +1538,68 @@ instead of induction on typing derivations.
 
 
 
-postulate
   progress′ : ∀ M {A} → ∅ ⊢ M ∶ A → Progress M
 
@@ -1616,598 +1661,598 @@ Formally:
 
 
 
-data _∈_ : Id → Term → Set where
-  free-`  : ∀ {x} → x ∈ ` x
-  free-λ  :_∈_ ∀: Id → Term {x y A N} → Set where y ≢ x → x ∈
+  free-`  : N∀ → {x} ∈→ (λ[x ∈ y` ∶x A ] N)
   free-·₁free-λ  : ∀ {x :y ∀A {xN} L→ M}y →≢ x ∈ L → x ∈ (LN → x ∈ ·(λ[ My ∶ A ] N)
   free-·₂free-·₁ : ∀ {x L M}: →∀ {x ∈L M →} x→ ∈x (∈ L ·→ M)x ∈ (L · M)
   free-if₁ : ∀ {x Lfree-·₂ M: N}∀ →{x xL ∈ L → x ∈ (if L then M} else→ Nx ∈ M → x ∈ (L · M)
   free-if₂free-if₁ : ∀ {x L M N} → x ∈ →L x→ ∈x M∈ → x(if ∈L (if L then M else N)
   free-if₃free-if₂ : ∀ {x L M N} → x ∈ →M x→ ∈x N∈ → x(if ∈L (if L then M else N)
+  free-if₃ : ∀ {x L M N} → x ∈ N → x ∈ (if L then M else N)
 
@@ -2217,131 +2262,131 @@ A term in which no variables appear free is said to be _closed_.
 
 
 
-_∉_ : Id → Term → Set
-x ∉ M = ¬ (x ∈ M)
-
-closed : Term → Set
-closed M =→ ∀ {Set
+x} →∉ xM ∉= ¬ (x ∈ M)
+
+closed : Term → Set
+closed M = ∀ {x} → x ∉ M
 
@@ -2351,240 +2396,240 @@ Here are proofs corresponding to the first two examples above.
 
 
 
-f≢x : f ≢ x
-f≢x ()
-
-example-free₁ : x ∈ (λ[ f ∶ (𝔹 ⇒ 𝔹) ] `: f ·≢ ` x)
 example-free₁ = free-λ f≢x (free-·₂ free-`)()
 
 example-free₂example-free₁ : f ∉ (λ[ f ∶ (𝔹 ⇒ 𝔹) ] ` f · ` x ∈ (λ[ f ∶ (𝔹 ⇒ 𝔹) ] ` f · ` x)
 example-free₂example-free₁ (= free-λ f≢ff≢x _)(free-·₂ free-`)
+
+example-free₂ : f ∉ (λ[ =f f≢f∶ (𝔹 ⇒ 𝔹) ] ` f · ` x)
+example-free₂ (free-λ f≢f _) = f≢f refl
 
@@ -2596,367 +2641,367 @@ Prove formally the remaining examples given above.
 
 
 
-postulate
-  example-free₃ : x ∈ ((λ[ f ∶ (𝔹 ⇒ 𝔹) ] ` f · ` x) · ` f)
   example-free₄example-free₃ : fx ∈ ((λ[ ((λ[ f ∶ (𝔹 ∶⇒ (𝔹) ⇒] 𝔹) ] ` f · ` x) `· x) · ` f)
   example-free₅example-free₄ : xf ∉∈ ((λ[ (λ[f ∶ f ∶ (𝔹 ⇒ 𝔹) ] ` ]f λ[· ` x ∶) 𝔹· ]` ` f · ` x)
   example-free₆example-free₅ : x ∉ (λ[ f ∉∶ (λ[𝔹 f⇒ ∶𝔹) (𝔹] ⇒λ[ x ∶ 𝔹) ] λ[ x` ∶f 𝔹· ]` ` f · ` x)
+  example-free₆ : f ∉ (λ[ f ∶ (𝔹 ⇒ 𝔹) ] λ[ x ∶ 𝔹 ] ` f · ` x)
 
@@ -2975,115 +3020,115 @@ then `Γ` must assign a type to `x`.
 
 
 
-free-lemma : ∀ {x M A Γ} → x ∈ M → Γ ⊢ M ∶ A → ∃ λ B → Γ x ≡ just B
 
@@ -3119,454 +3164,454 @@ _Proof_: We show, by induction on the proof that `x` appears
 
 
 
-free-lemma free-` (Ax Γx≡A) = (_ , Γx≡A)
-free-lemma (free-·₁ x∈L) (⇒-E ⊢L ⊢M) = free-lemma x∈L ⊢L
 free-lemma (free-·₂free-·₁ x∈Mx∈L) (⇒-E ⊢L ⊢L ⊢M) = free-lemma x∈Mx∈L ⊢L ⊢M
 free-lemma (free-if₁free-·₂ x∈Lx∈M) (𝔹-E⇒-E ⊢L ⊢M) ⊢M ⊢N) = free-lemma x∈M ⊢M x∈L ⊢L
 free-lemma (free-if₂free-if₁ x∈Mx∈L) (𝔹-E ⊢L ⊢M ⊢N) ⊢M ⊢N) = free-lemma x∈L ⊢L x∈M ⊢M
 free-lemma (free-if₃free-if₂ x∈Nx∈M) (𝔹-E ⊢L ⊢M ⊢N) ⊢M ⊢N) = free-lemma x∈M ⊢M x∈N ⊢N
 free-lemma (free-λfree-if₃ x∈N) {x}(𝔹-E {y}⊢L y≢x⊢M x∈N⊢N) = (⇒-I ⊢N) with free-lemma x∈N ⊢N
+free-lemma ⊢N
-... |(free-λ {Γx≡C with y ≟ x} {y} y≢x x∈N)
- ...(⇒-I |⊢N) yes y≡xwith =free-lemma ⊥-elimx∈N (y≢x y≡x)⊢N
 ... | no  _   Γx≡C with y ≟ x
+... | yes y≡x = ⊥-elim (y≢x y≡x)
+... | no  _   = Γx≡C
 
@@ -3584,68 +3629,68 @@ typed in the empty context is closed (has no free variables).
 
 
 
-postulate
   ∅⊢-closed : ∀ {M A} → ∅ ⊢ M ∶ A → closed M
 
@@ -3654,294 +3699,294 @@ typed in the empty context is closed (has no free variables).