update to Lean 4.12

Bml/Partitions.lean

@@ -307,9 +307,9 @@ theorem endNodesOfChildSublistEndNodes
     (c_in_C : cLR ∈ C)
     lrApp
     : (endNodesOf ⟨cLR, subTabs cLR c_in_C⟩).Sublist (endNodesOf ⟨LR, LocalTableau.fromRule lrApp subTabs⟩) := by
-  simp_all [endNodesOf]
-  apply List.sublist_join
-  simp_all
+  simp_all only [lrEndNodes]
+  apply List.sublist_join_of_mem
+  simp_all only [List.mem_map, List.mem_attach, true_and, Subtype.exists]
   use cLR, c_in_C
 
 open List

Bml/Tableau.lean

@@ -59,7 +59,7 @@ def SimpleForm : Formula → Prop
   | _ => False
 
 instance : Decidable (SimpleForm φ) :=
-  match h : φ with
+  match φ with
   | ⊥
   | ·_
   | □_  => Decidable.isTrue <| by aesop
@@ -204,13 +204,13 @@ inductive LocalRuleApp : TNode → List TNode → Type
 
 theorem oneSidedRule_preserves_other_side_L
   {ruleApp : LocalRuleApp (L, R) C}
-  (hmyrule : ruleApp = (@LocalRuleApp.mk L R C (List.map (fun res => (res, ∅)) _) _ _ rule hC preproof))
+  (_ : ruleApp = (@LocalRuleApp.mk L R C (List.map (fun res => (res, ∅)) _) _ _ rule hC preproof))
   (rule_is_left : rule = LocalRule.oneSidedL orule )
   : ∀ c ∈ C, c.2 = R := by aesop
 
 theorem oneSidedRule_preserves_other_side_R
   {ruleApp : LocalRuleApp (L, R) C}
-  (hmyrule : ruleApp = (@LocalRuleApp.mk L R C (List.map (fun res => (∅, res)) _) _ _ rule hC preproof))
+  (_ : ruleApp = (@LocalRuleApp.mk L R C (List.map (fun res => (∅, res)) _) _ _ rule hC preproof))
   (rule_is_right : rule = LocalRule.oneSidedR orule )
   : ∀ c ∈ C, c.1 = L := by aesop
 
@@ -820,7 +820,9 @@ theorem existsLocalTableauFor LR : Nonempty (LocalTableau LR) :=
       apply LocalTableau.fromSimple
       by_contra hyp
       have := notSimpleThenLocalRule hyp
-      aesop
+      rcases this with ⟨Lcond, Rcond, ress, lr, Lin, Rin⟩
+      absurd canApplyRule
+      tauto
     case inr canApplyRule =>
       rw [not_not] at canApplyRule
       rcases canApplyRule with ⟨LCond, RCond, C, lr_exists, preconL, preconR⟩

Bml/Tableauexamples.lean

@@ -139,23 +139,7 @@ example : ClosedTableau ({r⋀~(□p), r↣□(p⋀q)}, {}) :=
       intro Y Y_in
       simp (config := {decide := true}) at *
       have : Y = ({·'r', ~(□p), □(p⋀q)}, {}) := by
-        rcases Y_in with ⟨l, ⟨a, ⟨a_def, def_l⟩⟩, Y_in_l⟩
-        subst_eqs
-        simp [endNodesOf] at *
-        rcases Y_in_l with ⟨l, ⟨a, ⟨a_def, def_l⟩⟩, Y_in_l⟩
-        cases a_def
-        · subst_eqs
-          simp [endNodesOf] at *
-        · subst_eqs
-          simp [endNodesOf] at *
-          have : ({·'r', ~(□p), ~~(□(p⋀q))}, ∅) ≠ (({·'r', ~(□p), ~·'r'}: Finset Formula), (∅ : Finset Formula)) := by decide
-          simp only [this] at Y_in_l
-          simp at Y_in_l
-          clear this -- hmm
-          rcases Y_in_l with ⟨l, ⟨a, ⟨ a_def, def_l⟩ ⟩, Y_in_l⟩
-          subst_eqs
-          simp [endNodesOf] at *
-          subst Y_in_l
-          decide
+        subst Y_in
+        decide
       subst this
       exact subTabForEx2

Makefile

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

Pdl/LocalTableau.lean

