Define Model.toTail as RootedModel and fill its sorries

- Change toTail return type from Model to RootedModel (κ ⊕ ℕ∞) α, folding
  the root (.inr ⊤) into the structure; fix r : M.World (was broken M.root)
- root field: .inr ⊤ relates to every other world via lt_top_iff_ne_top
- IsTrans / Std.Irrefl instances for the tail relation
- toTail.tail_isChain via exact_mod_cast

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

Author: SnO2WMaN

SeqPL/Kripke/Tail.lean

@@ -1,7 +1,7 @@
 module
 
 public import SeqPL.Kripke.RootExtension
-public import Mathlib
+public import Mathlib.Data.ENat.Basic
 
 @[expose]
 public section
@@ -10,7 +10,7 @@ variable [Nonempty κ] {M : Model κ α} {n : ℕ+} {A B : Formula α} {Γ Γ' 
 
 namespace Model
 
-abbrev toTail (M : Model κ α) (r : M.root) : Model (κ ⊕ ℕ∞) α where
+abbrev toTail (M : Model κ α) (r : M.World) : RootedModel (κ ⊕ ℕ∞) α where
   Rel' x y :=
     match x, y with
     | .inl x, .inl y => M.Rel x y
@@ -21,19 +21,18 @@ abbrev toTail (M : Model κ α) (r : M.root) : Model (κ ⊕ ℕ∞) α where
     match x with
     | .inl x => M.Val x a
     | .inr _ => M.Val r a
+  root := ⟨.inr ⊤, by
+    intro x hx;
+    match x with
+    | .inl x => simp [Model.Rel];
+    | .inr i =>
+      simp only [Model.Rel];
+      exact lt_top_iff_ne_top.mpr (by simpa using hx);
+  ⟩
 
 namespace toTail
 
-variable {r : M.root}
-
-protected abbrev root (M : Model κ α) (r : M.root) : (M.toTail r).root := ⟨.inr ⊤, by
-  intro x hx;
-  match x with
-  | .inl x => simp_all [toTail, Model.Rel]
-  | .inr i => simp_all [Model.Rel]; grind;
-⟩
-
-instance : Nonempty (M.toTail r).root := ⟨toTail.root M r⟩
+variable {r : M.World}
 
 instance [IsTrans _ M.Rel] : IsTrans _ (M.toTail r).Rel := by
   constructor;
@@ -42,8 +41,9 @@ instance [IsTrans _ M.Rel] : IsTrans _ (M.toTail r).Rel := by
   | .inl x, .inl y, .inl z =>
     simp_all only [Model.Rel];
     exact IsTrans.trans _ _ _ Rxy Ryz;
-  | .inr _, .inr _, .inr _ =>
-    grind;
+  | .inr a, .inr b, .inr c =>
+    simp_all only [Model.Rel];
+    exact lt_trans Ryz Rxy;
   | _, .inl _, .inr _
   | .inl _, .inr _, _
   | .inr _, _, .inl _ =>
@@ -56,11 +56,12 @@ instance [Std.Irrefl M.Rel] : Std.Irrefl (M.toTail r).Rel := by
   | .inl x => simp_all only [Model.Rel]; apply Std.Irrefl.irrefl
   | .inr i => simp [Model.Rel];
 
-protected abbrev tail (M : Model κ α) (r : M.root) : ℕ+ → (M.toTail r).World := λ n => .inr n
+protected abbrev tail (M : Model κ α) (r : M.World) : ℕ+ → (M.toTail r).World := λ n => .inr (n : ℕ∞)
 
 @[simp]
 lemma tail_isChain (h : i < j) : ((toTail.tail M r) j ≺ (toTail.tail M r) i) := by
-  simp [Model.Rel]; grind;
+  simp only [Model.Rel];
+  exact_mod_cast h;
 
 end toTail