two separate IHs in tableautheNotSat + foldr boxes

Pdl/LoadSplit.lean

@@ -90,7 +90,6 @@ theorem loadMulti_nonEmpty_eq_loadMulti :
   case cons IH =>
     simp
     rw [IH]
-    simp
 
 theorem LoadFormula.split_eq_loadMulti (lf : LoadFormula) {δ α φ}
     (h : lf.split = (δ ++ [α], φ)) : lf = loadMulti δ α φ := by

Pdl/Modelgraphs.lean

@@ -75,12 +75,12 @@ theorem loadClaimHelper {Worlds : Finset (Finset Formula)}
     apply IHδ (δ.get (i.cast help1)) (by apply List.get_mem) (List.get (X :: l ++ [Y]) i.castSucc)
     · have : (⌈List.get δ (i.cast help1)⌉⌈⌈List.drop (i + 1) δ⌉⌉φ) = (⌈⌈List.drop (i.castSucc) δ⌉⌉φ) := by
         simp only [List.append_eq, Fin.coe_castSucc]
-        rw [← Formula.boxes]
         have := @List.drop_eq_get_cons _ i δ (by rw [← length_def]; have := Fin.is_lt i; convert this; simp)
         rw [this]
         cases i
         simp_all only [instBot, insTop, List.zip_cons_cons, Subtype.forall, List.append_eq,
-          Fin.castSucc_mk, boxes, Fin.cast_mk]
+          Fin.castSucc_mk, Fin.cast_mk]
+        rw [Formula.boxes_cons]
       rw [this]
       exact IH
     · simp [relate]

Pdl/Semantics.lean

@@ -283,7 +283,7 @@ theorem evalBoxes (δ : List Program) φ :
   induction δ generalizing w
   · simp [relateSeq]
   case cons α δ IH =>
-    simp only [Formula.boxes, evaluate]
+    simp only [evaluate, boxes_first]
     constructor
     · intro lhs
       intro v v_αδ_w

Pdl/Soundness.lean

@@ -778,45 +778,47 @@ theorem tableauThenNotSat (tab : Tableau .nil Root) (t : PathIn tab) :
     ·
       clear not_free
       rcases nlf with ⟨lf⟩
-      -- Now we take apart the loaded formula to get all loaded boxes from the front at once,
-      -- so that we know how many `loadedDiamondPaths` applications we need below.
+      -- Now we take apart the loaded formula to get all loaded boxes from the front at once ...
       rcases LoadFormula.exists_loadMulti lf with ⟨δ, α, φ, lf_def⟩
-
       -- Now assume for contradiction, that Λ(t) is satisfiable.
       rintro ⟨W,M,v,v_⟩
-
       have := v_ (~ unload (loadMulti δ α φ)) (by simp; right; aesop)
       rw [unload_loadMulti] at this
-      induction δ generalizing lf -- α -- amazing that this does not give a wrong motive ;-)
+      -- ... so that we can do induction on δ for multiple `loadedDiamondPaths` applications.
+      induction δ generalizing lf v t -- α -- amazing that this does not give a wrong motive ;-)
       · simp [evalBoxes] at this
         rcases this with ⟨w, v_α_w, not_w_φ⟩
         simp only [loadMulti, List.foldr_nil] at *
