From ec46d635c06da971dcbc792ab1626a5a34e77267 Mon Sep 17 00:00:00 2001 From: wadler Date: Thu, 29 Jun 2017 23:05:23 +0100 Subject: [PATCH] inductive data type for progress --- out/Stlc.md | 47 +- out/StlcProp.md | 8012 +++++++++++++++++++++----------------------- src/Stlc.lagda | 47 +- src/StlcProp.lagda | 84 +- 4 files changed, 3995 insertions(+), 4195 deletions(-) diff --git a/out/Stlc.md b/out/Stlc.md index 2603053a..249d5263 100644 --- a/out/Stlc.md +++ b/out/Stlc.md @@ -4100,36 +4100,35 @@ Example terms. Construction of a type derivation is best done interactively. We start with the declaration: - `typing₁ : ∅ ⊢ not ∶ 𝔹 ⇒ 𝔹` - `typing₁ = ?` + typing₁ : ∅ ⊢ not ∶ 𝔹 ⇒ 𝔹 + typing₁ = ? -Typing control-L causes Agda to create a hole and tell us its expected type. +Typing C-L (control L) causes Agda to create a hole and tell us its +expected type. - `typing₁ = { }0` - `?0 : ∅ ⊢ not ∶ 𝔹 ⇒ 𝔹` + 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. +Now we fill in the hole by typing C-R (control R). Agda observes that +the outermost term in `not` in a `λ`, which is typed using `⇒-I`. The +`⇒-I` rule in turn takes one argument, which Agda leaves as a hole. - `typing₁ = ⇒-I { }0` - `?0 : ∅ , x ∶ 𝔹 ⊢ if var x then false else true ∶ 𝔹` + 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. +Again we fill in the hole by typing C-R. Agda observes that the +outermost term is now `if_then_else_`, which is typed using `𝔹-E`. The +`𝔹-E` rule in turn takes three arguments, which Agda leaves as holes. - `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. + typing₁ = ⇒-I (𝔹-E { }0 { }1 { }2) + ?0 : ∅ , x ∶ 𝔹 ⊢ var x ∶ + ?1 : ∅ , x ∶ 𝔹 ⊢ false ∶ 𝔹 + ?2 : ∅ , x ∶ 𝔹 ⊢ true ∶ 𝔹 +Again we fill in the three holes by typing C-R in each. Agda observes +that `var x`, `false`, and `true` are typed using `Ax`, `𝔹-I₂`, and +`𝔹-I₁` respectively. The `Ax` rule in turn takes an argument, to show +that `(∅ , x ∶ 𝔹) x = just 𝔹`, which can in turn be specified with a +hole. After filling in all holes, the term is as above. diff --git a/out/StlcProp.md b/out/StlcProp.md index 5dce75b7..cf7cf557 100644 --- a/out/StlcProp.md +++ b/out/StlcProp.md @@ -635,10 +635,8 @@ while for boolean types they are values `true` and `false`. >Ax ⊢x)()) {% raw %} -progressdata :Progress ∀: Term → Set where + steps : ∀ {M A} → ∅ ⊢ M ∶ A → Value M ⊎ ∃ λ N} → M ⟹ N → Progress M + done : ∀ {M} → Value M → Progress M + +progress : ∀ {M A} → ∅ ⊢ M ∶ A → Progress M {% endraw %} @@ -888,751 +982,485 @@ _Proof_: By induction on the derivation of `∅ ⊢ M ∶ A`. - 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 `L` is a value then consider `M`. By the second induction - hypothesis, either `M` is a value or it can take a step. - - - 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 `β⇒`. - - - If `M` can take a step, then so can `L · M` by `γ⇒₂`. + hypotheses. By the first induction hypothesis, either `L` + can take a step or is a value. - If `L` can take a step, then so can `L · M` by `γ⇒₁`. + - If `L` is a value then consider `M`. By the second induction + hypothesis, either `M` can take a step or is a value. + + - If `M` can take a step, then so can `L · M` by `γ⇒₂`. + + - If `M` is a value, then since `L` is a value with a + function type we know from the canonical forms lemma + that it must be a lambda abstraction, + and hence `L · M` can take a step by `β⇒`. + - 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 `L` is a value, then since it has type boolean it must be - either `true` or `false`. - - - If `L` is `true`, then then term steps by `β𝔹₁` - - - If `L` is `false`, then then term steps by `β𝔹₂` + By the induction hypothesis, either `L` can take a step or is + a value. - If `L` can take a step, then so can `if L then M else N` by `γ𝔹`. + - If `L` is a value, then since it has type boolean we know from + the canonical forms lemma that it must be either `true` or + `false`. + + - If `L` is `true`, then `if L then M else N` steps by `β𝔹₁` + + - If `L` is `false`, then `if L then M else N` steps 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′) =())
+progress inj₂ (L⇒-I · M′ , γ⇒₂ valueL M⟹M′⊢N) = done value-λ
 ...progress |(⇒-E inj₁ valueM with canonicalFormsLemma ⊢L valueL⊢M) with progress ⊢L
 ... | canonical-λsteps L⟹L′ = steps (γ⇒₁ {x} L⟹L′{.A})
+... {N}| {.B}done =valueL inj₂ ((Nwith [ x ∶= Mprogress ])⊢M , β⇒ valueM)
 progress... 𝔹-I₁| steps M⟹M′ = inj₁steps value-true(γ⇒₂ valueL M⟹M′)
 progress... | done 𝔹-I₂ =valueM inj₁with value-falsecanonicalFormsLemma ⊢L valueL
 progress (𝔹-E {Γ} {L}... {M}| {N}canonical-λ {A}= ⊢L ⊢M ⊢N)steps with(β⇒ progress ⊢LvalueM)
 ...progress |𝔹-I₁ inj₂= (L′done ,value-true
+progress L⟹L′)𝔹-I₂ = inj₂ ((if L′ then Mdone else N) , γ𝔹 L⟹L′)value-false
 ...progress |(𝔹-E inj₁⊢L valueL⊢M ⊢N) with canonicalFormsLemmaprogress ⊢L
+... | ⊢Lsteps valueLL⟹L′ = steps (γ𝔹 L⟹L′)
 ... | canonical-true = inj₂| (Mdone ,valueL β𝔹₁)
-...with | canonical-false =canonicalFormsLemma inj₂⊢L (N ,valueL
+... | canonical-true = steps β𝔹₁
+... | canonical-false = steps β𝔹₂)
 {% endraw %}
@@ -1641,101 +1469,69 @@ Show that progress can also be proved by induction on terms instead of induction on typing derivations. 
{% raw %}
-postulate
   progress′ : ∀ M {M A} → ∅ ⊢ M ∶ A → ValueProgress M ⊎ ∃ λ N → M ⟹ N
 {% endraw %}
@@ -1794,602 +1590,602 @@ For example: Formally: 
{% raw %}
-data _∈_ : Id → Term → Set where
-  free-var  : ∀ {x} → x ∈ (var x)
-  free-λ  : ∀ {x y A N} →where
+  free-var  : y∀ ≢ {x} → x ∈ N → x ∈(var (λ[ y ∶ A ] Nx)
   free-·₁ free-λ  : ∀ {x y A N} ∀→ {y ≢ x L M}→ →x x∈ ∈N L→ →x x∈ ∈ (Lλ[ ·y M)∶ A ] N)
   free-·₂free-·₁ : ∀ {x L∀ M}{x →L x ∈ M} → x ∈ (L → x ·∈ M)(L · M)
   free-if₁ : ∀free-·₂ : ∀ {x L Mx N}L M→} x→ ∈x L∈ →M x→ ∈x ∈ (if L then· M else N)
   free-if₂free-if₁ : ∀ {x L M :N} ∀→ {x L∈ ML N} → x ∈ M(if →L x ∈then (if L then M else N)
   free-if₃free-if₂ : ∀ {x L M :N} ∀→ {x L∈ M N} → x ∈ N(if →L x ∈then (if L then M else N)
+  free-if₃ : ∀ {x L M N} → x ∈ N → x ∈ (if L then M else N)
 {% endraw %}
@@ -2397,72 +2193,72 @@ Formally: A term in which no variables appear free is said to be _closed_. 
{% raw %}
-closed : Term → Set
 closed M = ∀ {x} → ¬ (x ∈ M)
 {% endraw %}
@@ -2483,115 +2279,115 @@ well typed in context `Γ`, then it must be the case that `Γ` assigns a type to `x`. 
{% raw %}
-freeLemma : ∀ {x M A Γ} → x ∈ M → Γ ⊢ M ∶ A → ∃ λ B → Γ x ≡ just B
 {% endraw %}
@@ -2626,454 +2422,454 @@ _Proof_: We show, by induction on the proof that `x` appears `_≟_`, noting that `x` and `y` are different variables. 
{% raw %}
-freeLemma free-var (Ax Γx≡justA) = (_ , Γx≡justA)
-freeLemma (free-·₁ x∈L) (⇒-E ⊢L ⊢M) = freeLemma(_ x∈L, ⊢LΓx≡justA)
 freeLemma (free-·₂free-·₁ x∈Mx∈L) (⇒-E ⊢L ⊢M) = ⊢M) = freeLemma x∈Mx∈L ⊢M⊢L
 freeLemma (free-if₁free-·₂ x∈Lx∈M) (𝔹-E⇒-E ⊢L ⊢M) ⊢L ⊢M ⊢N) = freeLemma freeLemmax∈M x∈L ⊢L⊢M
 freeLemma (free-if₁ x∈L) (free-if₂𝔹-E x∈M)⊢L (𝔹-E⊢M ⊢N) ⊢L ⊢M ⊢N) = freeLemma freeLemmax∈L x∈M ⊢M⊢L
 freeLemma (free-if₂ x∈M) (free-if₃𝔹-E x∈N)⊢L (𝔹-E⊢M ⊢N) ⊢L ⊢M ⊢N) = freeLemma freeLemmax∈M x∈N ⊢N⊢M
 freeLemma (free-if₃ x∈N) (free-λ𝔹-E {x}⊢L {y}⊢M y≢x⊢N) = freeLemma x∈N) (⇒-I ⊢N) with 
+freeLemma x∈N(free-λ ⊢N
-... | Γx=justC with y ≟ {x
-...} |{y} y≢x x∈N) (⇒-I ⊢N) with yes y≡x =freeLemma ⊥-elimx∈N ⊢N (y≢x y≡x)
 ... | no  _Γx=justC with y   = ≟ x
+... | yes y≡x = ⊥-elim (y≢x y≡x)
+... | no  _   = Γx=justC
 {% endraw %}
@@ -3088,362 +2884,362 @@ the empty context is closed (it has no free variables). #### Exercise: 2 stars, optional (∅⊢-closed) 
{% raw %}
-postulate
   ∅⊢-closed : ∀ {M A} → ∅ ⊢ M ∶ A → closed M
 {% endraw %}