restructure and new strong norm

Author: amarmaduke

LeanSysF.lean

@@ -1,3 +1,4 @@
 -- This module serves as the root of the `LeanSysf` library.
 -- Import modules here that should be built as part of the library.
 import LeanSysF.OneSortHomArityGen
+import LeanSysF.TwoSortHet

LeanSysF/OneSortHomArityGen.lean

@@ -1,12 +1,13 @@
 
 import OneSortHomArityGen.FreeVar
--- import OneSortHomArityGen.Infer
+import OneSortHomArityGen.Infer
 import OneSortHomArityGen.Kinding
 import OneSortHomArityGen.Preservation
 import OneSortHomArityGen.Progress
 import OneSortHomArityGen.Reduction
 import OneSortHomArityGen.SN
-import OneSortHomArityGen.StrongNormalization
+import OneSortHomArityGen.StrongNorm1
+import OneSortHomArityGen.StrongNorm2
 import OneSortHomArityGen.Term
 import OneSortHomArityGen.Typing
 import OneSortHomArityGen.Utility

LeanSysF/TwoSortHet.lean

@@ -0,0 +1,2 @@
+import TwoSortHet.Ty
+import TwoSortHet.Term

OneSortHomArityGen/FreeVar.lean

@@ -3,6 +3,8 @@ import LeanSubst
 import OneSortHomArityGen.Utility
 import OneSortHomArityGen.Term
 
+namespace OneSortHomArityGen
+
 open LeanSubst
 
 inductive FV : Term -> Nat -> Prop
@@ -104,3 +106,5 @@ theorem FV.zero_not_in_succ {t : Term} : ¬ (0 ∈ t[+1]) := by
   intro j
   have lem := @var_not_in_one_more 0 t; simp at lem
   apply lem j
+
+end OneSortHomArityGen

OneSortHomArityGen/Infer.lean

@@ -1,6 +1,8 @@
 import LeanSubst
 import OneSortHomArityGen.Typing
 
+namespace OneSortHomArityGen
+
 open LeanSubst
 
 def Term.beq : Term -> Term -> Bool
@@ -118,7 +120,7 @@ def infer (Γ : Ctx Term) : Term -> Option Term
   let a := ts 1
   let F <- infer Γ f
   let P <- F.is_all
-  if a.is_type Γ then P[su a::+0]
+  if a.is_type Γ then return P[su a::+0]
   else none
 | .bind .lam ts t => do
   let A := ts 0
@@ -210,3 +212,5 @@ def ex2 : Term := ex1 :@[ex0] :@ ex1
 
 #eval infer Ctx.nil ex1
 #eval infer Ctx.nil ex2
+
+end OneSortHomArityGen

OneSortHomArityGen/Kinding.lean

@@ -3,6 +3,8 @@ import LeanSubst
 import OneSortHomArityGen.Term
 import OneSortHomArityGen.FreeVar
 
+namespace OneSortHomArityGen
+
 open LeanSubst
 
 inductive Kinding : Ctx Term -> Term -> Prop where
@@ -182,3 +184,8 @@ theorem Kinding.injection_arrow : Γ ⊢ (A -:> B) type -> Γ ⊢ A type ∧ Γ
     rw [Vec.inv2] at e
     rcases e with ⟨e1, e2⟩; simp at e1 e2; subst e1 e2
     simp [*]
+
+theorem Kinding.type_not_star : Γ ⊢ A type -> A ≠ ★ := by
+  intro j h; subst h; cases j
+
+end OneSortHomArityGen

OneSortHomArityGen/Model.lean