-        have in_t : NegLoadFormula_in_TNode (~'⌊α⌋AnyFormula.normal φ) (nodeAt t) := by
+        have in_t : NegLoadFormula_in_TNode (~'⌊α⌋φ) (nodeAt t) := by
           simp_all [nodeAt, NegLoadFormula_in_TNode]; aesop
         have := loadedDiamondPaths α tab t v_ φ in_t v_α_w (not_w_φ)
-
-        · rcases this with ⟨s, t_cc_s, (notequi | not_af_in_s), w_s, rest_s_free⟩
-          · -- left the cluster, cannot be the case by Lemma and IH:
-            have := eProp2.f t s t_cc_s (by rw [cEquiv.symm]; exact notequi)
-            absurd IH _ this
-            use W, M, w
-          ·
-            -- this should now be a relatively easy contradiction!
-            -- or not ;-) (it is not about ~φ and φ at w ...)
-            absurd IH s ?_
-            use W, M, w
-            · -- Remains to show that s is simpler than t.
-              -- Follows because s is free, which we get from `loadedDiamondPaths`.
-              simp only [TNode.without_normal_isFree_iff_isFree] at rest_s_free
-              apply eProp2.d_cc t s ?_ rest_s_free t_cc_s
-              · unfold TNode.isLoaded
-                cases in_t <;> aesop
-      case cons β δ IH =>
-        -- we need an unknown number of applications of `loadedDiamondPaths`
-        -- now the new `IH` here should solve this??
-        -- probably still need to make one step with the lemma for β
-        simp [evalBoxes, relateSeq] at this -- ???
-        sorry
+        rcases this with ⟨s, t_cc_s, s_property, w_s, rest_s_free⟩
+        -- We now claim that we have a contradiction with the IH because we left the cluster:
+        absurd IH s ?_
+        use W, M, w
+        -- Remains to show that s is simpler than t, using eProp2 for that.
+        rcases s_property with (notequi | not_af_in_s)
+        · exact eProp2.f t s t_cc_s (by rw [cEquiv.symm]; exact notequi)
+        · -- Follows because s is free, which we get from `loadedDiamondPaths`.
+          simp only [TNode.without_normal_isFree_iff_isFree] at rest_s_free
+          apply eProp2.d_cc t s ?_ rest_s_free t_cc_s
+          unfold TNode.isLoaded
+          cases in_t <;> aesop
+      case cons β δ IH_inner =>
+        -- We make one step with `loadedDiamondPaths` for β before we can apply IH.
+        rw [boxes_first] at this
+        simp at this
+        rcases this with ⟨w, v_β_w, not_w_δαφ⟩
+        have in_t : NegLoadFormula_in_TNode (~'⌊β⌋(⌊⌊δ⌋⌋⌊α⌋φ)) (nodeAt t) := by
+          simp_all [nodeAt, NegLoadFormula_in_TNode]
+          aesop
+        have := loadedDiamondPaths β tab t v_ (⌊⌊δ⌋⌋⌊α⌋φ) in_t v_β_w
+          (by simp [vDash,modelCanSemImplyAnyNegFormula]; exact not_w_δαφ)
+        -- this gets us a node `s` to which we apply the **inner or outer ???** IH
+        rcases this with ⟨s, t_cc_s, s_property, w_s, rest_s_free⟩
+        rcases s_property with (notequi | not_af_in_s)
+        · sorry
+        · sorry
 
 theorem correctness : ∀ LR : TNode, satisfiable LR → consistent LR := by
   intro LR

Pdl/Substitution.lean

@@ -91,7 +91,7 @@ theorem repl_in_boxes_non_occ_eq_neg (δ : List Program) :
   induction δ
   · simp
   case cons α δ IH =>
-    simp only [Formula.boxes, repl_in_F, Formula.box.injEq]
+    simp only [Formula.boxes, List.foldr_cons, repl_in_F, Formula.box.injEq]
     constructor
     · apply repl_in_P_non_occ_eq
       simp_all [voc, vocabOfProgram, Vocab.fromList]
@@ -105,7 +105,7 @@ theorem repl_in_boxes_non_occ_eq_pos (δ : List Program) :
   induction δ
   · simp
   case cons α δ IH =>
-    simp only [Formula.boxes, repl_in_F, Formula.box.injEq]
+    simp only [Formula.boxes, List.foldr_cons, repl_in_F, Formula.box.injEq]
     constructor
     · apply repl_in_P_non_occ_eq
       simp_all [voc, vocabOfProgram, Vocab.fromList]

Pdl/Syntax.lean

@@ -24,10 +24,8 @@ def Formula.or : Formula → Formula → Formula
   | f, g => Formula.neg (Formula.and (Formula.neg f) (Formula.neg g))
 
 /-- □(αs,φ) -/
-@[simp]
 def Formula.boxes : List Program → Formula → Formula
-  | [], f => f
-  | (p :: ps), f => Formula.box p (Formula.boxes ps f)
+| δ, χ => List.foldr (fun β φ => Formula.box β φ) χ δ
 
 @[simp]
 def Program.steps : List Program → Program
@@ -63,19 +61,19 @@ def isStar : Program → Bool
 | ∗_ => true
 | _ => false
 
-theorem boxes_last : (~⌈a⌉Formula.boxes (as ++ [c]) P) = (~⌈a⌉Formula.boxes as (⌈c⌉P)) :=
+@[simp]
+theorem Formula.boxes_nil : Formula.boxes [] φ = φ := by simp [Formula.boxes]
+
+@[simp]
+theorem Formula.boxes_cons : Formula.boxes (β :: δ) φ = Formula.box β (Formula.boxes δ φ) := by simp [Formula.boxes]
+
+theorem boxes_last : Formula.boxes (δ ++ [α]) φ = Formula.boxes δ (⌈α⌉φ) :=
   by
-  induction as
-  · simp
-  · simp at *
-    assumption
+  induction δ <;> simp [Formula.boxes]
 
 theorem boxes_append : Formula.boxes (as ++ bs) P = Formula.boxes as (Formula.boxes bs P) :=
   by
-  induction as
-  · simp
-  · simp at *
-    assumption
+  induction as <;> simp [Formula.boxes]
 
 /-! ## Loaded Formulas -/
 
@@ -99,14 +97,21 @@ instance : Coe LoadFormula AnyFormula := ⟨AnyFormula.loaded⟩
 inductive AnyNegFormula
 | neg : AnyFormula → AnyNegFormula
 
-@[simp]
 def loadMulti : List Program → Program → Formula → LoadFormula
-| bs, α, φ => List.foldr (fun f β => LoadFormula.box f β) (LoadFormula.box α φ) bs
+| bs, α, φ => List.foldr (fun β lf => LoadFormula.box β lf) (LoadFormula.box α φ) bs
 
 @[simp]
+theorem loadMulti_nil : loadMulti [] α φ = LoadFormula.box α φ := by simp [loadMulti]
+
+@[simp]
+theorem loadMulti_cons : loadMulti (β :: δ) α φ = LoadFormula.box β (loadMulti δ α φ) := by simp [loadMulti]
+
 def LoadFormula.boxes : List Program → LoadFormula → LoadFormula
-| [], χ => χ
-| (b::bs), χ => LoadFormula.box b (LoadFormula.boxes bs χ)
+| δ, χ => List.foldr (fun β lf => LoadFormula.box β lf) χ δ
+
+@[simp]
+theorem boxes_first : (Formula.boxes (α :: δ) φ) = ⌈α⌉(Formula.boxes δ φ) := by
+  simp [Formula.boxes, LoadFormula.boxes]
 
 @[simp]
 def unload : LoadFormula → Formula
@@ -116,11 +121,8 @@ def unload : LoadFormula → Formula
 @[simp]
 theorem unload_loadMulti : unload (loadMulti δ α φ) = ⌈⌈δ⌉⌉⌈α⌉φ := by
   induction δ
-  · simp
-  case cons IH =>
-    simp only [loadMulti, List.foldr_cons, unload, Formula.boxes, Formula.box.injEq, true_and]
-    rw [← IH]
-    simp
+  · simp [Formula.boxes, LoadFormula.boxes, loadMulti]
+  · simpa [Formula.boxes, LoadFormula.boxes, loadMulti]
 
 inductive NegLoadFormula : Type -- ¬χ
   | neg : LoadFormula → NegLoadFormula
@@ -144,20 +146,17 @@ example : NegLoadFormula := ~'(⌊⌊[·1, ·2]⌋⌋⌊·1⌋(⊤ : Formula))
 
 theorem loadBoxes_append : LoadFormula.boxes (as ++ bs) P = LoadFormula.boxes as (LoadFormula.boxes bs P) :=
   by
-  induction as
-  · simp
-  · simp at *
-    assumption
+  induction as <;> simp [LoadFormula.boxes]
 
 theorem loadBoxes_last : (~'⌊a⌋LoadFormula.boxes (as ++ [c]) P) = (~'⌊a⌋LoadFormula.boxes as (⌊c⌋P)) :=
   by
-  induction as <;> simp [loadBoxes_append]
+  induction as <;> simp [LoadFormula.boxes, loadBoxes_append]
 
 @[simp]
 theorem unload_boxes : unload (⌊⌊δ⌋⌋φ) = ⌈⌈δ⌉⌉(unload φ) := by
   induction δ
-  · simp
-  · simp_all only [LoadFormula.boxes, unload, Formula.boxes]
+  · simp only [LoadFormula.boxes, List.foldr_nil, Formula.boxes]
+  · simpa [Formula.boxes, LoadFormula.boxes]
 
 @[simp]
 theorem unload_neg_loaded : unload (~'⌊α⌋(.loaded χ)).1 = ⌈α⌉(unload χ) := by

Pdl/UnfoldBox.lean

@@ -693,7 +693,7 @@ theorem localBoxTruthI γ ψ (ℓ :TP γ) :
       · tauto
       · subst def_φ
         cases em (δ = [])
-        · simp_all only [Formula.boxes.eq_1, evaluate, ite_true] -- uses IHβ
+        · simp_all only [Formula.boxes_nil, evaluate, ite_true] -- uses IHβ
           clear IHβ
           rintro φ ((φ_in_Fβ) | ⟨δ, ⟨(δ_from_Pβ), def_φ⟩⟩)
           · apply rhs