@@ -89,31 +89,31 @@ theorem tautImp_iff_TNodeUnsat {φ ψ} {X : TNode} :
 /-! ## Different kinds of formulas as elements of TNode -/
 
 @[simp]
-instance : Membership Formula TNode := ⟨fun φ X => φ ∈ X.L ∨ φ ∈ X.R⟩
+instance : Membership Formula TNode := ⟨fun X φ => φ ∈ X.L ∨ φ ∈ X.R⟩
 
 @[simp]
-def NegLoadFormula_in_TNode (nlf : NegLoadFormula) (X : TNode) : Prop :=
+def NegLoadFormula.mem_TNode (X : TNode) (nlf : NegLoadFormula) : Prop :=
   X.O = some (Sum.inl nlf) ∨ X.O = some (Sum.inr nlf)
 
-instance : Decidable (NegLoadFormula_in_TNode nlf ⟨L,R,O⟩) := by
+instance : Decidable (NegLoadFormula.mem_TNode ⟨L,R,O⟩ nlf) := by
   refine
     if h : O = some (Sum.inl nlf) then isTrue ?_
     else if h2 : O = some (Sum.inr nlf) then isTrue ?_ else isFalse ?_
   all_goals simp; tauto
 
 def TNode.without : (LRO : TNode) → (naf : AnyNegFormula) → TNode
 | ⟨L,R,O⟩, ⟨.normal f⟩  => ⟨L \ {~f}, R \ {~f}, O⟩
