diff --git a/out/StlcProp.md b/out/StlcProp.md index d98d62e2..9191fb82 100644 --- a/out/StlcProp.md +++ b/out/StlcProp.md @@ -4548,141 +4548,113 @@ _Proof_: By induction on the derivation of `Γ ⊢ M ∶ A`. >) + (context-lemma (Γ~Γ′ ∘ free-·₂) ⊢M) context-lemma Γ~Γ′ 𝔹-I₁ = 𝔹-I₁ context-lemma Γ~Γ′ 𝔹-I₂ = 𝔹-I₂ -context-lemma Γ~Γ′ (𝔹-E ⊢L ⊢M𝔹-I₂ ⊢N) - = 𝔹-E (𝔹-I₂ +context-lemma (Γ~Γ′ (𝔹-E ∘⊢L free-if₁⊢M ⊢N) = ⊢L)𝔹-E (Γ~Γ′ ∘ free-if₂free-if₁) ⊢M⊢L) + (context-lemma (Γ~Γ′ ∘ free-if₃free-if₂) ⊢M) + (context-lemma (Γ~Γ′ ∘ free-if₃) ⊢N) @@ -4762,162 +4764,162 @@ _Lemma_: If `Γ , x ∶ A ⊢ N ∶ B` and `∅ ⊢ V ∶ A`, then 
 
-preservation-[:=] : ∀ {Γ x A N B V}
-                 → (Γ , x ∶ A) ⊢ N ∶ B
-                 → ∅ ⊢ V ∶ A
-                 → Γ ⊢ (N [ x := V: ])∀ ∶{Γ x A N B V}
+                 → (Γ , x ∶ A) ⊢ N ∶ B
+                 → ∅ ⊢ V ∶ A
+                 → Γ ⊢ (N [ x := V ]) ∶ B
 
@@ -4991,425 +4993,425 @@ we show that if `∅ ⊢ V ∶ A` then `Γ ⊢ N [ x := V ] ∶ B`.
 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 = context-lemma Γ~Γ′ ⊢V
