Optimize PDL proof search and tableau measures

LeanPool/PDL/AllPdlRule.lean

@@ -135,7 +135,7 @@ lemma PdlRule.all_spec {X Y} (bas : X.basic) (r : PdlRule X Y) : ⟨Y, r⟩ ∈
       cases α_def : α <;> simp_all only [LoadFormula.boxes_nil, all, Finset.singleton_union,
         AnyFormula.split, LoadFormula.unload, List.cons_append, List.nil_append, List.mem_cons,
         Sigma.mk.injEq, Finset.union_singleton, List.not_mem_nil, or_false]
-      case atom_prog a => aesop
+      case atom_prog a => aesop (rule_sets := [-default])
       all_goals
         -- Here we need `bas` to disallow non-atomic freeL applications
         subst_eqs
@@ -180,7 +180,7 @@ lemma PdlRule.all_spec {X Y} (bas : X.basic) (r : PdlRule X Y) : ⟨Y, r⟩ ∈
       cases α_def : α <;> simp_all only [LoadFormula.boxes_nil, all, Finset.singleton_union,
         AnyFormula.split, LoadFormula.unload, List.cons_append, List.nil_append, List.mem_cons,
         Sigma.mk.injEq, Finset.union_singleton, List.not_mem_nil, or_false]
-      case atom_prog a => aesop
+      case atom_prog a => aesop (rule_sets := [-default])
       all_goals
         -- Here we need `bas` to disallow non-atomic freeL applications
         subst_eqs

LeanPool/PDL/Beth.lean

@@ -49,7 +49,7 @@ theorem beth (φ : Formula) (h : φ.impDef p) :
       and_imp] at h
     intro w_φp0 w_p0
     specialize h w_φp0
-    aesop
+    aesop (rule_sets := [-default])
   rcases interpolation this with ⟨ψ, ip_voc, ip_one, ip_two⟩
   clear this
   use ψ
@@ -85,7 +85,7 @@ theorem beth (φ : Formula) (h : φ.impDef p) :
         simp only [Formula.voc, Finset.union_singleton, Finset.mem_inter, Finset.mem_insert,
           true_or, Sum.inl.injEq, p0_neq_p1, false_or, true_and] at ip_voc
         rw [repl_in_F_voc_def] at ip_voc
-        aesop
+        aesop (rule_sets := [-default])
     have ip_two_p : tautology (ψ ↣ (φ ↣ ·p)) := by
       clear ip_one
       have := non_occ_taut_then_taut_imp_repl_in
@@ -99,7 +99,7 @@ theorem beth (φ : Formula) (h : φ.impDef p) :
         simp only [Formula.voc, Finset.union_singleton, Finset.mem_inter, Finset.mem_insert,
           Sum.inl.injEq, true_or, and_true] at ip_voc
         rw [repl_in_F_voc_def] at ip_voc
-        aesop
+        aesop (rule_sets := [-default])
       · assumption
     intro W M w w_φ
     simp at w_φ

LeanPool/PDL/Completeness/BuildTree.lean

@@ -120,7 +120,7 @@ lemma BuildTree.size_lt_loc (H : History) (X : Sequent) (nbas : ¬X.basic)
   have : ∀ lt, (next lt).size = (next lt).6.size := fun lt => by
     cases next lt; simp [BuildChoice.size]
   simp_rw [this]
-  grind
+  grind only []
 
 lemma BuildTree.size_lt_pdl (H : History) (X : Sequent) (bas : X.basic)
     (someR : PdlRule.all X ≠ [])
@@ -131,7 +131,7 @@ lemma BuildTree.size_lt_pdl (H : History) (X : Sequent) (bas : X.basic)
     simp only [List.mem_map, Sigma.exists]
     use Y, r, PdlRule.all_spec bas _
   have := List.le_sum_of_mem this
-  grind
+  grind only []
 
 @[simp]
 lemma BuildChoice.fst_eq {H X YS} {bc : BuildChoice H X YS} : bc.1 = H := by cases bc; rfl