-| ⟨L,R,O⟩, ⟨.loaded lf⟩ => if (NegLoadFormula_in_TNode (~'lf) ⟨L,R,O⟩) then ⟨L, R, none⟩ else ⟨L,R,O⟩
+| ⟨L,R,O⟩, ⟨.loaded lf⟩ => if ((~'lf).mem_TNode ⟨L,R,O⟩) then ⟨L, R, none⟩ else ⟨L,R,O⟩
 
 @[simp]
-instance : Membership NegLoadFormula TNode := ⟨NegLoadFormula_in_TNode⟩
+instance : Membership NegLoadFormula TNode := ⟨NegLoadFormula.mem_TNode⟩
 
-def AnyNegFormula_in_TNode : (anf : AnyNegFormula) → (X : TNode) → Prop
-| ⟨.normal φ⟩, X => (~φ) ∈ X
-| ⟨.loaded χ⟩, X => NegLoadFormula_in_TNode (~'χ) X -- FIXME: ∈ not working here
+def AnyNegFormula.mem_TNode : (X : TNode) → (anf : AnyNegFormula) → Prop
+| X, ⟨.normal φ⟩ => (~φ) ∈ X
+| X, ⟨.loaded χ⟩ => (~'χ).mem_TNode X -- FIXME: ∈ not working here
 
 @[simp]
-instance : Membership AnyNegFormula TNode := ⟨AnyNegFormula_in_TNode⟩
+instance : Membership AnyNegFormula TNode := ⟨AnyNegFormula.mem_TNode⟩
 
 /-! ## Local Tableaux -/
 
@@ -660,21 +660,32 @@ theorem preconP_to_submultiset (preconditionProof : List.Subperm Lcond L ∧ Lis
     have := List.Subperm.count_le (List.Subperm.append preconditionProof.1 preconditionProof.2.1) f
     cases g <;> (rename_i nlform; cases nlform; simp_all)
 
+-- easier way to do this?
+theorem Multiset.sub_of_le [DecidableEq α] {M N X Y: Multiset α} (h : N ≤ M) :
+    M - N + Y = X ↔ M + Y = X + N := by
+  constructor
+  · intro hyp
+    have := @tsub_eq_iff_eq_add_of_le _ _ _ _ _ _ _ _ _ Y _ h
+    sorry
+  · intro hyp
+    sorry
+
 /-- Applying `node_to_multiset` before or after `applyLocalRule` gives the same. -/
 theorem node_to_multiset_of_precon (precon : Lcond.Subperm L ∧ Rcond.Subperm R ∧ Ocond ⊆ O) :
     node_to_multiset (L, R, O) - node_to_multiset (Lcond, Rcond, Ocond) + node_to_multiset (Lnew, Rnew, Onew)
     = node_to_multiset (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, Olf.change O Ocond Onew) := by
   have := preconP_to_submultiset precon -- TODO: can we use this to avoid the `-`?
+  rw [Multiset.sub_of_le]
   simp only [node_to_multiset_eq]
-  simp only [Multiset.coe_add, List.append_assoc, Multiset.coe_sub, List.diff_append,
-    Multiset.coe_eq_coe]
+  -- simp only [Multiset.coe_add, List.append_assoc, Multiset.coe_sub, List.diff_append, Multiset.coe_eq_coe]
   rcases precon with ⟨Lpre, Rpre, Opre⟩
   -- we now get 3 * 3 * 3 = 27 cases
   all_goals cases O <;> try (rename_i O; cases O)
   all_goals cases Onew <;> try (rename_i Onew; cases Onew)
   all_goals cases Ocond <;> try (rename_i cond; cases cond)
-  all_goals simp_all -- deals with 12 out of 27 cases
+  all_goals try (simp_all; done) -- deals with 12 out of 27 cases
   all_goals
+    simp
     sorry
 
 @[simp]
@@ -783,20 +794,30 @@ theorem H_goes_down (α : Program) φ {Fs δ} (in_H : (Fs, δ) ∈ H α) {ψ} (i
         · have IHα := H_goes_down α φ in_H in_Fs'
           cases α
           all_goals
-            simp_all [testsOfProgram, lmOfFormula, List.attach_map_val]
+            simp [lmOfFormula] at IHα
+          all_goals
+            simp only [List.attach_map_val, testsOfProgram] at *
+            simp_all [lmOfFormula]
             try linarith
         · have IHβ := H_goes_down β φ in_Hβ in_Fs''
           cases β
           all_goals
             simp_all [H, testsOfProgram, lmOfFormula, List.attach_map_val]
             try linarith
-      · simp_all [testsOfProgram]
+          all_goals
+            simp_all only [Function.comp_def, List.attach_map_val]
+            linarith
+      · simp_all only [ite_false, List.mem_singleton, Prod.mk.injEq, testsOfProgram,
+        List.attach_append, List.map_append, List.map_map, List.sum_append]
+        rw [Function.comp_def, Function.comp_def, List.attach_map_val, List.attach_map_val]
         cases in_l
         subst_eqs
         have IHα := H_goes_down α φ in_H in_Fs
         cases α
         all_goals
           simp_all [H, testsOfProgram, lmOfFormula, List.attach_map_val]
+        all_goals
+          try rw [Function.comp_def, Function.comp_def, List.attach_map_val, List.attach_map_val] at IHα
           try linarith
   case union α β =>
     simp [H] at in_H
@@ -806,11 +827,15 @@ theorem H_goes_down (α : Program) φ {Fs δ} (in_H : (Fs, δ) ∈ H α) {ψ} (i
       all_goals
         simp_all [H, testsOfProgram, lmOfFormula, List.attach_map_val]
         try linarith
+      all_goals
+        sorry
     · have IHβ := H_goes_down β φ hyp in_Fs
       cases β
       all_goals
         simp_all [H, testsOfProgram, lmOfFormula, List.attach_map_val]
         try linarith
+      all_goals
+        sorry
   case star α =>
     simp [H] at in_H
     rcases in_H with _ | ⟨l, ⟨Fs', δ', in_H', def_l⟩, in_l⟩
@@ -838,7 +863,7 @@ theorem unfoldDiamond.decreases_lmOf_nonAtomic {α : Program} {φ : Formula} {X
   · cases α <;> simp_all [Program.isAtomic, testsOfProgram, List.attach_map_val]
     case sequence α β =>
       suffices lmOfFormula ψ < (List.map lmOfFormula (testsOfProgram (α;'β))).sum.succ by
-        simp_all [testsOfProgram]
+        simp_all [testsOfProgram, Function.comp_def, List.attach_map_val]
         linarith
       suffices ∃ τ' ∈ testsOfProgram (α;'β), lmOfFormula ψ < 1 + lmOfFormula τ' by
         rw [Nat.lt_succ]
@@ -850,7 +875,7 @@ theorem unfoldDiamond.decreases_lmOf_nonAtomic {α : Program} {φ : Formula} {X
       aesop
     case union α β =>
       suffices lmOfFormula ψ < (List.map lmOfFormula (testsOfProgram (α⋓β))).sum.succ by
-        simp_all [testsOfProgram]
+        simp_all [testsOfProgram, Function.comp_def, List.attach_map_val]
         linarith
       suffices ∃ τ' ∈ testsOfProgram (α;'β), lmOfFormula ψ < 1 + lmOfFormula τ' by
         rw [Nat.lt_succ]

Pdl/MultisetOrder.lean

@@ -45,7 +45,6 @@ lemma singleton_add_sub_of_cons_add [DecidableEq α] {a a0: α} {M X : Multiset
 theorem sub_singleton [DecidableEq α] (a : α) (s : Multiset α) : s - {a} = s.erase a := by
   ext
   simp [Multiset.erase_singleton, Multiset.count_singleton]
-  split <;> simp_all
 
 theorem mem_sub_of_not_mem_of_mem {α} [DecidableEq α] (x : α) (X Y: Multiset α) (x_in_X : x ∈ X)
     (x_notin_Y : x ∉ Y) : x ∈ X - Y  := by
@@ -136,13 +135,6 @@ lemma not_redLT_zero [DecidableEq α] [LT α] (M: Multiset α) : ¬ MultisetRedL
       simp_all only [Multiset.mem_add, Multiset.mem_singleton, or_true]
     contradiction
 
--- Should be added to 'mathlib4/Mathlib/Data/Multiset/Basic.lean'
-lemma mul_singleton_erase [DecidableEq α] {a : α} {M : Multiset α} :
-    M - {a} = M.erase a := by
-  ext
-  simp [Multiset.erase_singleton, Multiset.count_singleton]
-  split <;> simp_all
-
 lemma red_insert [DecidableEq α] [LT α] {a : α} {M N : Multiset α} (h : MultisetRedLT N (a ::ₘ M)) :
     ∃ M',
       N = (a ::ₘ M') ∧ (MultisetRedLT M' M) ∨ (N = M + M') ∧ (∀ x : α, x ∈ M' → x < a) := by
@@ -165,7 +157,6 @@ lemma red_insert [DecidableEq α] [LT α] {a : α} {M N : Multiset α} (h : Mult
         · have := h0 b
           aesop
         · have := h0 b
-          simp [mul_singleton_erase]
           aesop
       subst this
       rw [add_comm]
@@ -179,7 +170,7 @@ lemma red_insert [DecidableEq α] [LT α] {a : α} {M N : Multiset α} (h : Mult
         have a0M: a0 ∈ M := by
           apply in_of_ne_of_cons_erase
           · change M = Multiset.erase (a0 ::ₘ X) a
-            rw [mul_singleton_erase, add_comm] at this0
+            rw [Multiset.sub_singleton, add_comm] at this0
             exact this0
           · exact hyp
         rw [add_comm]

Pdl/Soundness.lean

@@ -126,8 +126,8 @@ theorem pdlRuleSat (r : PdlRule X Y) (satX : satisfiable X) : satisfiable Y := b
 The `loc` ad `pdl` steps correspond to two out of three constructors of `Tableau`. -/
 inductive PathIn : ∀ {H X}, Tableau H X → Type
 | nil : PathIn _
-| loc : (Y_in : Y ∈ endNodesOf lt) → (tail : PathIn (next Y Y_in)) → PathIn (Tableau.loc lt next)
-| pdl : (r : PdlRule Γ Δ) → PathIn (child : Tableau (Γ :: Hist) Δ) → PathIn (Tableau.pdl r child)
+| loc {Y lt next} : (Y_in : Y ∈ endNodesOf lt) → (tail : PathIn (next Y Y_in)) → PathIn (Tableau.loc lt next)
+| pdl {Γ Δ Hist child} : (r : PdlRule Γ Δ) → PathIn (child : Tableau (Γ :: Hist) Δ) → PathIn (Tableau.pdl r child)
 deriving DecidableEq
 
 def tabAt : PathIn tab → Σ H X, Tableau H X
@@ -368,7 +368,7 @@ theorem not_edge_nil (tab : Tableau Hist X) (t : PathIn tab) : ¬ edge t .nil :=
     subst X_eq_Z
     rw [heq_eq_eq] at hyp
     subst hyp
-    simp_all only
+    simp_all
 
 theorem nodeAt_loc_nil {H : List TNode} {lt : LocalTableau X}
     (next : (Y : TNode) → Y ∈ endNodesOf lt → Tableau (X :: H) Y) (Y_in : Y ∈ endNodesOf lt) :

Pdl/UnfoldBox.lean

@@ -121,7 +121,7 @@ theorem signature_contradiction_of_neq_TPs {ℓ ℓ' : TP α} :
     constructor
     · use τ, τ_in
       simp_all
-    · assumption
+    · simp_all
 
 -- unused?
 theorem equiv_iff_TPequiv : φ ≡ ψ  ↔  ∀ ℓ : TP α, φ ⋀ signature α ℓ ≡ ψ ⋀ signature α ℓ := by
@@ -270,15 +270,16 @@ theorem P_goes_down : γ ∈ δ → δ ∈ P α ℓ → (if α.isAtomic then γ
     case nil =>
       exfalso; cases γ_in
     case cons =>
-      simp_all only [false_or]
-      rcases δ_in with ⟨αs, αs_in, def_δ⟩
+      simp only [reduceCtorEq, false_or] at δ_in
+      rcases δ_in with ⟨αs, ⟨αs_in, αs_not_null⟩, def_δ⟩
       cases em (γ ∈ αs)
       case inl γ_in =>
-        have IH := P_goes_down γ_in αs_in.1
+        have IH := P_goes_down γ_in αs_in
         cases em (α.isAtomic) <;> cases em α.isStar
         all_goals (simp_all;try linarith)
       case inr γ_not_in =>
-        have : γ = (∗α) := by rw [← def_δ] at γ_in; simp at γ_in; tauto
+        have : γ = (∗α) := by
+          rw [← def_δ] at γ_in; simp at γ_in; tauto
         subst_eqs
         simp
   case test τ =>
@@ -746,9 +747,9 @@ theorem localBoxTruthI γ ψ (ℓ :TP γ) :
     simp only [evaluate, and_congr_left_iff, relate] at *
     intro w_sign_ℓ
     specialize IHα ?_
-    · simp_all [signature, conEval, testsOfProgram]; intro f τ τ_in; apply w_sign_ℓ; aesop
+    · simp_all [signature, conEval, testsOfProgram]
     specialize IHβ ?_
-    · simp_all [signature, conEval, testsOfProgram]; intro f τ τ_in; apply w_sign_ℓ; aesop
+    · simp_all [signature, conEval, testsOfProgram]
     -- rewrite using semantics of union and the two IH:
     have : (∀ (v : W), relate M α w v ∨ relate M β w v → evaluate M v ψ)
         ↔ ((∀ (v : W), relate M α w v → evaluate M v ψ)
@@ -825,9 +826,9 @@ theorem localBoxTruthI γ ψ (ℓ :TP γ) :
     simp only [evaluate, relate, forall_exists_index, and_imp, and_congr_left_iff] at *
     intro w_sign_ℓ
     specialize IHα ?_
-    · simp_all [signature, conEval, testsOfProgram]; intro f τ τ_in; apply w_sign_ℓ; aesop
+    · simp_all [signature, conEval, testsOfProgram]
     specialize IHβ ?_
-    · simp_all [signature, conEval, testsOfProgram]; intro f τ τ_in; apply w_sign_ℓ; aesop
+    · simp_all [signature, conEval, testsOfProgram]
     -- only rewriting with IHα here, but not yet IHβ
     have : (∀ (v x : W), relate M α w x → relate M β x v → evaluate M v ψ)
           ↔ ∀ (v : W), relate M α w v → ∀ (v_1 : W), relate M β v v_1 → evaluate M v_1 ψ := by
@@ -843,9 +844,12 @@ theorem localBoxTruthI γ ψ (ℓ :TP γ) :
       · tauto
       · rw [F_mem_iff_neg β ℓ φ] at φ_in_Fβ
         rcases φ_in_Fβ with ⟨τ, τ_in, def_φ, not_ℓ_τ⟩
-        apply w_sign_ℓ _ τ
-        · simp_all
-        · simp_all [testsOfProgram]
+        apply w_sign_ℓ φ
+        subst def_φ
+        simp_all only [testsOfProgram]
+        right
+        use τ, τ_in
+        simp_all
       · subst def_φ
         apply lhs
         right
@@ -859,7 +863,7 @@ theorem localBoxTruthI γ ψ (ℓ :TP γ) :
           apply IHβ.1 ?_ (⌈⌈δ⌉⌉ψ) <;> clear IHβ
           · right; aesop
           · have := lhs (⌈β⌉ψ)
-            simp at this; apply this; clear this -- sounds like daft punk ;-)
+            simp only [evaluate] at this; apply this; clear this -- sounds like daft punk ;-)
             right
             use []
             simp_all