update leansubst

Author: amarmaduke

LeanStlc/Infer.lean

@@ -1,4 +1,5 @@
 
+import Std.Tactic.Do
 import LeanStlc.Typing
 
 namespace Ty

LeanStlc/SNi.lean

@@ -333,7 +333,7 @@ namespace SNi
           intro i y h
           cases i <;> simp at *
           case zero => exact h
-          case _ z => apply Or.inl; exact h
+          case _ z => exact h
         rw [lem] at j2
         apply SNi.lam
         apply @antirename .nor (b[r]) r j2

LeanStlc/Term.lean

@@ -135,13 +135,13 @@ theorem ren_subst_apply_eq_lift {r : Ren} {σ : Subst Term} :
       simp [Subst.compose]
       generalize zdef : σ i = z at *
       cases z <;> simp at *
-      case _ y => subst h; apply Or.inl; exact h2
+      case _ y => subst h; exact h2
       case _ t => subst h; simp; exact h2
     case _ h =>
       simp [Subst.compose]
       generalize zdef : σ i = z at *
       cases z <;> simp at *
-      case _ y => subst h; apply Or.inl; exact h2
+      case _ y => subst h; exact h2
 
 theorem ren_subst_apply_eq {t : Term} {r : Ren} {σ : Subst Term} :
   (∀ i x, r i = x -> σ i = #x ∨ σ i = .re x) ->

LeanStlc/WeakNorm.lean

@@ -82,7 +82,7 @@ namespace WeakNormalization
       apply lem
 end WeakNormalization
 
-theorem weak_termination {t A} : [] ⊢ t : A -> ∃ v, t ~>* v ∧ WeakValue v := by
+theorem weak_termination {t A} : .nil ⊢ t : A -> ∃ v, t ~>* v ∧ WeakValue v := by
   intro j
   have lem := WeakNormalization.fundamental j
   simp at lem
@@ -92,12 +92,12 @@ theorem weak_termination {t A} : [] ⊢ t : A -> ∃ v, t ~>* v ∧ WeakValue v
   exists v
   apply And.intro lem.1 weak
 
-theorem consistency_lemma {t} : [] ⊢ t : ⊤ -> WeakValue t -> False := by
+theorem consistency_lemma {t} : .nil ⊢ t : ⊤ -> WeakValue t -> False := by
   intro h1 h2
   cases t <;> simp [WeakValue] at *
   case lam A b => cases h1
 
-theorem consistency {t} : ¬ ([] ⊢ t : ⊤) := by
+theorem consistency {t} : ¬ (.nil ⊢ t : ⊤) := by
   intro h
   have lem := weak_termination h
   cases lem; case _ v lem =>

Main.lean

@@ -6,8 +6,8 @@ def tt (A : Ty) : Term := :λ[A] :λ[A] #1
 def ff (A : Ty) : Term := :λ[A] :λ[A] #0
 def not (A : Ty) : Term := :λ[bool_ty (bool_ty A)] #0 :@ (ff A) :@ (tt A)
 
-#eval Option.get! (infer [] (tt ⊤))
-#eval Option.get! (infer [] (not ⊤))
-#eval Option.get! (infer [] ((not ⊤) :@ (tt (bool_ty ⊤))))
+#eval Option.get! (infer .nil (tt ⊤))
+#eval Option.get! (infer .nil (not ⊤))
+#eval Option.get! (infer .nil ((not ⊤) :@ (tt (bool_ty ⊤))))
 
 def main : IO Unit := do return ()

docbuild/lake-manifest.json

@@ -62,7 +62,7 @@
    "type": "git",
    "subDir": null,
    "scope": "amarmaduke",
-   "rev": "987039ce9c6e92b6a1b4e7a0ddcfbc9678eb48a5",
+   "rev": "8da67cb68dd63ef181e521996f58992c7d9e7008",
    "name": "«lean-subst»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "amarmaduke",
-   "rev": "987039ce9c6e92b6a1b4e7a0ddcfbc9678eb48a5",
+   "rev": "8da67cb68dd63ef181e521996f58992c7d9e7008",
    "name": "«lean-subst»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",