diff --git a/out/StlcProp.md b/out/StlcProp.md index 627f6b79..d98d62e2 100644 --- a/out/StlcProp.md +++ b/out/StlcProp.md @@ -554,226 +554,226 @@ while for boolean types they are values `true` and `false`. canonicalFormsLemmacanonical-forms : ∀ : ∀ {L A} → ∅ →⊢ ∅L ⊢∶ LA ∶→ A → Value L → L → canonical L for for A canonicalFormsLemmacanonical-forms (Ax ()) (Ax ()) () canonicalFormsLemmacanonical-forms (⇒-I ⊢N) value-λ ⊢N) value-λ = canonical-λ canonicalFormsLemmacanonical-forms (⇒-E ⊢L ⊢M) () +canonical-forms -canonicalFormsLemma 𝔹-I₁ value-true = canonical-true canonicalFormsLemmacanonical-forms 𝔹-I₂ value-false = canonical-false canonicalFormsLemmacanonical-forms (𝔹-E ⊢L ⊢M ⊢N) () @@ -787,191 +787,191 @@ step or it is a value. 
 
-data Progress : Term → Set where
+  steps : ∀ {M N} Set→ M where⟹ N → Progress M
   steps : ∀ {M N}done  : →∀ {M} ⟹ N → ProgressValue M M→
-  done  : ∀ {M} → Value M → Progress M
 
 progress : ∀ {M A} → ∅ ⊢ M ∶ A → Progress M
 
@@ -1028,451 +1028,451 @@ This completes the proof.
 
 
 
