add(Modal/Kripke): Remove IsRootedBy and add F.Root (#783)

Author: SnO2WMaN

Foundation.lean

@@ -294,7 +294,6 @@ public import Foundation.Modal.Kripke.LinearFrame
 public import Foundation.Modal.Kripke.Logic.GL.Completeness
 public import Foundation.Modal.Kripke.Logic.GL.MDP
 public import Foundation.Modal.Kripke.Logic.GL.Soundness
-public import Foundation.Modal.Kripke.Logic.GL.Tree
 public import Foundation.Modal.Kripke.Logic.GL.Unnecessitation
 public import Foundation.Modal.Kripke.Logic.GLPoint3
 public import Foundation.Modal.Kripke.Logic.Grz.Completeness
@@ -340,7 +339,7 @@ public import Foundation.Modal.Kripke.Logic.Ver
 public import Foundation.Modal.Kripke.NNFormula
 public import Foundation.Modal.Kripke.Preservation
 public import Foundation.Modal.Kripke.Rank
-public import Foundation.Modal.Kripke.Rooted
+public import Foundation.Modal.Kripke.Root
 public import Foundation.Modal.Kripke.Terminated
 public import Foundation.Modal.Kripke.Tree
 public import Foundation.Modal.Kripke.Undefinability

Foundation/Modal/Boxdot/GL_S.lean

@@ -6,6 +6,17 @@ public import Foundation.ProvabilityLogic.S.Completeness
 
 namespace LO
 
+namespace Modal.Kripke.Model
+
+variable {M : Kripke.Model} {x : M.World}
+
+instance [M.IsTransitive] : (M↾x).IsTransitive := inferInstance
+
+instance [M.IsTransitive] [M.IsPointRooted] : (M.extendRoot n).IsTransitive := inferInstance
+
+end Modal.Kripke.Model
+
+
 namespace Modal.Logic
 
 open Kripke Formula.Kripke
@@ -19,21 +30,19 @@ lemma iff_provable_boxdot_GL_provable_boxdot_S : Modal.GL ⊢ φᵇ ↔ Modal.S
   . apply Entailment.WeakerThan.wk;
     infer_instance;
   . intro h;
-    apply GL.Kripke.fintype_completeness_TFAE.out 2 0 |>.mp;
-    replace h := GL.Kripke.finite_completeness_TFAE.out 0 3 |>.mp $ iff_provable_rflSubformula_GL_provable_S.mpr h;
+    replace h := GL.Kripke.finite_completeness_TFAE.out 0 2 |>.mp $ iff_provable_rflSubformula_GL_provable_S.mpr h;
 
-    intro M _ _ _ r _;
-
-    obtain ⟨i, hi⟩ := Kripke.Model.extendRoot.inr_satisfies_axiomT_set (M := M) (Γ := □⁻¹'φᵇ.subformulas);
-    apply Model.extendRoot.inl_satisfies_boxdot_iff (n := ⟨(□⁻¹'φᵇ.subformulas).card + 1, by omega⟩) (i := i) |>.mpr;
+    apply GL.Kripke.fintype_completeness_TFAE.out 2 0 |>.mp;
+    intro M _ _ _ _;
 
-    let M₁ := M.extendRoot ⟨(□⁻¹'φᵇ.subformulas).card + 1, by omega⟩;
-    let i₁ : M₁.World := Sum.inl i;
-    apply Model.pointGenerate.modal_equivalent_at_root (r := i₁) |>.mp $ h (M₁↾i₁) _;
+    obtain ⟨i, hi⟩ := Kripke.Model.extendRoot.inr_satisfies_forall_axiomT_set (M := M) (Γ := □⁻¹'φᵇ.subformulas);
+    apply Model.extendRoot.inl_satisfies_boxdot_iff (i := i) |>.mp;
+    apply h;
     apply Satisfies.fconj_def.mpr;
-    intro ψ hψ;
-    apply Satisfies.fconj_def.mp hi;
-    grind;
+    simp only [Formula.rflSubformula, Finset.mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂];
+    rintro ψ hψ;
+    apply hi;
+    exact hψ;
 
 end Modal.Logic
 

Foundation/Modal/Kripke/AxiomH.lean

@@ -1,6 +1,6 @@
 module
 
-public import Foundation.Modal.Kripke.Rooted
+public import Foundation.Modal.Kripke.Root
 
 @[expose] public section
 

Foundation/Modal/Kripke/Cluster.lean

@@ -1,6 +1,6 @@
 module
 
-public import Foundation.Modal.Kripke.Rooted
+public import Foundation.Modal.Kripke.Root
 public import Mathlib.Data.Finite.Card