@@ -0,0 +1,86 @@
+
+import LeanSubst
+import OneSortHomArityGen.Term
+
+namespace OneSortHomArityGen
+
+open LeanSubst
+
+universe u u1 u2 u3
+
+class Model (D : Sort u) where
+  A : D -> D -> D
+  Q : (D -> D) -> D
+  P : D -- Any model has to know what to do with junk
+
+@[simp]
+def Model.int_term [Model D] (v : Nat -> D) : Term -> D
+| #x => v x
+| .ctor .arr ts => A (int_term v (ts 0)) (int_term v (ts 1))
+| .bind .all _ t => Q (λ d => int_term (d::v) t)
+| _ => P
+
+@[simp]
+def Model.int_subst [Model D] (v : Nat -> D) (σ : Subst Term) : Nat -> D
+| i => Model.int_term v (σ i)
+
+notation "⟦ " t " ⟧ " v:100 => Model.int_term v t
+notation "⟦ " σ " ⟧ " v:100 => Model.int_subst v σ
+
+theorem Model.rename [Model D] {A : Term} {ξ : Nat -> D} (r : Ren)
+  : ⟦ A[r] ⟧ ξ = ⟦ A ⟧ (ξ ∘ r)
+:= by
+  induction A generalizing r ξ <;> simp at *
+  case ctor v _ ih =>
+    cases v <;> simp at *; case _ ts =>
+    generalize Adef : ts 0 = A at *
+    generalize Bdef : ts 1 = B at *
+    rcases ih with ⟨ih1, ih2⟩; congr 1
+    rw [ih1]; rw [ih2]
+  case bind v _ _ ih1 ih2 =>
+    cases v <;> simp at *
+    congr; funext; case _ d =>
+    replace ih2 := @ih2 (d::ξ) r.lift
+    rw [Ren.to_lift (S := Term)] at ih2
+    simp at ih2; rw [ih2]; congr
+    funext; case _ i =>
+    cases i <;> simp [Ren.lift]
+
+@[simp]
+theorem Model.weaken [Model D] {A : Term} {ξ : Nat -> D}
+  : ⟦ A[+1] ⟧ (d::ξ) = ⟦ A ⟧ ξ
+:= by
+  have lem := Model.rename (A := A) (ξ := d::ξ) (· + 1)
+  simp at lem; rw [lem]
+  have lem : ((d::ξ) ∘ (· + 1)) = ξ := by
+    funext; case _ i =>
+    cases i <;> simp
+  rw [lem]
+
+theorem Model.subst [Model D] {A : Term} {σ : Subst Term} {ξ : Nat -> D}
+  : ⟦ A[σ] ⟧ ξ = ⟦ A ⟧ (⟦ σ ⟧ ξ)
+:= by
+  induction A generalizing σ ξ <;> simp
+  case ctor v _ ih =>
+    cases v <;> simp
+    simp [*]
+  case bind v _ _ ih1 ih2 =>
+    cases v <;> simp
+    congr; funext; case _ d =>
+    replace ih2 := @ih2 σ.lift (d::ξ)
+    simp at ih2; rw [ih2]; congr
+    funext; case _ i =>
+    cases i <;> simp [Subst.compose]
+    case _ i =>
+    generalize σ i = z
+    cases z <;> simp
+
+@[simp]
+theorem Model.beta [Model D] {A B : Term} {ξ : Nat -> D}
+  : ⟦ A[su B::+0] ⟧ ξ = ⟦ A ⟧ (⟦ B ⟧ ξ :: ξ)
+:= by
+  rw [Model.subst]; congr
+  funext; case _ i =>
+  cases i <;> simp
+
+end OneSortHomArityGen

OneSortHomArityGen/Preservation.lean

@@ -5,6 +5,8 @@ import OneSortHomArityGen.Typing
 import OneSortHomArityGen.Reduction
 import OneSortHomArityGen.Progress
 
+namespace OneSortHomArityGen
+
 open LeanSubst
 
 theorem preservation_step : Γ ⊢ t : A -> t ~> t' -> Γ ⊢ t' : A := by
@@ -82,3 +84,5 @@ theorem preservation : Γ ⊢ t : A -> t ~>* t' -> Γ ⊢ t' : A := by
   case _ => exact j
   case _ y z r1 r2 ih =>
     apply preservation_step ih r2
+
+end OneSortHomArityGen

OneSortHomArityGen/Progress.lean

@@ -4,6 +4,8 @@ import OneSortHomArityGen.Kinding
 import OneSortHomArityGen.Typing
 import OneSortHomArityGen.Reduction
 
+namespace OneSortHomArityGen
+
 open LeanSubst
 
 @[simp]
@@ -250,3 +252,5 @@ theorem progress t : Value t ∨ (∃ t', t ~> t') := by
         apply Or.inr
         exists (:∀ t')
         apply Red.bind2 _ r
+
+end OneSortHomArityGen

OneSortHomArityGen/Reduction.lean

@@ -3,6 +3,8 @@ import LeanSubst
 import LeanSubst.Reduction
 import OneSortHomArityGen.Term
 
+namespace OneSortHomArityGen
+
 open LeanSubst
 
 inductive Red : Term -> Term -> Prop where
@@ -39,7 +41,7 @@ theorem Red.antirename {s t : Term} (r : Ren) :
   ∃ z, s ~> z ∧ t = z[r]
 := by
   intro h
-  generalize wdef : s[r:Term] = w at *
+  generalize wdef : s[r] = w at *
   induction h generalizing s r
   case beta A b t =>
     cases s <;> simp at wdef
@@ -114,7 +116,6 @@ theorem Red.antirename {s t : Term} (r : Ren) :
     rcases ih with ⟨z, h1, h2⟩
     exists (Term.bind v' ts' z); apply And.intro
     apply Red.bind2 _ h1; subst h2; simp
-    rw [Ren.to_lift (S := Term)]; simp
 
 theorem Red.ctor_star_lemma {ts ts'} i :
   (∀ j ≠ i, ts j = ts' j) ->
@@ -599,3 +600,5 @@ instance : Substitutive Red where
 --   instance : HasConfluence Red where
 --     confluence := confluence
 -- end Red
+
+end OneSortHomArityGen