-progress (Ax ())
+progress (⇒-I ⊢N) = (Axdone ())value-λ
 progress (⇒-I ⊢N(⇒-E ⊢L ⊢M) =with doneprogress value-λ⊢L
 progress (⇒-E... ⊢L| ⊢M)steps withL⟹L′ progress= steps ⊢L(ξ·₁ L⟹L′)
 ... | steps L⟹L′| =done stepsvalueL (ξ·₁with L⟹L′)
-...progress | done⊢M
+... valueL| withsteps progressM⟹M′ = steps ⊢M(ξ·₂ valueL M⟹M′)
 ... | steps M⟹M′ = steps (ξ·₂ valueL M⟹M′)
-... | done valueM with canonical-forms valueM with canonicalFormsLemma ⊢L valueL
 ... | canonical-λ = steps (βλ· valueM)
+progress 𝔹-I₁ = done value-true
 progress 𝔹-I₁𝔹-I₂ = done value-truevalue-false
 progress 𝔹-I₂(𝔹-E =⊢L done⊢M value-false
-progress (𝔹-E ⊢L ⊢M ⊢N) with progress ⊢L
 ... | steps L⟹L′ = steps (ξif L⟹L′)
 ... | done valueL with canonical-forms ⊢L valueL
+... | canonicalFormsLemmacanonical-true ⊢L= steps valueLβif-true
 ... | canonical-true = steps βif-true
-... | canonical-false = steps βif-false
 
@@ -1493,68 +1493,68 @@ instead of induction on typing derivations.
 
 
 
-postulate
   progress′ : ∀ M {A} → ∅ ⊢ M ∶ A → Progress M
 
@@ -1616,598 +1616,598 @@ Formally:
 
 
 
-data _∈_ : Id → Term → Set where
+  free-`  : :∀ Id{x} → Termx ∈ →` Set wherex
   free-`free-λ  : ∀ {x y A N} → →y x≢ ∈x `→ x
-  free-λ  : ∀∈ N → x ∈ (λ[ {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 ∈ (L · M) → x ∈ (L · M)
   free-·₂ : ∀ {x Lfree-if₁ M}: →∀ {x ∈L M N} → x ∈ (L ·L → x ∈ (if L then M else N)
   free-if₁ : ∀ {x L M N} → x ∈ L →free-if₂ x: ∈∀ (if{x L then M elseN} → x ∈ M → x ∈ (if L then M else N)
   free-if₂ : ∀ {x L M N} → x ∈ M →free-if₃ x: ∈∀ (if{x L then M elseN} → x ∈ N N)
-  free-if₃ : ∀ {x L M N} → x ∈ N → x ∈ (if L then M else N)
 
@@ -2217,131 +2217,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 = ∀ {x} → x ∉ M
 
@@ -2351,240 +2351,240 @@ Here are proofs corresponding to the first two examples above.
 
 
 
-f≢x : f ≢ x
+f≢x ()
+
+example-free₁ : x ∈ : f(λ[ ≢f x
-f≢x ()
-
-example-free₁ : x ∈ (λ[ f ∶ (𝔹 ⇒ 𝔹) ] ` f · ` x)
+example-free₁ = free-λ ] `f≢x f · ` x)
-example-free₁ = free-λ f≢x (free-·₂ free-`)
 
 example-free₂ : f ∉ (λ[ f ∶ (𝔹 ⇒ 𝔹) ] ` f · ` x)
 example-free₂ (free-λ f≢f _) = f≢f refl
 
@@ -2596,367 +2596,367 @@ Prove formally the remaining examples given above.
 
 
 
-postulate
   example-free₃ : x ∈ ((λ[ f ∶ (𝔹 ⇒ 𝔹) ] ` f · ` x) :· x` ∈ ((λ[ f ∶ (𝔹 ⇒ 𝔹)
+  example-free₄ ]: `f f∈ ·((λ[ ` x)f ·∶ `(𝔹 f)⇒
-  example-free₄ 𝔹) ] ` f · ` x) :· f` ∈ ((λ[ f ∶ (𝔹 ⇒ 𝔹)
+  example-free₅ ]: `x f∉ · `(λ[ x)f ·∶ `(𝔹 f⇒ 𝔹) ] λ[ x ∶ 𝔹 ] ` f · ` x)
   example-free₅example-free₆ : xf ∉ (λ[ f ∶ (𝔹 ⇒ 𝔹) ] λ[ x ∶ 𝔹 ]λ[ ` f ·∶ `(𝔹 x)
-  example-free₆ : f ∉ (λ[ f ∶ (𝔹 ⇒ 𝔹) ] λ[ x ∶ 𝔹 ] ` f · ` x)
 
@@ -2975,115 +2975,115 @@ then `Γ` must assign a type to `x`.
 
 
 
-freeLemmafree-lemma : ∀ {x M A Γ} → x ∈ M → Γ ⊢ M ∶ A → ∃ λ B M→ AΓ Γ} → x ∈≡ just M → Γ ⊢ M ∶ A → ∃ λ B → Γ x ≡ just B
 
@@ -3119,364 +3119,393 @@ _Proof_: We show, by induction on the proof that `x` appears
 
 
 
-freeLemmafree-lemma free-` (Ax Γx≡A) = (_ , Γx≡A)
+free-lemma (Ax Γx≡A) =free-·₁ x∈L(_ , Γx≡A) (⇒-E ⊢L ⊢M) = free-lemma x∈L ⊢L
 freeLemmafree-lemma (free-·₁ x∈L) (⇒-E ⊢L ⊢M(free-·₂ x∈M) = freeLemma x∈L(⇒-E ⊢L ⊢M) = free-lemma x∈M ⊢M
 freeLemma (free-·₂ x∈M) (⇒-E ⊢L ⊢M)free-lemma =(free-if₁ freeLemmax∈L) x∈M(𝔹-E ⊢L ⊢M ⊢N) = free-lemma x∈L ⊢L
 freeLemma (free-if₁ x∈L) (𝔹-E ⊢L ⊢M ⊢N) =free-lemma freeLemma(free-if₂ x∈L ⊢L
-freeLemma (free-if₂ x∈M) (𝔹-E ⊢L ⊢M ⊢N) = free-lemma x∈M ⊢L⊢M ⊢M ⊢N) = freeLemma x∈M ⊢M
 freeLemmafree-lemma (free-if₃ x∈N) (𝔹-E ⊢L ⊢M ⊢N) = freeLemmafree-lemma x∈N ⊢N
 freeLemmafree-lemma (free-λ {x} {y} y≢x x∈N) (⇒-I ⊢N) with y≢xfree-lemma x∈N) (⇒-I ⊢N)
+... | Γx≡C with freeLemmay x∈N≟ ⊢Nx
 | Γx≡Cyes withy≡x = y⊥-elim ≟ x
-... |(y≢x yes y≡x = ⊥-elim (y≢x y≡x)
 ... | no  _   = Γx≡C
 
@@ -3584,68 +3584,68 @@ typed in the empty context is closed (has no free variables).
 
 
 
-postulate
   ∅⊢-closed : ∀ {M A} → ∅ ⊢ M ∶ A :→ ∀ {M A} → ∅ ⊢ M ∶ A → closed M
 
@@ -3654,294 +3654,294 @@ typed in the empty context is closed (has no free variables).