WIP to upgrade to Lean v4.11

NOTES:

- DM ordering replaced with current PR files that still have sorry

- new sorry in soundness

Bml/Soundness.lean

@@ -81,9 +81,9 @@ theorem combMo_preserves_truth_at_oldWOrld {β : Type}
         constructor
         · intro newWorld
           unfold combinedModel
+          -- the new world is never reachable, trivial case
           tauto
-        -- the new world is never reachable, trivial case
-        · intro otherR otherWorld
+        · rintro ⟨otherR, otherWorld⟩
           intro rel_in_new_model
           specialize f_IH otherR otherWorld
           unfold combinedModel at rel_in_new_model

Makefile

@@ -22,7 +22,7 @@ dependencies.svg: Pdl/*.lean
 
 update-fix:
 	rm -rf .lake
-	echo "leanprover/lean4:v4.10.0" > lean-toolchain
+	echo "leanprover/lean4:v4.11.0" > lean-toolchain
 	echo "If next command fails, edit lakefile.lean manually."
-	grep v4.10.0 lakefile.lean
+	grep v4.11.0 lakefile.lean
 	lake update -R

Pdl/Examples.lean

@@ -133,7 +133,7 @@ example (a b : Program) (X : Formula) :
   constructor
   · intro lhs
     constructor
-    · simp_all only [true_or]
+    · simp_all
     · constructor
       · intro v w_a_v u
         intro v_aSubS_w

Pdl/LoadSplit.lean

@@ -1,4 +1,5 @@
 import Pdl.Syntax
+import Mathlib.Tactic.Use
 
 /-! ## Spliting of loaded formulas -/
 

Pdl/LocalTableau.lean

@@ -143,10 +143,8 @@ inductive LoadRule : NegLoadFormula → List (List Formula × Option NegLoadForm
 /-- Given a LoadRule application, define the equivalent unloaded rule application.
 This allows re-using `oneSidedLocalRuleTruth` to prove `loadRuleTruth`. -/
 def LoadRule.unload : LoadRule (~'χ) B → OneSidedLocalRule [~(unload χ)] (B.map pairUnload)
-| @dia α χ => by
-    convert OneSidedLocalRule.dia α ((_root_.unload χ)) <;> simp [unfoldDiamondLoaded_eq α χ]
-| @dia' α φ => by
-    convert OneSidedLocalRule.dia α φ  <;> simp [unfoldDiamondLoaded'_eq α φ]
+| @dia α χ => unfoldDiamondLoaded_eq α χ ▸ OneSidedLocalRule.dia α ((_root_.unload χ))
+| @dia' α φ => unfoldDiamondLoaded'_eq α φ ▸ OneSidedLocalRule.dia α φ
 
 /-- The loaded unfold rule is sound and invertible.
 In the notes this is part of localRuleTruth. -/
@@ -363,6 +361,7 @@ theorem localRuleTruth
         · intro g g_in
           subst def_f
           simp_all [pairUnload, negUnload, conEval]
+          have := w_f (~unload val.1)
           aesop
     · rintro ⟨Ci, ⟨⟨X, O, ⟨in_ress, def_Ci⟩⟩, w_Ci⟩⟩
       intro f f_in
@@ -413,6 +412,7 @@ theorem localRuleTruth
         · intro g g_in
           subst def_f
           simp_all [pairUnload, negUnload, conEval]
+          have := w_f (~unload val.1)
           aesop
     · rintro ⟨Ci, ⟨⟨X, O, ⟨in_ress, def_Ci⟩⟩, w_Ci⟩⟩
       intro f f_in
@@ -545,13 +545,13 @@ def preconP_to_submultiset (preconditionProof : List.Sublist Lcond L ∧ List.Su
     cases g <;> (rename_i nlform; cases nlform; simp_all)
 
 @[simp]
-def lt_TNode (X : TNode) (Y : TNode) := MultisetLT (node_to_multiset X) (node_to_multiset Y)
+def lt_TNode (X : TNode) (Y : TNode) := MultisetDMLT (node_to_multiset X) (node_to_multiset Y)
 
 -- Needed for termination of endNOdesOf.
 -- Here we use `dm_wf` from MultisetOrder.lean.
 instance : WellFoundedRelation TNode where
   rel := lt_TNode
-  wf := InvImage.wf node_to_multiset (dm_wf Formula.WellFoundedLT)
+  wf := InvImage.wf node_to_multiset (dmLT_wf Formula.WellFoundedLT)
 
 theorem LocalRule.cond_non_empty (rule : LocalRule (Lcond, Rcond, Ocond) X) :
     node_to_multiset (Lcond, Rcond, Ocond) ≠ ∅ :=
@@ -687,16 +687,16 @@ def MultisetLT' {α} [DecidableEq α] [Preorder α] (M : Multiset α) (N : Multi
 
 -- The definition used in the DM proof is equivalent to the standard definition.
 -- TODO: Move to MultisetOrder
-theorem MultisetLT.iff_MultisetLT' [DecidableEq α] [Preorder α] {M N : Multiset α} :
-    MultisetLT M N ↔ MultisetLT' M N := by
+theorem MultisetDMLT.iff_MultisetLT' [DecidableEq α] [Preorder α] {M N : Multiset α} :
+    MultisetDMLT M N ↔ MultisetLT' M N := by
   unfold MultisetLT'
   constructor
   · intro M_LT_N
     cases M_LT_N
     aesop
   · intro M_LT'_N
     rcases M_LT'_N with ⟨X,Y,Z,claim⟩
-    apply MultisetLT.MLT X Y Z
+    apply MultisetDMLT.DMLT X Y Z
     all_goals tauto
 
 theorem localRuleApp.decreases_DM {X : TNode} {B : List TNode}
@@ -710,7 +710,7 @@ theorem localRuleApp.decreases_DM {X : TNode} {B : List TNode}
   rcases RES_in with ⟨⟨Lnew,Rnew,Onew⟩, Y_in_ress, claim⟩
   unfold lt_TNode
   simp at claim
-  rw [MultisetLT.iff_MultisetLT']
+  rw [MultisetDMLT.iff_MultisetLT']
   unfold MultisetLT'
   use node_to_multiset (Lnew, Rnew, Onew) -- choose X to be the newly added formulas
   use node_to_multiset (Lcond, Rcond, Ocond) -- choose Y to be the removed formulas

Pdl/Modelgraphs.lean

@@ -269,7 +269,7 @@ theorem loadedTruthLemmaProg {Worlds} (MG : ModelGraph Worlds) α :
           simp [F]
           convert ψ_in
         apply (loadedTruthLemma MG X ψ).1
-        apply mysat; left; simp [F]; assumption
+        apply mysat.1; simp [F]; assumption
       -- now use Lemma 34:
       have := existsBoxFP β X_β_Z ℓ X_ConF
       rcases this with ⟨δ, δ_in_P, X_δ_Z⟩
@@ -302,12 +302,9 @@ theorem loadedTruthLemmaProg {Worlds} (MG : ModelGraph Worlds) α :
       case inr δ_notEmpty =>
         have : (δ ++ [∗β]) ∈ P (∗β) ℓ := by
           simp [P]
-          apply List.mem_filter_of_mem
           all_goals simp_all
         have δβSφ_in_X : (⌈⌈δ⌉⌉⌈∗β⌉φ) ∈ X.1 := by
-          apply mysat
-          right
-          use δ ++ [∗β]
+          have := mysat.2 _ this
           simp_all [boxes_append]
         have : (⌈∗β⌉φ) ∈ Z.1 := by
           clear innerIH