-  where
-  Γ~Γ′ : ∀ {x} → x ∈ V → ∅ x ≡A Γ} x
-  Γ~Γ′→ ∅ ⊢ V {x}∶ A x∈V→ Γ =⊢ ⊥-elimV (x∉V∶ x∈V)A
-    where
-    x∉Vweaken-closed {V} {A} {Γ} ⊢V := ¬context-lemma (xΓ~Γ′ ∈ V)
-    x∉V = ∅⊢-closed ⊢V {x}
-
-just-injectivewhere
+  Γ~Γ′ : ∀ {x} → x ∈ V :→ ∀∅ {X : Set} {x y≡ Γ x
+  Γ~Γ′ : X} → _≡_ {Ax} x∈V = Maybe⊥-elim (x∉V X} x∈V(just x) (just y) →
+    where
+    x∉V x: ≡¬ (x ∈ 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
 
@@ -5417,937 +5419,937 @@ We need a couple of lemmas. A closed term can be weakened to any context, and `j
 
 
 
-preservation-[:=] {Γ} {x} {A} (Ax {Γ,x∶A} {x′} {B} [Γ,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} [Γ,x∶A]x′≡B) ⊢V with x ≟ x′
 preservation-[:=]...| {Γ}yes {x} {A}x≡x′ {λ[rewrite x′ ∶ A′ ] N′} {.A′just-injective ⇒ B′} {V} (⇒-I[Γ,x∶A]x′≡B  = ⊢N′) ⊢V with x  weaken-closed ≟ x′⊢V
 ...| yes x≡x′ rewrite x≡x′ no  x≢x′  =  Ax context-lemma[Γ,x∶A]x′≡B
+preservation-[:=] Γ′~Γ (⇒-I{Γ} ⊢N′)
-  where
-  Γ′~Γ{x} {A} {λ[ x′ ∶ A′ :] ∀ N′{y} →{.A′ y⇒ ∈B′} (λ[ x′{V} ∶ A′(⇒-I ] N′⊢N′) →⊢V (Γ ,with x ≟ x′ ∶ A) y ≡
+...| Γ y
-  Γ′~Γ {y} (free-λ x′≢y y∈N′) with x′ ≟ y
-  ...| yes x′≡y  x≡x′ rewrite x≡x′ = ⊥-elimcontext-lemma Γ′~Γ (⇒-I ⊢N′)
+  where
+  Γ′~Γ : ∀ (x′≢y{y} → x′≡yy ∈ )
-  ...|(λ[ x′ ∶ noA′  _     = refl
-...|] no  x≢x′N′) =→ ⇒-I ⊢N′V
-  where
-  x′x⊢N′ : (Γ , x′ ∶ A) y ≡ Γ y
+  Γ′~Γ {y} (free-λ x′≢y y∈N′) with x′ A′≟ , x ∶ Ay
+  ...| ⊢yes N′x′≡y  = ∶ B′
-  x′x⊢N′⊥-elim rewrite(x′≢y update-permute Γ x A x′ A′ x≢x′ = ⊢N′x′≡y)
   ...| no  _     = refl
+...| no  x≢x′ = ⇒-I ⊢N′V : (Γ , x′ ∶ A′)
+  where ⊢ N′ [ x
+  x′x⊢N′ :=: VΓ ], ∶x′ ∶ A′ , x ∶ A ⊢ N′ ∶ B′
   ⊢N′V = preservation-[:=] x′x⊢N′ ⊢Vrewrite
-preservation-[:=] (⇒-Eupdate-permute ⊢LΓ ⊢M)x ⊢VA x′ A′ x≢x′ = ⇒-E⊢N′
+  ⊢N′V : (preservation-[:=]Γ ⊢L, x′ ∶ A′) ⊢V)⊢ (preservation-[:=]N′ ⊢M[ ⊢V)x := V ] ∶ B′
-⊢N′V = preservation-[:=] 𝔹-I₁x′x⊢N′ ⊢V = 𝔹-I₁
 preservation-[:=] (⇒-E 𝔹-I₂⊢L ⊢M) ⊢V = 𝔹-I₂
-preservation-[:=]= ⇒-E (𝔹-Epreservation-[:=] ⊢L ⊢L ⊢M ⊢N) ⊢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)
 
@@ -6363,95 +6365,95 @@ reduction preserves types.
 
 
 
-preservation : ∀ {M N A} → ∅ ⊢ M ∶ A → M ⟹ N → ∅ ⊢ N ∶ A
 
@@ -6489,435 +6491,435 @@ _Proof_: By induction on the derivation of `∅ ⊢ M ∶ A`.
 
 
 
-preservation (Ax Γx≡A) ()
-preservation (⇒-I ⊢N) ()
-preservation (⇒-E (⇒-I ⊢N) ⊢V) (βλ· valueV) = preservation-[:=] ⊢N ⊢V
-preservation (⇒-E ⊢L ⊢M) (ξ·₁ L⟹L′) with preservation ⊢L L⟹L′()
 preservation (⇒-I ⊢N) ()
+preservation ...|(⇒-E ⊢L′(⇒-I ⊢N) ⊢V) (βλ· valueV) = ⇒-Epreservation-[:=] ⊢L′⊢N ⊢M⊢V
 preservation (⇒-E ⊢L ⊢M) (ξ·₂ valueL M⟹M′) with preservation ⊢M M⟹M′
-...| ⊢M′ = ⇒-E ⊢L ⊢M′
-preservation 𝔹-I₁ ()
-preservation 𝔹-I₂ ()
-preservation (𝔹-E⇒-E 𝔹-I₁⊢L ⊢M) (ξ·₁ L⟹L′) with preservation ⊢L L⟹L′
+...| ⊢L′ = ⇒-E ⊢L′ ⊢M
+preservation (⇒-E ⊢L ⊢M) (ξ·₂ valueL ⊢M ⊢NM⟹M′) βif-truewith =preservation ⊢M M⟹M′
 preservation...| (𝔹-E⊢M′ 𝔹-I₂= ⊢M⇒-E ⊢N)⊢L βif-false = ⊢N⊢M′
 preservation 𝔹-I₁ ()
+preservation 𝔹-I₂ ()
+preservation (𝔹-E ⊢L𝔹-I₁ ⊢M ⊢N) (ξif L⟹L′) with preservation ⊢L L⟹L′βif-true = ⊢M
 ...| ⊢L′ = 𝔹-E ⊢L′ ⊢Mpreservation (𝔹-E 𝔹-I₂ ⊢M ⊢N) βif-false = ⊢N
+preservation (𝔹-E ⊢L ⊢M ⊢N) (ξif L⟹L′) with preservation ⊢L L⟹L′
+...| ⊢L′ = 𝔹-E ⊢L′ ⊢M ⊢N
 
@@ -6941,207 +6943,49 @@ term can _never_ reach a stuck state.
 
 
 
-Normal : Term → Set
-Normal M = ∀ {N} → ¬ (M ⟹ N)
-
-Stuck : Term → Set
-Stuck M = Normal M × ¬ Value M
-
-postulate
-  Soundness : ∀ {M N A}→ → ∅Set
+Normal ⊢ M ∶= A∀ → M ⟹* {N}  (StuckM ⟹ N)
+
+Stuck : Term → Set
+Stuck M = Normal M × ¬ Value M
+
+postulate
+  Soundness : ∀ {M N A} → ∅ ⊢ M ∶ A → M ⟹* N → ¬ (Stuck N)
 
@@ -7169,342 +7171,342 @@ term can _never_ reach a stuck state.