@@ -512,7 +512,7 @@ lemma Match.btAt_newHist_length_eq_length_plus_oldHist {H X} {bt : BuildTree H X
     unfold btAt
     rw [IH]
     simp
-    grind
+    grind only []
   | pdl tail => by
     have IH := Match.btAt_newHist_length_eq_length_plus_oldHist tail
     simp only [length]

LeanPool/PDL/Completeness/BuildTreeExistence.lean

@@ -221,7 +221,7 @@ lemma Sequent.not_closed_of_sub {L R L' R' : Finset Formula} {O O' : Olf}
     (hL : ∀ f ∈ L', f ∈ L) (hR : ∀ f ∈ R', f ∈ R) (h : ¬ Sequent.closed ⟨L, R, O⟩) :
     ¬ Sequent.closed ⟨L', R', O'⟩ := by
   simp only [Sequent.closed, Sequent.mem_def, Sequent.L_eq, Sequent.R_eq] at h ⊢
-  grind
+  grind only []
 
 /-- Applying the rule `(L-)` to free the loaded formula: all formulas we had are kept. -/
 lemma PdlRule.exists_freeStep {Z : Sequent} (hZ : Z.O ≠ none) :

LeanPool/PDL/Completeness/Modelgraphs.lean

@@ -108,7 +108,7 @@ theorem loadClaimHelper {Worlds : Finset (Finset Formula)}
         rw [← length_def]
         simp only [List.append_eq, List.length_append, List.length_cons, List.length_nil,
           zero_add] at hyp
-        linarith
+        omega
       simp only [pairRel, List.zip_cons_cons, List.append_eq, List.getElem_cons_succ,
         List.getElem_zip] at lchain
       convert lchain
@@ -254,8 +254,9 @@ theorem loadedTruthLemmaProg {Worlds} (MG : ModelGraph Worlds) α :
     induction n generalizing X φ -- not generalizing Y, but φ to be replaced φ with ⌈∗β⌉φ below!
     · rcases claim with ⟨YS, X_def, Y_def, _⟩
       have : YS.head = YS.last := by
+        clear * -YS
         have := List.Vector.exists_eq_cons YS
-        aesop
+        aesop (rule_sets := [-default])
       rw [this] at X_def
       subst X_def Y_def
       have := ((MG.2.1 (YS.last)).1 φ φ (∗β)).right.right.right.left boxP_in_X
@@ -265,9 +266,10 @@ theorem loadedTruthLemmaProg {Worlds} (MG : ModelGraph Worlds) α :
       rcases claim with ⟨YS, X_def, Y_def, relSteps⟩
       let Z := YS.get 1
       have X_β_Z : relate MG.1 β X Z := by
+        clear * -relSteps X_def
         specialize relSteps 0
         unfold Z
-        convert relSteps <;> aesop
+        convert relSteps <;> aesop (rule_sets := [-default])
       have := ((MG.2.1 X).1 φ φ (∗β)).right.right.right.left boxP_in_X
       rcases this with ⟨ℓ, mysat⟩
       simp only [Bset, List.all_append, List.all_map, Bool.and_eq_true, List.all_eq_true,
@@ -297,18 +299,18 @@ theorem loadedTruthLemmaProg {Worlds} (MG : ModelGraph Worlds) α :
         refine ⟨YS.tail, ?_, ?_, ?_⟩
         · rw [← List.Vector.get_zero]
           rw [List.Vector.get_tail_succ]
-          aesop
+          aesop (rule_sets := [-default])
         · rw [List.Vector.last_def]
           rw [List.Vector.get_tail_succ]
-          aesop
+          aesop (rule_sets := [-default])
         · intro i
           clear * -relSteps
           specialize relSteps i.succ
           have : ((List.Vector.tail YS).get i.castSucc) = (YS.get ((Fin.succ i).castSucc)) := by
-            aesop
+            aesop (rule_sets := [-default])
           rw [this]; clear this
           have : ((List.Vector.tail YS).get i.succ) = (YS.get ((Fin.succ i).succ)) := by
-            aesop
+            aesop (rule_sets := [-default])
           rw [this]; clear this
           exact relSteps
       case inr δ_notEmpty =>
@@ -360,9 +362,11 @@ theorem loadedTruthLemmaProg {Worlds} (MG : ModelGraph Worlds) α :
         · intro i
           clear * -relSteps
           specialize relSteps i.succ
-          have : ((List.Vector.tail YS).get i.castSucc) = (YS.get i.succ.castSucc) := by aesop
+          have : ((List.Vector.tail YS).get i.castSucc) = (YS.get i.succ.castSucc) := by
+            aesop (rule_sets := [-default])
           rw [this]; clear this
-          have : ((List.Vector.tail YS).get i.succ) = (YS.get i.succ.succ) := by aesop
+          have : ((List.Vector.tail YS).get i.succ) = (YS.get i.succ.succ) := by
+            aesop (rule_sets := [-default])
           rw [this]; clear this
           exact relSteps
   -- remaining cases: sequence, union, test
@@ -384,7 +388,7 @@ theorem loadedTruthLemmaProg {Worlds} (MG : ModelGraph Worlds) α :
       (by simp only [vDash.SemImplies, evaluatePoint, conEval]; exact X_F)
     rcases this with ⟨δ, δ_in_P, X_δ_Y⟩
     have δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ X.val := by
-      simp_all only [relate, Subtype.exists]
+      clear * -Bset_sub_X δ_in_P α_def
       subst_eqs
       apply Bset_sub_X
       right
@@ -458,13 +462,14 @@ theorem Qsteps_single : Qsteps R [α] v w ↔ Q R α v w := by
 theorem Qsteps_append : Qsteps R (δ1 ++ δ2) v w ↔ ∃ u, Qsteps R δ1 v u ∧ Qsteps R δ2 u w := by
   induction δ1 generalizing v w
   case nil =>
-    simp [Qsteps]
+    simp only [List.nil_append, Qsteps, beq_iff_eq, exists_eq_left']
   case cons α δ IH =>
-    simp only [List.cons_append, Qsteps, Relation.Comp, Subtype.exists]
-    constructor <;> rintro ⟨z, z_in, hyp⟩
-    · rw [IH] at hyp
-      aesop
-    · aesop
+    simp only [List.cons_append, Qsteps, Relation.Comp, IH]
+    constructor
+    · rintro ⟨u, hu, z, h1, h2⟩
+      exact ⟨z, ⟨u, hu, h1⟩, h2⟩
+    · rintro ⟨z, ⟨u, hu, h1⟩, h2⟩
+      exact ⟨u, hu, z, h1, h2⟩
 
 /-- Q_Fδ for a list of tests F and a list or programs δ. -/
 def Qcombo {W : Finset (Finset Formula)} (R : Nat → W → W → Prop)

LeanPool/PDL/Completeness/TableauGame.lean

@@ -74,7 +74,7 @@ def posOf (H : History) (X : Sequent) : ProverPos H X ⊕ BuilderPos H X :=
 lemma posOf_eq_inr_then_lpr {H X p} :
     posOf H X = Sum.inr p → ∃ lpr, p = .lpr lpr := by
   unfold posOf
-  grind
+  grind only []
 
 /-! ## Moves -/
 
@@ -206,7 +206,7 @@ private theorem theMoves_loaded_forward {H : History} {next : GamePos}
   dsimp only
   unfold theMoves at mv
   rcases χ with (⟨⟨χ⟩⟩|⟨⟨χ⟩⟩) <;> rcases χ with ⟨δ,φ|χ⟩ <;> cases δ <;> simp_all
-  all_goals grind
+  all_goals grind only []
 
 /-- Characterization of `theMoves`. -/
 lemma theMoves_iff {H X} {p : ProverPos H X ⊕ BuilderPos H X} {next : GamePos} :
@@ -363,7 +363,7 @@ lemma no_moves_of_rep {H X pos} (h : rep H X ∧ X.isFree) :
   push Not at hyp
   rcases hyp with ⟨p, p_in⟩
   unfold theMoves at p_in
-  rcases X with ⟨L,R,_|o⟩ <;> rcases pos with (_|_|_)|(_|_) <;> aesop
+  rcases X with ⟨L,R,_|o⟩ <;> rcases pos with (_|_|_)|(_|_) <;> aesop (rule_sets := [-default])
 
 /-- The finite set given by `theMoves` indeed agrees with the relation `move`.
 Other direction is `mem_theMoves_of_move`. -/
@@ -451,7 +451,7 @@ lemma move_of_mem_theMoves {pos next} :
           simp [loadMulti, LoadFormula.boxes]
       · constructor; apply Move.prPdl; apply PdlRule.modR rfl rfl
     all_goals
-      grind
+      grind only []
   · subst mv
     exact ⟨Move.prLocTab⟩
   · subst mv
@@ -494,7 +494,7 @@ lemma mem_theMoves_of_move {pos next} :
           use a, AnyFormula.normal ψ
           simp only [AnyFormula.normal.injEq, exists_eq_left', reduceCtorEq, false_and,
             exists_false, LoadFormula.unload, false_or, true_and]
-          aesop
+          aesop (rule_sets := [-default])
         all_goals
           absurd bas
           rintro ⟨bas, nclos⟩
@@ -529,7 +529,7 @@ lemma mem_theMoves_of_move {pos next} :
           use a, AnyFormula.normal ψ
           simp only [AnyFormula.normal.injEq, exists_eq_left', reduceCtorEq, false_and,
             exists_false, LoadFormula.unload, false_or, true_and]
-          aesop
+          aesop (rule_sets := [-default])
         all_goals
           absurd bas
           rintro ⟨bas, nclos⟩
@@ -560,22 +560,22 @@ lemma mem_theMoves_of_move {pos next} :
       left
       use a, ξ
       simp only [true_and]
-      cases ξ <;> grind
+      cases ξ <;> grind only []
     case some.modR =>
-    · grind -- sus that this works but did not in `modL` case?!
+    · grind only [] -- sus that this works but did not in `modL` case?!
   case prLocTab nbas nrep =>
-    grind
+    grind only []
   case buEnd Y ltX nbas Y_in nrep =>
-    grind
+    grind only []
 
 lemma move.hist {Hist next pos} (mov : move ⟨Hist, X, pos⟩ next) :
       (∃ newPos, next = ⟨Hist, X, newPos⟩) -- this is for the annoying `prLocTab` case;-)
     ∨ (∃ Y newPos, next = ⟨X :: Hist, Y, newPos⟩)  := by
   rcases mov with ⟨mov⟩
   cases mov
-  case prPdl => right; grind
-  case prLocTab => left; grind
-  case buEnd => right; grind
+  case prPdl => right; grind only []
+  case prLocTab => left; grind only []
+  case buEnd => right; grind only []
 
 lemma move.hist_suffix {Hist next pos} (mov : move ⟨Hist, X, pos⟩ next) : Hist <:+ next.1 := by
   have := move.hist mov
@@ -610,10 +610,10 @@ lemma move.trans_hist {pX pY} (movt : Relation.TransGen move pX pY) :
       simp_all
     · cases Y_def
       simp
-      aesop
+      aesop (rule_sets := [-default])
     · cases HXP_eq
       simp at *
-      aesop
+      aesop (rule_sets := [-default])
     · cases Y_def
       simp only [] at *
       rcases pX with ⟨X, H, p⟩
@@ -950,7 +950,7 @@ lemma move_then_not_flprep {H X next} {p : (ProverPos H X ⊕ BuilderPos H X)} :
     move ⟨H, X, p⟩ next → ¬ flprep H X := by
   simp only [move, Nonempty.forall]
   intro next_p hyp
-  cases next_p <;> grind
+  cases next_p <;> grind only []
 
 /-- Helper lemma for `matchesFinite`: if a property of natural numbers holds arbitrarily late,
 then we can enumerate witnesses for it with gaps of at least two. -/
@@ -1349,7 +1349,7 @@ theorem gameP_general Hist (X : Sequent) (sP : Strategy tableauGame Prover) (pos
         all_goals
           -- non-atomic program is impossible, X would not have been basic then
           exfalso
-          grind
+          grind only []
       · -- COPY PASTA only changed L to R
         rcases χ with ⟨α, (ψ : AnyFormula)⟩
         cases α
@@ -1377,7 +1377,7 @@ theorem gameP_general Hist (X : Sequent) (sP : Strategy tableauGame Prover) (pos
         all_goals
           -- non-atomic program is impossible, X would not have been basic then
           exfalso
-          grind
+          grind only []
     case nbas nrep X_nbas =>
       -- not basic, Prover must move to the uniform local tableau
       -- COPY PASTA from bas case ...

LeanPool/PDL/Completeness/Theorem.lean

@@ -147,7 +147,7 @@ theorem completeness : ∀ X, consistent X → satisfiable X :=
   intro f f_in
   apply truthLemma M w f
   apply h
-  aesop
+  aesop (rule_sets := [-default])
 
 theorem consIffSat : ∀ X, X.isFree → (consistent X ↔ satisfiable X) :=
   fun X X_isFree => ⟨completeness X, correctness X X_isFree⟩

LeanPool/PDL/Discon.lean

@@ -34,7 +34,7 @@ theorem conempty : con ∅ = (⊤ : Formula) := by rfl
 theorem consingle {f : Formula} : con [f] = f := by rfl
 
 theorem listEq_to_conEq : l1 = l2 → con l1 = con l2 := by
-  aesop
+  aesop (rule_sets := [-default])
 
 theorem conEvalHT {X f W M} {w : W} :
     evaluate M w (con (f :: X)) ↔ evaluate M w f ∧ evaluate M w (con X) :=
@@ -106,7 +106,7 @@ theorem disempty : dis ∅ = (⊥ : Formula) := rfl
 theorem dissingle {f : Formula} : dis [f] = f := rfl
 
 theorem listEq_to_disEq : l1 = l2 → dis l1 = dis l2 := by
-  aesop
+  aesop (rule_sets := [-default])
 
 theorem disEvalHT {X f W M} {w : W} :
     evaluate M w (dis (f :: X)) ↔ evaluate M w f ∨ evaluate M w (dis X) :=
@@ -356,7 +356,7 @@ theorem disconAnd {XS YS} : discon (XS ⊎ YS) ≡ discon XS ⋀ discon YS :=
     exists_exists_and_eq_and, exists_exists_and_exists_and_eq_and, List.mem_append, evaluate]
   rw [disconEval XS]
   rw [disconEval YS]
-  aesop
+  aesop (rule_sets := [-default])
 
 theorem union_elem_uplus {XS YS : Finset (Finset Formula)} {X Y : Finset Formula} :
   X ∈ XS → Y ∈ YS → ((X ∪ Y) ∈ (XS ⊎ YS)) :=
@@ -371,6 +371,6 @@ theorem mapCon_mapForall (M : KripkeModel W) w φ
     (∃ f ∈ List.map (fun Fδ => con (g Fδ φ)) X, evaluate M w f) ↔
     ∃ fs ∈ List.map (fun Fδ => g Fδ φ) X, ∀ f ∈ fs, evaluate M w f := by
   simp_all only [List.mem_map, Prod.exists, ↓existsAndEq, and_true]
-  constructor <;> grind [conEval]
+  constructor <;> grind only [conEval]
 
 end PDL

LeanPool/PDL/Distance.lean

@@ -257,7 +257,7 @@ lemma distance_list_eq_distance_steps (M : KripkeModel W) (v w : W) δ :
     (distanceList M v w δ) = (distance M (Program.steps δ) v w) := by
   induction δ generalizing v w
   · simp_all [distanceList, distance]
-    aesop
+    aesop (rule_sets := [-default])
   case cons α δ IH =>
     simp_all [distanceList, distance]
 
@@ -466,8 +466,8 @@ theorem relateSeq_existsD_dist (v_αγ_w : relateSeq M (α :: γ) v w)
     rw [distance_list_cons] at αγ_not_inf
     rw [distance_list_cons]
     refine ⟨u, ?_, ?_, u_minimizes⟩
-    · rw [← dist_iff_rel]; aesop
-    · rw [← distance_list_iff_relate_Seq]; aesop
+    · rw [← dist_iff_rel]; aesop (rule_sets := [-default])
+    · rw [← distance_list_iff_relate_Seq]; aesop (rule_sets := [-default])
   rcases claim with ⟨u, v_α_u, u_w, αγ_eq_α_γ⟩
   have := rel_existsD_dist v_α_u -- applying (f)
   rcases this with ⟨⟨X,δ⟩, in_D, v_X, δ_eq_α⟩
@@ -577,8 +577,8 @@ theorem exists_same_distance_list_relateSeq_concat (w_δα_v : relateSeq M (δ +
   rcases this with ⟨x, same_dist⟩
   refine ⟨x, ?_, ?_, same_dist⟩
   · rw [← distance_list_iff_relate_Seq]
-    aesop
+    aesop (rule_sets := [-default])
   · rw [← dist_iff_rel]
-    aesop
+    aesop (rule_sets := [-default])
 
 end PDL