diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean index a9ef24858b..98fcffaad5 100644 --- a/src/Init/Data/Array/Lemmas.lean +++ b/src/Init/Data/Array/Lemmas.lean @@ -986,7 +986,11 @@ theorem mem_or_eq_of_mem_set @[simp, grind] theorem setIfInBounds_empty {i : Nat} {a : α} : #[].setIfInBounds i a = #[] := rfl -@[simp] theorem set!_eq_setIfInBounds : @set! = @setIfInBounds := rfl +@[simp, grind =] theorem set!_eq_setIfInBounds : set! xs i v = setIfInBounds xs i v := rfl + +@[grind] +theorem setIfInBounds_def (xs : Array α) (i : Nat) (a : α) : + xs.setIfInBounds i a = if h : i < xs.size then xs.set i a else xs := rfl @[deprecated set!_eq_setIfInBounds (since := "2024-12-12")] abbrev set!_is_setIfInBounds := @set!_eq_setIfInBounds @@ -1078,7 +1082,7 @@ theorem mem_or_eq_of_mem_setIfInBounds by_cases h : i < xs.size <;> simp [setIfInBounds, Nat.not_lt_of_le, h, getD_getElem?] -@[simp] theorem toList_setIfInBounds {xs : Array α} {i : Nat} {x : α} : +@[simp, grind =] theorem toList_setIfInBounds {xs : Array α} {i : Nat} {x : α} : (xs.setIfInBounds i x).toList = xs.toList.set i x := by simp only [setIfInBounds] split <;> rename_i h diff --git a/src/Init/Data/List/Pairwise.lean b/src/Init/Data/List/Pairwise.lean index 75afb9ac8c..16f12d8daf 100644 --- a/src/Init/Data/List/Pairwise.lean +++ b/src/Init/Data/List/Pairwise.lean @@ -279,7 +279,7 @@ theorem nodup_nil : @Nodup α [] := theorem nodup_cons {a : α} {l : List α} : Nodup (a :: l) ↔ a ∉ l ∧ Nodup l := by simp only [Nodup, pairwise_cons, forall_mem_ne] -theorem Nodup.sublist : l₁ <+ l₂ → Nodup l₂ → Nodup l₁ := +@[grind →] theorem Nodup.sublist : l₁ <+ l₂ → Nodup l₂ → Nodup l₁ := Pairwise.sublist grind_pattern Nodup.sublist => l₁ <+ l₂, Nodup l₁ diff --git a/src/Init/Grind.lean b/src/Init/Grind.lean index 56db7d2b03..e7c05cc8f8 100644 --- a/src/Init/Grind.lean +++ b/src/Init/Grind.lean @@ -18,3 +18,4 @@ import Init.Grind.CommRing import Init.Grind.Module import Init.Grind.Ordered import Init.Grind.Ext +import Init.Data.Int.OfNat -- This may not have otherwise been imported, breaking `grind` proofs. diff --git a/src/Std/Sat/CNF/Literal.lean b/src/Std/Sat/CNF/Literal.lean index 724bf667eb..4091d705a2 100644 --- a/src/Std/Sat/CNF/Literal.lean +++ b/src/Std/Sat/CNF/Literal.lean @@ -21,7 +21,7 @@ namespace Literal /-- Flip the polarity of `l`. -/ -@[inline] +@[inline, grind =] def negate (l : Literal α) : Literal α := (l.1, !l.2) end Literal diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Assignment.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Assignment.lean index 927bf3c27f..0b28de5ac7 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Assignment.lean +++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Assignment.lean @@ -7,6 +7,9 @@ prelude import Init.ByCases import Std.Tactic.BVDecide.LRAT.Internal.Entails import Std.Tactic.BVDecide.LRAT.Internal.PosFin +import Init.Grind + +set_option grind.warning false namespace Std.Tactic.BVDecide namespace LRAT @@ -38,6 +41,8 @@ deriving Inhabited, DecidableEq, BEq namespace Assignment +attribute [local grind cases] Assignment + instance : ToString Assignment where toString := fun a => match a with @@ -108,102 +113,77 @@ def removeNegAssignment (oldAssignment : Assignment) : Assignment := | both => pos | unassigned => unassigned -- Note: This case should not occur -def addAssignment (b : Bool) : Assignment → Assignment := - if b then - addPosAssignment - else - addNegAssignment +attribute [local grind] hasPosAssignment hasNegAssignment addNegAssignment addPosAssignment + removePosAssignment removeNegAssignment -def removeAssignment (b : Bool) : Assignment → Assignment := +def addAssignment (b : Bool) (a : Assignment) : Assignment := if b then - removePosAssignment + addPosAssignment a else - removeNegAssignment + addNegAssignment a -def hasAssignment (b : Bool) : Assignment → Bool := +def removeAssignment (b : Bool) (a : Assignment) : Assignment := if b then - hasPosAssignment + removePosAssignment a else - hasNegAssignment + removeNegAssignment a + +def hasAssignment (b : Bool) (a : Assignment) : Bool := + if b then + hasPosAssignment a + else + hasNegAssignment a + +attribute [local grind] addAssignment removeAssignment hasAssignment theorem removePos_addPos_cancel {assignment : Assignment} (h : ¬(hasPosAssignment assignment)) : - removePosAssignment (addPosAssignment assignment) = assignment := by - cases assignment <;> simp_all [removePosAssignment, addPosAssignment, hasPosAssignment] + removePosAssignment (addPosAssignment assignment) = assignment := by grind theorem removeNeg_addNeg_cancel {assignment : Assignment} (h : ¬(hasNegAssignment assignment)) : - removeNegAssignment (addNegAssignment assignment) = assignment := by - cases assignment <;> simp_all [removeNegAssignment, addNegAssignment, hasNegAssignment] + removeNegAssignment (addNegAssignment assignment) = assignment := by grind theorem remove_add_cancel {assignment : Assignment} {b : Bool} (h : ¬(hasAssignment b assignment)) : - removeAssignment b (addAssignment b assignment) = assignment := by - by_cases hb : b - · simp only [removeAssignment, hb, addAssignment, ite_true] - simp only [hasAssignment, hb, ite_true] at h - exact removePos_addPos_cancel h - · simp only [removeAssignment, hb, addAssignment, ite_true] - simp only [hasAssignment, hb, ite_false] at h - exact removeNeg_addNeg_cancel h + removeAssignment b (addAssignment b assignment) = assignment := by grind -theorem add_both_eq_both (b : Bool) : addAssignment b both = both := by - rw [addAssignment] - split <;> decide +theorem add_both_eq_both (b : Bool) : addAssignment b both = both := by grind -theorem has_both (b : Bool) : hasAssignment b both = true := by - rw [hasAssignment] - split <;> decide +theorem has_both (b : Bool) : hasAssignment b both = true := by grind theorem has_add (assignment : Assignment) (b : Bool) : - hasAssignment b (addAssignment b assignment) := by - by_cases b <;> cases assignment <;> simp_all [hasAssignment, hasPosAssignment, addAssignment, - addPosAssignment, addNegAssignment, hasNegAssignment] + hasAssignment b (addAssignment b assignment) := by grind theorem not_hasPos_removePos (assignment : Assignment) : - ¬hasPosAssignment (removePosAssignment assignment) := by - cases assignment <;> simp [removePosAssignment, hasPosAssignment] + ¬hasPosAssignment (removePosAssignment assignment) := by grind theorem not_hasNeg_removeNeg (assignment : Assignment) : - ¬hasNegAssignment (removeNegAssignment assignment) := by - cases assignment <;> simp [removeNegAssignment, hasNegAssignment] + ¬hasNegAssignment (removeNegAssignment assignment) := by grind theorem not_has_remove (assignment : Assignment) (b : Bool) : - ¬hasAssignment b (removeAssignment b assignment) := by - by_cases b <;> cases assignment <;> simp_all [hasAssignment, removeAssignment, - removePosAssignment, hasPosAssignment, removeNegAssignment, hasNegAssignment] + ¬hasAssignment b (removeAssignment b assignment) := by grind theorem has_remove_irrelevant (assignment : Assignment) (b : Bool) : - hasAssignment b (removeAssignment (!b) assignment) → hasAssignment b assignment := by - by_cases hb : b - · simp only [hb, removeAssignment, Bool.not_true, ite_false, hasAssignment, ite_true] - cases assignment <;> decide - · simp only [Bool.not_eq_true] at hb - simp only [hb, removeAssignment, Bool.not_true, ite_false, hasAssignment, ite_true] - cases assignment <;> decide + hasAssignment b (removeAssignment (!b) assignment) → hasAssignment b assignment := by grind theorem unassigned_of_has_neither (assignment : Assignment) (lacks_pos : ¬(hasPosAssignment assignment)) (lacks_neg : ¬(hasNegAssignment assignment)) : - assignment = unassigned := by - simp only [hasPosAssignment, Bool.not_eq_true] at lacks_pos - split at lacks_pos <;> simp_all +decide + assignment = unassigned := by grind +@[local grind =] theorem hasPos_addNeg (assignment : Assignment) : - hasPosAssignment (addNegAssignment assignment) = hasPosAssignment assignment := by - cases assignment <;> simp [hasPosAssignment, addNegAssignment] + hasPosAssignment (addNegAssignment assignment) = hasPosAssignment assignment := by grind +@[local grind =] theorem hasNeg_addPos (assignment : Assignment) : - hasNegAssignment (addPosAssignment assignment) = hasNegAssignment assignment := by - cases assignment <;> simp [hasNegAssignment, addPosAssignment] + hasNegAssignment (addPosAssignment assignment) = hasNegAssignment assignment := by grind theorem has_iff_has_add_complement (assignment : Assignment) (b : Bool) : - hasAssignment b assignment ↔ hasAssignment b (addAssignment (¬b) assignment) := by - by_cases hb : b <;> simp [hb, hasAssignment, addAssignment, hasPos_addNeg, hasNeg_addPos] + hasAssignment b assignment ↔ hasAssignment b (addAssignment (¬b) assignment) := by grind theorem addPos_addNeg_eq_both (assignment : Assignment) : - addPosAssignment (addNegAssignment assignment) = both := by - cases assignment <;> simp [addPosAssignment, addNegAssignment] + addPosAssignment (addNegAssignment assignment) = both := by grind theorem addNeg_addPos_eq_both (assignment : Assignment) : - addNegAssignment (addPosAssignment assignment) = both := by - cases assignment <;> simp [addNegAssignment, addPosAssignment] + addNegAssignment (addPosAssignment assignment) = both := by grind instance {n : Nat} : Entails (PosFin n) (Array Assignment) where eval := fun p arr => ∀ i : PosFin n, ¬(hasAssignment (¬p i) arr[i.1]!) diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/CNF.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/CNF.lean index c56dab9d05..b820087579 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/CNF.lean +++ b/src/Std/Tactic/BVDecide/LRAT/Internal/CNF.lean @@ -6,6 +6,8 @@ Authors: Josh Clune prelude import Std.Tactic.BVDecide.LRAT.Internal.Formula.Class +set_option grind.warning false + namespace Std.Tactic.BVDecide namespace LRAT namespace Internal @@ -14,18 +16,10 @@ open Clause Formula Std Sat namespace Literal -theorem sat_iff (p : α → Bool) (a : α) (b : Bool) : p ⊨ (a, b) ↔ (p a) = b := by - simp only [Entails.eval] +theorem sat_iff (p : α → Bool) (a : α) (b : Bool) : p ⊨ (a, b) ↔ (p a) = b := Iff.rfl theorem sat_negate_iff_not_sat {p : α → Bool} {l : Literal α} : p ⊨ Literal.negate l ↔ p ⊭ l := by - simp only [Literal.negate, sat_iff] - constructor - · intro h pl - rw [sat_iff, h] at pl - simp at pl - · intro h - rw [sat_iff] at h - cases h : p l.fst <;> simp_all + grind [sat_iff, cases Bool] theorem unsat_of_limplies_complement [Entails α t] (x : t) (l : Literal α) : Limplies α x l → Limplies α x (Literal.negate l) → Unsatisfiable α x := by @@ -41,61 +35,25 @@ namespace Clause theorem sat_iff_exists [Clause α β] (p : α → Bool) (c : β) : p ⊨ c ↔ ∃ l ∈ toList c, p ⊨ l := by simp only [(· ⊨ ·), eval] - simp only [List.any_eq_true, decide_eq_true_eq, Prod.exists, Bool.exists_bool] + grind theorem limplies_iff_mem [DecidableEq α] [Clause α β] (l : Literal α) (c : β) : Limplies α l c ↔ l ∈ toList c := by simp only [Limplies, sat_iff_exists, Prod.exists, Bool.exists_bool] constructor - · intro h + · simp only [(· ⊨ ·)] + intro h -- Construct an assignment p such that p ⊨ l and p ⊭ c ∖ {l} let p := fun x : α => if x = l.1 then l.2 else (x, false) ∈ toList c - have pl : p ⊨ l := by simp only [(· ⊨ ·), ite_true, p] - specialize h p pl - rcases h with ⟨v, ⟨h1, h2⟩ | ⟨h1, h2⟩⟩ - · simp only [(· ⊨ ·), p] at h2 - split at h2 - · next v_eq_l => - cases l - simp_all - · next v_ne_l => - simp only [decide_eq_false_iff_not] at h2 - exfalso - exact h2 h1 - · simp only [(· ⊨ ·), p] at h2 - split at h2 - · next v_eq_l => - cases l - simp_all - · next v_ne_l => - simp only [decide_eq_true_eq] at h2 - exfalso - rcases not_tautology c (v, true) with v_not_in_c | negv_not_in_c - · exact v_not_in_c h1 - · simp only [Literal.negate, Bool.not_true] at negv_not_in_c - exact negv_not_in_c h2 - · intro h p pl - apply Exists.intro l.1 - by_cases hl : l.2 - · apply Or.inr - rw [← hl] - exact ⟨h, pl⟩ - · apply Or.inl - simp only [Bool.not_eq_true] at hl - rw [← hl] - exact ⟨h, pl⟩ + specialize h p + grind [not_tautology] + · grind [cases Bool] theorem entails_of_entails_delete [DecidableEq α] [Clause α β] {p : α → Bool} {c : β} {l : Literal α} : p ⊨ delete c l → p ⊨ c := by - intro h - simp only [(· ⊨ ·), eval, List.any_eq_true, decide_eq_true_eq, Prod.exists, Bool.exists_bool] at h - simp only [(· ⊨ ·), eval, List.any_eq_true, decide_eq_true_eq, Prod.exists, Bool.exists_bool] - rcases h with ⟨v, ⟨h1, h2⟩ | ⟨h1, h2⟩⟩ - · simp only [delete_iff, ne_eq] at h1 - exact Exists.intro v <| Or.inl ⟨h1.2, h2⟩ - · simp only [delete_iff, ne_eq] at h1 - exact Exists.intro v <| Or.inr ⟨h1.2, h2⟩ + simp only [(· ⊨ ·), eval] at ⊢ + grind end Clause @@ -103,27 +61,18 @@ namespace Formula theorem sat_iff_forall [Clause α β] [Entails α σ] [Formula α β σ] (p : α → Bool) (f : σ) : p ⊨ f ↔ ∀ c : β, c ∈ toList f → p ⊨ c := by - simp only [(· ⊨ ·), formulaEntails_def p f] - simp only [List.all_eq_true, decide_eq_true_eq] + simp only [formulaEntails_def] + grind theorem limplies_insert [Clause α β] [Entails α σ] [Formula α β σ] {c : β} {f : σ} : Limplies α (insert f c) f := by - intro p - simp only [formulaEntails_def, List.all_eq_true, decide_eq_true_eq] - intro h c' c'_in_f - have c'_in_fc : c' ∈ toList (insert f c) := by - simp only [insert_iff, List.toList_toArray, List.mem_singleton] - exact Or.inr c'_in_f - exact h c' c'_in_fc + simp only [Limplies, formulaEntails_def] + grind theorem limplies_delete [Clause α β] [Entails α σ] [Formula α β σ] {f : σ} {arr : Array Nat} : Limplies α f (delete f arr) := by - intro p - simp only [formulaEntails_def, List.all_eq_true, decide_eq_true_eq] - intro h c c_in_f_del - have del_f_subset := delete_subset f arr - specialize del_f_subset c c_in_f_del - exact h c del_f_subset + simp only [Limplies, formulaEntails_def] + grind end Formula diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Clause.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Clause.lean index 3b323056d2..bc26be37ef 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Clause.lean +++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Clause.lean @@ -10,7 +10,9 @@ import Std.Data.HashMap import Std.Sat.CNF.Basic import Std.Tactic.BVDecide.LRAT.Internal.PosFin import Std.Tactic.BVDecide.LRAT.Internal.Assignment +import Init.Grind +set_option grind.warning false namespace Std.Tactic.BVDecide namespace LRAT @@ -55,6 +57,8 @@ class Clause (α : outParam (Type u)) (β : Type v) where namespace Clause +attribute [grind] empty_eq unit_eq isUnit_iff negate_eq delete_iff contains_iff + instance : Entails α (Literal α) where eval := fun p l => p l.1 = l.2 @@ -89,8 +93,8 @@ that it was needed. -/ @[ext] structure DefaultClause (numVarsSucc : Nat) where clause : CNF.Clause (PosFin numVarsSucc) - nodupkey : ∀ l : PosFin numVarsSucc, (l, true) ∉ clause ∨ (l, false) ∉ clause - nodup : List.Nodup clause + nodupkey : ∀ l : PosFin numVarsSucc, (l, true) ∉ clause ∨ (l, false) ∉ clause := by grind + nodup : List.Nodup clause := by grind deriving BEq instance : ToString (DefaultClause n) where @@ -98,45 +102,23 @@ instance : ToString (DefaultClause n) where namespace DefaultClause -def toList (c : DefaultClause n) : CNF.Clause (PosFin n) := c.clause +@[grind] def toList (c : DefaultClause n) : CNF.Clause (PosFin n) := c.clause + +attribute [local grind] DefaultClause.nodup DefaultClause.nodupkey theorem not_tautology (c : DefaultClause n) (l : Literal (PosFin n)) : l ∉ toList c ∨ ¬Literal.negate l ∈ toList c := by - simp only [toList, Literal.negate] - have h := c.nodupkey l.1 - by_cases hl : l.2 - · simp only [hl, Bool.not_true] - rwa [← hl] at h - · simp only [Bool.not_eq_true] at hl - simp only [hl, Bool.not_false] - apply Or.symm - rwa [← hl] at h + grind [cases Bool] @[inline] -def empty : DefaultClause n := - let clause := [] - have nodupkey := by - simp only [clause, List.find?, List.not_mem_nil, not_false_eq_true, or_self, implies_true] - have nodup := by - simp only [clause, List.nodup_nil] - ⟨clause, nodupkey, nodup⟩ +def empty : DefaultClause n where + clause := [] theorem empty_eq : toList (empty : DefaultClause n) = [] := rfl @[inline] -def unit (l : Literal (PosFin n)) : DefaultClause n := - let clause := [l] - have nodupkey : ∀ (l : PosFin n), ¬(l, true) ∈ clause ∨ ¬(l, false) ∈ clause := by - intro l' - by_cases l.2 - · apply Or.inr - cases l - simp_all [clause] - · apply Or.inl - cases l - simp_all [clause] - have nodup : List.Nodup clause:= by simp [clause] - ⟨clause, nodupkey, nodup⟩ +def unit (l : Literal (PosFin n)) : DefaultClause n where + clause := [l] theorem unit_eq (l : Literal (PosFin n)) : toList (unit l) = [l] := rfl @@ -148,54 +130,14 @@ def isUnit (c : DefaultClause n) : Option (Literal (PosFin n)) := theorem isUnit_iff (c : DefaultClause n) (l : Literal (PosFin n)) : isUnit c = some l ↔ toList c = [l] := by - simp only [isUnit, toList] - split - · next l' heq => simp [heq] - · next hne => - simp - apply hne + grind [isUnit] @[inline] def negate (c : DefaultClause n) : CNF.Clause (PosFin n) := c.clause.map Literal.negate theorem negate_eq (c : DefaultClause n) : negate c = (toList c).map Literal.negate := rfl -def ofArray (ls : Array (Literal (PosFin n))) : Option (DefaultClause n) := - let mapOption := ls.foldl folder (some (HashMap.emptyWithCapacity ls.size)) - match mapOption with - | none => none - | some map => - have mapnodup := map.distinct_keys - have nodupkey : ∀ (l : PosFin n), ¬(l, true) ∈ map.toList ∨ ¬(l, false) ∈ map.toList := by - intro l - apply Classical.byContradiction - simp_all - have nodup : map.toList.Nodup := by - rw [List.Nodup, List.pairwise_iff_forall_sublist] - simp only [ne_eq, Prod.forall, Bool.forall_bool, Prod.mk.injEq, not_and, Bool.not_eq_false, - Bool.not_eq_true, Bool.false_eq_true, imp_false, implies_true, and_true, Bool.true_eq_false, - true_and] - intro l1 - constructor - . intros l2 h hl - rw [List.pairwise_iff_forall_sublist] at mapnodup - replace h : [l1, l2].Sublist map.keys := by - rw [← HashMap.map_fst_toList_eq_keys, List.sublist_map_iff] - apply Exists.intro [(l1, false), (l2, false)] - simp [h] - specialize mapnodup h - simp [hl] at mapnodup - . intros l2 h hl - rw [List.pairwise_iff_forall_sublist] at mapnodup - replace h : [l1, l2].Sublist map.keys := by - rw [← HashMap.map_fst_toList_eq_keys, List.sublist_map_iff] - apply Exists.intro [(l1, true), (l2, true)] - simp [h] - specialize mapnodup h - simp [hl] at mapnodup - some ⟨map.toList, nodupkey, nodup⟩ -where - folder (acc : Option (Std.HashMap (PosFin n) Bool)) (l : Literal (PosFin n)) : +@[irreducible] def ofArray.folder (acc : Option (Std.HashMap (PosFin n) Bool)) (l : Literal (PosFin n)) : Option (Std.HashMap (PosFin n) Bool) := match acc with | none => none @@ -209,119 +151,58 @@ where else some map +-- Recall `@[local grind]` doesn't work for theorems in namespaces, +-- so we add the attribute after the fact. +attribute [local grind] DefaultClause.ofArray.folder + +def ofArray (ls : Array (Literal (PosFin n))) : Option (DefaultClause n) := + let mapOption := ls.foldl ofArray.folder (some (HashMap.emptyWithCapacity ls.size)) + match mapOption with + | none => none + | some map => + -- FIXME: Commenting this out gives an unknown metavariable error in `grind`! + -- reported as https://github.com/leanprover/lean4/pull/8607 + have mapnodup := map.distinct_keys + some ⟨map.toList, by grind, by grind⟩ + @[simp] theorem ofArray.foldl_folder_none_eq_none : List.foldl ofArray.folder none ls = none := by - apply List.foldlRecOn (motive := (· = none)) - · simp - · intro b hb a ha - unfold DefaultClause.ofArray.folder - simp [hb] + apply List.foldlRecOn (motive := (· = none)) <;> grind + +attribute [local grind] ofArray.foldl_folder_none_eq_none theorem ofArray.mem_of_mem_of_foldl_folder_eq_some - (h : List.foldl DefaultClause.ofArray.folder (some acc) ls = some acc') : - ∀ l ∈ acc.toList, l ∈ acc'.toList := by - intro l hl - induction ls generalizing acc with - | nil => simp_all - | cons x xs ih => - rcases l with ⟨var, pol⟩ - rw [List.foldl_cons, DefaultClause.ofArray.folder.eq_def] at h - split at h - · contradiction - · simp only [HashMap.getThenInsertIfNew?_fst, HashMap.get?_eq_getElem?, bne_iff_ne, ne_eq, - HashMap.getThenInsertIfNew?_snd, ite_not] at h - split at h - · split at h - · apply ih - · exact h - · rw [Std.HashMap.mem_toList_iff_getElem?_eq_some, Std.HashMap.getElem?_insertIfNew] - rename_i map _ _ _ _ _ - have : x.fst ∈ map := by - apply Classical.byContradiction - intro h2 - have := Std.HashMap.getElem?_eq_none h2 - simp_all - simp [this] - rw [Std.HashMap.mem_toList_iff_getElem?_eq_some] at hl - simp_all - · simp at h - · apply ih - · exact h - · rw [Std.HashMap.mem_toList_iff_getElem?_eq_some, Std.HashMap.getElem?_insertIfNew] - simp_all - intros - cases pol <;> simp_all + (h : List.foldl DefaultClause.ofArray.folder (some acc) ls = some acc') (l) (h : l ∈ acc.toList) : + l ∈ acc'.toList := by + induction ls generalizing acc with grind (gen := 7) + +attribute [local grind] ofArray.mem_of_mem_of_foldl_folder_eq_some theorem ofArray.folder_foldl_mem_of_mem (h : List.foldl DefaultClause.ofArray.folder acc ls = some map) : ∀ l ∈ ls, l ∈ map.toList := by intro l hl induction ls generalizing acc with - | nil => simp at hl + | nil => grind | cons x xs ih => simp at hl h - rcases hl with hl | hl - · rw [DefaultClause.ofArray.folder.eq_def] at h - simp at h - split at h - · simp at h - · split at h - · split at h - · apply mem_of_mem_of_foldl_folder_eq_some - · exact h - · rw [Std.HashMap.mem_toList_iff_getElem?_eq_some] - rw [Std.HashMap.getElem?_insertIfNew] - simp_all - · simp at h - · apply mem_of_mem_of_foldl_folder_eq_some - · exact h - · next hfoo => - rw [hl] - cases x - simp [Std.HashMap.getElem_insertIfNew] - intro hbar - exfalso - apply hfoo - rw [Std.HashMap.getElem?_eq_some_getElem! hbar] - · exact ih h hl + rw [DefaultClause.ofArray.folder.eq_def] at h -- TODO why doesn't `grind` handle this? + rcases hl <;> grind (gen := 7) -@[inline] -def delete (c : DefaultClause n) (l : Literal (PosFin n)) : DefaultClause n := - let clause := c.clause.erase l - let nodupkey : ∀ (l : PosFin n), ¬(l, true) ∈ clause ∨ ¬(l, false) ∈ clause := by - intro l' - simp only [clause] - rcases c.nodupkey l' with ih | ih - · apply Or.inl - intro h - exact ih <| List.mem_of_mem_erase h - · apply Or.inr - intro h - exact ih <| List.mem_of_mem_erase h - have nodup := by - simp only [clause] - exact List.Nodup.erase l c.nodup - ⟨clause, nodupkey, nodup⟩ +@[inline, local grind] +def delete (c : DefaultClause n) (l : Literal (PosFin n)) : DefaultClause n where + clause := c.clause.erase l theorem delete_iff (c : DefaultClause n) (l l' : Literal (PosFin n)) : l' ∈ toList (delete c l) ↔ l' ≠ l ∧ l' ∈ toList c := by - simp only [toList, delete, ne_eq] - by_cases hl : l' = l - · simp only [hl, not_true, false_and, iff_false] - exact List.Nodup.not_mem_erase c.nodup - · simp only [hl, not_false_eq_true, true_and] - exact List.mem_erase_of_ne hl + grind @[inline] def contains (c : DefaultClause n) (l : Literal (PosFin n)) : Bool := c.clause.contains l theorem contains_iff : ∀ (c : DefaultClause n) (l : Literal (PosFin n)), contains c l = true ↔ l ∈ toList c := by - intro c l - simp only [contains, List.contains] - constructor - · exact List.mem_of_elem_eq_true - · exact List.elem_eq_true_of_mem + grind [contains] def reduce_fold_fn (assignments : Array Assignment) (acc : ReduceResult (PosFin n)) (l : Literal (PosFin n)) : diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Convert.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Convert.lean index 427a3f876b..5c413aa923 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Convert.lean +++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Convert.lean @@ -111,7 +111,7 @@ theorem unsat_of_cons_none_unsat (clauses : List (Option (DefaultClause n))) : apply h assign simp only [Formula.formulaEntails_def, List.all_eq_true, decide_eq_true_eq] at * intro clause hclause - simp_all[DefaultFormula.ofArray, Formula.toList, DefaultFormula.toList] + simp_all [DefaultFormula.ofArray, Formula.toList, DefaultFormula.toList] theorem CNF.unsat_of_convertLRAT_unsat (cnf : CNF Nat) : Unsatisfiable (PosFin (cnf.numLiterals + 1)) (CNF.convertLRAT cnf) diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Class.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Class.lean index b2023e4a70..57ef1abfcd 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Class.lean +++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Class.lean @@ -56,6 +56,14 @@ class Formula (α : outParam (Type u)) (β : outParam (Type v)) [Clause α β] ( ∀ f : σ, ∀ c : β, ∀ p : Literal α, ∀ rupHints : Array Nat, ∀ ratHints : Array (Nat × Array Nat), ∀ f' : σ, ReadyForRatAdd f → p ∈ Clause.toList c → performRatAdd f c p rupHints ratHints = (f', true) → Equisat α f f' +open Formula + +attribute [grind] insert_iff readyForRupAdd_insert readyForRatAdd_insert + delete_subset readyForRupAdd_delete readyForRatAdd_delete + +attribute [grind →] + rupAdd_result rupAdd_sound ratAdd_result ratAdd_sound + end Internal end LRAT end Std.Tactic.BVDecide diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean index 9fa10b47cf..3dfdbdc534 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean +++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean @@ -7,6 +7,8 @@ prelude import Std.Tactic.BVDecide.LRAT.Internal.Formula.Implementation import Std.Tactic.BVDecide.LRAT.Internal.CNF +set_option grind.warning false -- I've only made a partial effort to use grind here so far. + /-! This module contains basic statements about the invariants that are satisfied by the LRAT checker implementation in `Implementation`. @@ -21,6 +23,8 @@ namespace DefaultFormula open Std.Sat open DefaultClause DefaultFormula Assignment +attribute [local grind] insert ofArray + /-- This invariant states that if the `assignments` field of a default formula `f` indicates that `f` contains an assignment `b` at index `i`, then the unit literal `(i, b)` must be included in `f`. @@ -86,25 +90,23 @@ def ReadyForRatAdd {n : Nat} (f : DefaultFormula n) : Prop := f.ratUnits = #[] theorem rupUnits_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) : (insert f c).rupUnits = f.rupUnits := by simp only [insert] - split <;> simp only + grind theorem ratUnits_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) : (insert f c).ratUnits = f.ratUnits := by simp only [insert] - split <;> simp only + grind theorem size_ofArray_fold_fn {n : Nat} (assignments : Array Assignment) (cOpt : Option (DefaultClause n)) : (ofArray_fold_fn assignments cOpt).size = assignments.size := by rw [ofArray_fold_fn.eq_def] - split - · rfl - · split <;> simp [Array.size_modify] + grind theorem readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n))) : ReadyForRupAdd (ofArray arr) := by constructor - · simp only [ofArray] + · grind · have hsize : (ofArray arr).assignments.size = n := by simp only [ofArray, ← Array.foldl_toList] have hb : (Array.replicate n unassigned).size = n := by simp only [Array.size_replicate] @@ -148,8 +150,7 @@ theorem readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n)) simp only [unit, b_eq_true, i_eq_l] have c_def : c = ⟨c.clause, c.nodupkey, c.nodup⟩ := rfl simp only [heq] at c_def - rw [c_def] at cOpt_in_arr - exact cOpt_in_arr + grind · next b_eq_false => simp only [Bool.not_eq_true] at b_eq_false simp only [hasAssignment, b_eq_false, ite_false, hasNeg_addPos, reduceCtorEq] at h @@ -157,9 +158,7 @@ theorem readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n)) simp only [hasAssignment, ite_false] at ih rw [b_eq_false, Subtype.ext i_eq_l] exact ih h - · next i_ne_l => - simp only [Array.getElem_modify_of_ne (Ne.symm i_ne_l)] at h - exact ih i b h + · next i_ne_l => grind | some (l, false) => simp only [heq] at h rcases ih with ⟨hsize, ih⟩ @@ -172,7 +171,7 @@ theorem readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n)) specialize ih l true simp only [hasAssignment, ite_false] at ih rw [b_eq_true, Subtype.ext i_eq_l] - exact ih h + grind · next b_eq_false => rw [isUnit_iff, DefaultClause.toList] at heq simp only [toList, ofArray, List.map, List.append_nil, List.mem_filterMap, id_eq, exists_eq_right] @@ -180,80 +179,32 @@ theorem readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n)) simp only [unit, b_eq_false, i_eq_l] have c_def : c = ⟨c.clause, c.nodupkey, c.nodup⟩ := rfl simp only [heq] at c_def - rw [c_def] at cOpt_in_arr - exact cOpt_in_arr - · next i_ne_l => - simp only [Array.getElem_modify_of_ne (Ne.symm i_ne_l)] at h - exact ih i b h + grind + · next i_ne_l => grind rcases List.foldlRecOn arr.toList ofArray_fold_fn hb hl with ⟨_h_size, h'⟩ - intro i b h - simp only [ofArray, ← Array.foldl_toList] at h - exact h' i b h + grind [ofArray] theorem readyForRatAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n))) : ReadyForRatAdd (ofArray arr) := by constructor - · simp only [ofArray] - · exact readyForRupAdd_ofArray arr + · grind + · grind [readyForRupAdd_ofArray] theorem insert_iff {n : Nat} (f : DefaultFormula n) (c1 : DefaultClause n) (c2 : DefaultClause n) : c2 ∈ toList (insert f c1) ↔ c2 = c1 ∨ c2 ∈ toList f := by - simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq, exists_eq_right, - List.mem_map, Prod.exists, Bool.exists_bool] - by_cases c2 = c1 - · next c2_eq_c1 => - constructor - · intro _ - exact Or.inl c2_eq_c1 - · intro _ - apply Or.inl - simp only [c2_eq_c1, insert] - split <;> simp - · next c2_ne_c1 => - constructor - · intro h - apply Or.inr - rcases h with h | h | h - · apply Or.inl - simp only [insert] at h - split at h - all_goals - simp only [Array.toList_push, List.mem_append, List.mem_singleton, Option.some.injEq] at h - rcases h with h | h - · exact h - · exact False.elim <| c2_ne_c1 h - · rw [rupUnits_insert] at h - exact Or.inr <| Or.inl h - · rw [ratUnits_insert] at h - exact Or.inr <| Or.inr h - · intro h - rcases h with h | h | h | h - · exact False.elim <| c2_ne_c1 h - · apply Or.inl - simp only [insert] - split - all_goals - simp only [Array.toList_push, List.mem_append, List.mem_singleton, Option.some.injEq] - exact Or.inl h - · rw [rupUnits_insert] - exact Or.inr <| Or.inl h - · rw [ratUnits_insert] - exact Or.inr <| Or.inr h + simp only [toList, List.mem_append, List.mem_filterMap, id_eq, exists_eq_right] + simp only [insert] + grind theorem limplies_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) : Limplies (PosFin n) (insert f c) f := by - intro p - simp only [formulaEntails_def, List.all_eq_true, decide_eq_true_eq] - intro h c' c'_in_f - have c'_in_fc : c' ∈ toList (insert f c) := by - simp only [insert_iff, List.toList_toArray, List.mem_singleton] - exact Or.inr c'_in_f - exact h c' c'_in_fc + simp only [Limplies, formulaEntails_def, List.all_eq_true] + grind [insert_iff] theorem size_assignments_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) : (insert f c).assignments.size = f.assignments.size := by simp only [insert] - split <;> simp only [Array.size_modify] + grind theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) : ReadyForRupAdd f → ReadyForRupAdd (insert f c) := by @@ -263,13 +214,8 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus · refine ⟨f_readyForRupAdd.1, f_readyForRupAdd.2.1, ?_⟩ intro i b hb have hf := f_readyForRupAdd.2.2 i b hb - simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq, exists_eq_right, - List.mem_map, Prod.exists, Bool.exists_bool] at hf - simp only [toList, Array.toList_push, List.append_assoc, List.mem_append, List.mem_filterMap, - List.mem_singleton, id_eq, exists_eq_right, Option.some.injEq, List.mem_map, Prod.exists, Bool.exists_bool] - rcases hf with hf | hf - · exact (Or.inl ∘ Or.inl) hf - · exact Or.inr hf + simp only [toList] at hf ⊢ + grind · next l hc => have hsize : (Array.modify f.assignments l.1 addPosAssignment).size = n := by rw [Array.size_modify, f_readyForRupAdd.2.1] @@ -294,22 +240,13 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus by_cases b = true · next b_eq_true => simp only [b_eq_true, Subtype.ext l_eq_i, not_true] at ib_ne_c - · next b_eq_false => - simp only [Bool.not_eq_true] at b_eq_false - exact b_eq_false + · next b_eq_false => grind simp only [hasAssignment, b_eq_false, l_eq_i, Array.getElem_modify_self, ite_false, hasNeg_addPos, reduceCtorEq] at hb - simp only [hasAssignment, b_eq_false, ite_false, hb, reduceCtorEq] - · next l_ne_i => - simp only [Array.getElem_modify_of_ne l_ne_i] at hb - exact hb + grind [hasAssignment] + · next l_ne_i => grind specialize hf hb' - simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq, - exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool] at hf - simp only [toList, Array.toList_push, List.append_assoc, List.mem_append, List.mem_filterMap, - List.mem_singleton, id_eq, exists_eq_right, Option.some.injEq, List.mem_map, Prod.exists, Bool.exists_bool] - rcases hf with hf | hf - · exact Or.inl <| Or.inl hf - · exact Or.inr hf + simp only [toList] at hf ⊢ + grind · next l hc => have hsize : (Array.modify f.assignments l.1 addNegAssignment).size = n := by rw [Array.size_modify, f_readyForRupAdd.2.1] @@ -335,25 +272,18 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus · assumption · next b_eq_false => simp only [b_eq_false, Subtype.ext l_eq_i, not_true] at ib_ne_c - simp only [hasAssignment, b_eq_false, l_eq_i, Array.getElem_modify_self, ite_true, hasPos_addNeg] at hb - simp only [hasAssignment, b_eq_false, ite_true, hb] - · next l_ne_i => - simp only [Array.getElem_modify_of_ne l_ne_i] at hb - exact hb + grind [hasAssignment, hasPos_addNeg] + · next l_ne_i => grind specialize hf hb' - simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq, - exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool] at hf - simp only [toList, Array.toList_push, List.append_assoc, List.mem_append, List.mem_filterMap, - List.mem_singleton, id_eq, exists_eq_right, Option.some.injEq, List.mem_map, Prod.exists, Bool.exists_bool] - rcases hf with hf | hf - · exact Or.inl <| Or.inl hf - · exact Or.inr hf + simp only [toList] at hf ⊢ + grind theorem readyForRatAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) : ReadyForRatAdd f → ReadyForRatAdd (insert f c) := by intro h constructor - · simp only [insert, h.1] <;> split <;> rfl + · simp only [insert, h.1] + grind · exact readyForRupAdd_insert f c h.2 theorem mem_of_insertRupUnits {n : Nat} (f : DefaultFormula n) (units : CNF.Clause (PosFin n)) @@ -363,36 +293,27 @@ theorem mem_of_insertRupUnits {n : Nat} (f : DefaultFormula n) (units : CNF.Clau List.mem_filterMap, id_eq, exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool] intro h have hb : ∀ l : Literal (PosFin n), l ∈ (f.rupUnits, f.assignments, false).1.toList → (l ∈ f.rupUnits.toList ∨ l ∈ units) := by - intro l hl - exact Or.inl hl + grind have hl (acc : Array (Literal (PosFin n)) × Array Assignment × Bool) (ih : ∀ l : Literal (PosFin n), l ∈ acc.1.toList → l ∈ f.rupUnits.toList ∨ l ∈ units) (unit : Literal (PosFin n)) (unit_in_units : unit ∈ units) : ∀ l : Literal (PosFin n), l ∈ (insertUnit acc unit).1.toList → (l ∈ f.rupUnits.toList ∨ l ∈ units) := by intro l hl rw [insertUnit.eq_def] at hl - dsimp at hl - split at hl - · exact ih l hl - · simp only [Array.toList_push, List.mem_append, List.mem_singleton] at hl - rcases hl with l_in_acc | l_eq_unit - · exact ih l l_in_acc - · rw [l_eq_unit] - exact Or.inr unit_in_units + grind have h_insertUnit_fold := List.foldlRecOn units insertUnit hb hl rcases h with h | ⟨i, ⟨h1, h2⟩ | ⟨h1, h2⟩⟩ | h - · exact Or.inr <| Or.inl h + · grind · rcases h_insertUnit_fold (i, false) h1 with h_insertUnit_fold | h_insertUnit_fold · apply Or.inr ∘ Or.inr ∘ Or.inl ∘ Exists.intro i ∘ Or.inl - exact ⟨h_insertUnit_fold, h2⟩ + grind · apply Or.inl ∘ Exists.intro i ∘ Or.inl - exact ⟨h_insertUnit_fold, h2⟩ + exact ⟨by grind, h2⟩ · rcases h_insertUnit_fold (i, true) h1 with h_insertUnit_fold | h_insertUnit_fold - · apply Or.inr ∘ Or.inr ∘ Or.inl ∘ Exists.intro i ∘ Or.inr - exact ⟨h_insertUnit_fold, h2⟩ + · grind · apply Or.inl ∘ Exists.intro i ∘ Or.inr - exact ⟨h_insertUnit_fold, h2⟩ - · exact (Or.inr ∘ Or.inr ∘ Or.inr) h + exact ⟨by grind, h2⟩ + · grind theorem mem_of_insertRatUnits {n : Nat} (f : DefaultFormula n) (units : CNF.Clause (PosFin n)) (c : DefaultClause n) : @@ -406,40 +327,29 @@ theorem mem_of_insertRatUnits {n : Nat} (f : DefaultFormula n) (units : CNF.Clau (ih : ∀ l : Literal (PosFin n), l ∈ acc.1.toList → l ∈ f.ratUnits.toList ∨ l ∈ units) (unit : Literal (PosFin n)) (unit_in_units : unit ∈ units) : ∀ l : Literal (PosFin n), l ∈ (insertUnit acc unit).1.toList → (l ∈ f.ratUnits.toList ∨ l ∈ units) := by - intro l hl - rw [insertUnit.eq_def] at hl - dsimp at hl - split at hl - · exact ih l hl - · simp only [Array.toList_push, List.mem_append, List.mem_singleton] at hl - rcases hl with l_in_acc | l_eq_unit - · exact ih l l_in_acc - · rw [l_eq_unit] - exact Or.inr unit_in_units + grind [insertUnit] have h_insertUnit_fold := List.foldlRecOn units insertUnit hb hl rcases h with h | h | ⟨i, ⟨h1, h2⟩ | ⟨h1, h2⟩⟩ - · exact Or.inr <| Or.inl h - · exact (Or.inr ∘ Or.inr ∘ Or.inl) h + · grind + · grind · rcases h_insertUnit_fold (i, false) h1 with h_insertUnit_fold | h_insertUnit_fold - · apply Or.inr ∘ Or.inr ∘ Or.inr ∘ Exists.intro i ∘ Or.inl - exact ⟨h_insertUnit_fold, h2⟩ + · grind · apply Or.inl ∘ Exists.intro i ∘ Or.inl exact ⟨h_insertUnit_fold, h2⟩ · rcases h_insertUnit_fold (i, true) h1 with h_insertUnit_fold | h_insertUnit_fold - · apply Or.inr ∘ Or.inr ∘ Or.inr ∘ Exists.intro i ∘ Or.inr - exact ⟨h_insertUnit_fold, h2⟩ + · grind · apply Or.inl ∘ Exists.intro i ∘ Or.inr exact ⟨h_insertUnit_fold, h2⟩ theorem deleteOne_preserves_rupUnits {n : Nat} (f : DefaultFormula n) (id : Nat) : (deleteOne f id).rupUnits = f.rupUnits := by simp only [deleteOne] - split <;> simp only + grind theorem deleteOne_preserves_assignments_size {n : Nat} (f : DefaultFormula n) (id : Nat) : (deleteOne f id).assignments.size = f.assignments.size := by simp only [deleteOne] - split <;> simp only [Array.size_modify] + grind theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFormula n) (id : Nat) : StrongAssignmentsInvariant f → StrongAssignmentsInvariant (deleteOne f id) := by @@ -466,11 +376,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor by_cases l.1.1 = i.1 · next l_eq_i => simp only [l_eq_i, Array.getElem_modify_self] at hb - have l_ne_b : l.2 ≠ b := by - intro l_eq_b - rw [← l_eq_b] at hb - have hb' := not_has_remove f.assignments[i.1] l.2 - simp [hb] at hb' + have l_ne_b : l.2 ≠ b := by grind [not_has_remove] replace l_ne_b := Bool.eq_not_of_ne l_ne_b simp only [l_ne_b] at hb have hb := has_remove_irrelevant f.assignments[i.1] b hb @@ -484,25 +390,10 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor simp only [Array.set!, Array.setIfInBounds] split · rcases List.getElem_of_mem hf with ⟨idx, hbound, hidx⟩ - simp only [← hidx, Array.toList_set] + have idx_in_bounds : idx < List.length (List.set f.clauses.toList id none) := by grind rw [List.mem_iff_get] - have idx_in_bounds : idx < List.length (List.set f.clauses.toList id none) := by - simp only [List.length_set] - exact hbound apply Exists.intro ⟨idx, idx_in_bounds⟩ - by_cases id = idx - · next id_eq_idx => - exfalso - have idx_in_bounds2 : idx < f.clauses.size := by - conv => rhs; rw [List.size_toArray] - exact hbound - simp only [id_eq_idx, getElem!_def, idx_in_bounds2, Array.getElem?_eq_getElem, ← - Array.getElem_toList] at heq - rw [hidx, hl] at heq - simp only [unit, Option.some.injEq, DefaultClause.mk.injEq, List.cons.injEq, and_true] at heq - simp only [← heq] at l_ne_b - simp at l_ne_b - · next id_ne_idx => simp [id_ne_idx] + grind [unit] · exact hf · exact Or.inr hf · next l_ne_i => @@ -517,55 +408,19 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor simp only [Array.set!, Array.setIfInBounds] split · rcases List.getElem_of_mem hf with ⟨idx, hbound, hidx⟩ - simp only [← hidx, Array.toList_set] rw [List.mem_iff_get] - have idx_in_bounds : idx < List.length (List.set f.clauses.toList id none) := by - simp only [List.length_set] - exact hbound + have idx_in_bounds : idx < List.length (List.set f.clauses.toList id none) := by grind apply Exists.intro ⟨idx, idx_in_bounds⟩ - by_cases id = idx - · next id_eq_idx => - exfalso - have idx_in_bounds2 : idx < f.clauses.size := by - conv => rhs; rw [List.size_toArray] - exact hbound - simp only [id_eq_idx, getElem!_def, idx_in_bounds2, Array.getElem?_eq_getElem, ← - Array.getElem_toList] at heq - rw [hidx, hl] at heq - simp only [unit, Option.some.injEq, DefaultClause.mk.injEq, List.cons.injEq, and_true] at heq - have i_eq_l : i = l.1 := by rw [← heq] - simp only [i_eq_l, not_true] at l_ne_i - · next id_ne_idx => simp [id_ne_idx] + grind [unit] · exact hf · exact Or.inr hf · simp only [Prod.exists, Bool.exists_bool, not_exists, not_or, unit] at hl split - · next some_eq_none => - simp at some_eq_none - · next l _ _ heq => - simp only [Option.some.injEq] at heq - rw [heq] at hl - specialize hl l.1 - simp only [DefaultClause.mk.injEq, List.cons.injEq, and_true] at hl - by_cases hl2 : l.2 - · simp only [← hl2, not_true, and_false] at hl - · simp only [Bool.not_eq_true] at hl2 - simp only [← hl2, not_true, false_and] at hl + · next some_eq_none => grind + · next l _ _ heq => grind [cases Bool] · have deleteOne_f_rw : deleteOne f id = ⟨Array.set! f.clauses id none, f.rupUnits, f.ratUnits, f.assignments⟩ := by simp only [deleteOne] - split - · next heq2 => - simp [heq] at heq2 - · next l _ _ heq2 => - simp only [heq, Option.some.injEq] at heq2 - rw [heq2] at hl - specialize hl l.1 - simp only [DefaultClause.mk.injEq, List.cons.injEq, and_true] at hl - by_cases hl2 : l.2 - · simp only [← hl2, not_true, and_false] at hl - · simp only [Bool.not_eq_true] at hl2 - simp only [← hl2, not_true, false_and] at hl - · rfl + grind simp only [deleteOne_f_rw] at hb specialize hf i b hb simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq, @@ -577,28 +432,11 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor simp only [Array.set!, Array.setIfInBounds] split · rcases List.getElem_of_mem hf with ⟨idx, hbound, hidx⟩ - simp only [← hidx, Array.toList_set] rw [List.mem_iff_get] have idx_in_bounds : idx < List.length (List.set f.clauses.toList id none) := by - simp only [List.length_set] - exact hbound + grind apply Exists.intro ⟨idx, idx_in_bounds⟩ - by_cases id = idx - · next id_eq_idx => - exfalso - have idx_in_bounds2 : idx < f.clauses.size := by - conv => rhs; rw [List.size_toArray] - exact hbound - simp only [id_eq_idx, getElem!_def, idx_in_bounds2, Array.getElem?_eq_getElem, ← - Array.getElem_toList] at heq - rw [hidx] at heq - simp only [Option.some.injEq] at heq - rw [← heq] at hl - specialize hl i - simp only [unit, DefaultClause.mk.injEq, List.cons.injEq, Prod.mk.injEq, true_and, and_true, - Bool.not_eq_false, Bool.not_eq_true] at hl - by_cases b_val : b <;> simp [b_val] at hl - · next id_ne_idx => simp [id_ne_idx] + grind [unit] · exact hf · exact Or.inr hf @@ -611,59 +449,38 @@ theorem readyForRupAdd_delete {n : Nat} (f : DefaultFormula n) (arr : Array Nat) have hl (acc : DefaultFormula n) (ih : acc.rupUnits = #[]) (id : Nat) (_id_in_arr : id ∈ arr.toList) : (deleteOne acc id).rupUnits = #[] := by rw [deleteOne_preserves_rupUnits, ih] exact List.foldlRecOn arr.toList deleteOne hb hl - · have hb : StrongAssignmentsInvariant f := h.2 - have hl (acc : DefaultFormula n) (ih : StrongAssignmentsInvariant acc) (id : Nat) (_id_in_arr : id ∈ arr.toList) : + · have hl (acc : DefaultFormula n) (ih : StrongAssignmentsInvariant acc) (id : Nat) (_id_in_arr : id ∈ arr.toList) : StrongAssignmentsInvariant (deleteOne acc id) := deleteOne_preserves_strongAssignmentsInvariant acc id ih - exact List.foldlRecOn arr.toList deleteOne hb hl + exact List.foldlRecOn arr.toList deleteOne h.2 hl theorem deleteOne_preserves_ratUnits {n : Nat} (f : DefaultFormula n) (id : Nat) : (deleteOne f id).ratUnits = f.ratUnits := by simp only [deleteOne] - split <;> simp only + grind theorem readyForRatAdd_delete {n : Nat} (f : DefaultFormula n) (arr : Array Nat) : ReadyForRatAdd f → ReadyForRatAdd (delete f arr) := by intro h constructor · rw [delete, ← Array.foldl_toList] - have hb : f.ratUnits = #[] := h.1 have hl (acc : DefaultFormula n) (ih : acc.ratUnits = #[]) (id : Nat) (_id_in_arr : id ∈ arr.toList) : - (deleteOne acc id).ratUnits = #[] := by rw [deleteOne_preserves_ratUnits, ih] - exact List.foldlRecOn arr.toList deleteOne hb hl + (deleteOne acc id).ratUnits = #[] := by grind [deleteOne_preserves_ratUnits] + exact List.foldlRecOn arr.toList deleteOne h.1 hl · exact readyForRupAdd_delete f arr h.2 theorem deleteOne_subset (f : DefaultFormula n) (id : Nat) (c : DefaultClause n) : c ∈ toList (deleteOne f id) → c ∈ toList f := by simp only [deleteOne] intro h1 - split at h1 <;> first - | exact h1 - | rw [toList, List.mem_append, List.mem_append, or_assoc] at h1 - rw [toList, List.mem_append, List.mem_append, or_assoc] - rcases h1 with h1 | h1 | h1 - · apply Or.inl - simp only [List.mem_filterMap, id_eq, exists_eq_right] at h1 - simp only [List.mem_filterMap, id_eq, exists_eq_right] - rw [Array.set!, Array.setIfInBounds] at h1 - split at h1 - · simp only [Array.toList_set] at h1 - rcases List.getElem_of_mem h1 with ⟨i, h, h4⟩ - rw [List.getElem_set] at h4 - split at h4 - · simp at h4 - · rw [← h4] - apply List.getElem_mem - · exact h1 - · exact (Or.inr ∘ Or.inl) h1 - · exact (Or.inr ∘ Or.inr) h1 + rw [toList] at h1 ⊢ + split at h1 <;> grind theorem delete_subset (f : DefaultFormula n) (arr : Array Nat) (c : DefaultClause n) : c ∈ toList (delete f arr) → c ∈ toList f := by simp only [delete, ← Array.foldl_toList] - have hb : c ∈ toList f → c ∈ toList f := id have hl (f' : DefaultFormula n) (ih : c ∈ toList f' → c ∈ toList f) (id : Nat) (_ : id ∈ arr.toList) : - c ∈ toList (deleteOne f' id) → c ∈ toList f := by intro h; exact ih <| deleteOne_subset f' id c h - exact List.foldlRecOn arr.toList deleteOne hb hl + c ∈ toList (deleteOne f' id) → c ∈ toList f := by grind [deleteOne_subset] + exact List.foldlRecOn arr.toList deleteOne id hl end DefaultFormula diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.lean index d4af930c6c..d63eb0dfc1 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.lean +++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.lean @@ -11,6 +11,8 @@ This module contains the implementation of RAT-based clause adding for the defau implementation. -/ +set_option grind.warning false -- I've only made a partial effort to use grind here so far. + namespace Std.Tactic.BVDecide namespace LRAT namespace Internal @@ -30,9 +32,7 @@ theorem insertRatUnits_postcondition {n : Nat} (f : DefaultFormula n) (hf : f.ratUnits = #[] ∧ f.assignments.size = n) (units : CNF.Clause (PosFin n)) : let assignments := (insertRatUnits f units).fst.assignments - have hsize : assignments.size = n := by - rw [← hf.2] - exact size_assignments_insertRatUnits f units + have hsize : assignments.size = n := by grind [size_assignments_insertRatUnits] let ratUnits := (insertRatUnits f units).1.ratUnits InsertUnitInvariant f.assignments hf.2 ratUnits assignments hsize := by simp only [insertRatUnits] @@ -50,65 +50,15 @@ theorem nodup_insertRatUnits {n : Nat} (f : DefaultFormula n) (hf : f.ratUnits = #[] ∧ f.assignments.size = n) (units : CNF.Clause (PosFin n)) : ∀ i : Fin (f.insertRatUnits units).1.ratUnits.size, ∀ j : Fin (f.insertRatUnits units).1.ratUnits.size, i ≠ j → (f.insertRatUnits units).1.ratUnits[i] ≠ (f.insertRatUnits units).1.ratUnits[j] := by - intro i j i_ne_j + intro i rcases hi : (insertRatUnits f units).fst.ratUnits[i] with ⟨li, bi⟩ - rcases hj : (insertRatUnits f units).fst.ratUnits[j] with ⟨lj, bj⟩ - intro heq - cases heq have h := insertRatUnits_postcondition f hf units ⟨li.1, li.2.2⟩ - simp only [ne_eq, Bool.not_eq_true, exists_and_right] at h rcases h with ⟨_, h2⟩ | ⟨k, b, _, _, _, h4⟩ | ⟨k1, k2, li_gt_zero, h1, h2, h3, h4, h5⟩ - · specialize h2 j - rw [hj] at h2 - contradiction - · by_cases i = k - · next i_eq_k => - have j_ne_k : j ≠ k := by rw [← i_eq_k]; exact i_ne_j.symm - specialize h4 j j_ne_k - simp +decide only [hj] at h4 - · next i_ne_k => - specialize h4 i i_ne_k - simp +decide only [hi] at h4 + · grind + · by_cases i = k <;> grind · by_cases bi - · next bi_eq_true => - by_cases i = k1 - · next i_eq_k1 => - have j_ne_k1 : j ≠ k1 := by rw [← i_eq_k1]; exact i_ne_j.symm - by_cases j = k2 - · next j_eq_k2 => - rw [← j_eq_k2, hj, bi_eq_true] at h2 - simp at h2 - · next j_ne_k2 => - specialize h5 j j_ne_k1 j_ne_k2 - simp +decide only [hj] at h5 - · next i_ne_k1 => - by_cases i = k2 - · next i_eq_k2 => - rw [← i_eq_k2, hi, bi_eq_true] at h2 - simp at h2 - · next i_ne_k2 => - specialize h5 i i_ne_k1 i_ne_k2 - simp only [hi, not_true] at h5 - · next bi_eq_false => - simp only [Bool.not_eq_true] at bi_eq_false - by_cases i = k2 - · next i_eq_k2 => - have j_ne_k2 : j ≠ k2 := by rw [← i_eq_k2]; exact i_ne_j.symm - by_cases j = k1 - · next j_eq_k1 => - rw [← j_eq_k1, hj, bi_eq_false] at h1 - simp at h1 - · next j_ne_k1 => - specialize h5 j j_ne_k1 j_ne_k2 - simp +decide only [hj] at h5 - · next i_ne_k2 => - by_cases i = k1 - · next i_eq_k1 => - rw [← i_eq_k1, hi, bi_eq_false] at h1 - simp at h1 - · next i_ne_k1 => - specialize h5 i i_ne_k1 i_ne_k2 - simp +decide only [hi] at h5 + · by_cases i = k1 <;> grind + · by_cases i = k2 <;> grind theorem clear_insertRat_base_case {n : Nat} (f : DefaultFormula n) (hf : f.ratUnits = #[] ∧ f.assignments.size = n) (units : CNF.Clause (PosFin n)) : @@ -128,7 +78,7 @@ theorem clear_insertRat {n : Nat} (f : DefaultFormula n) ext : 1 · simp only [insertRatUnits] · simp only [insertRatUnits] - · rw [hf.1] + · grind · simp only let motive := ClearInsertInductionMotive f hf.2 (insertRatUnits f units).1.ratUnits have h_base : motive 0 (insertRatUnits f units).1.assignments := clear_insertRat_base_case f hf units @@ -144,8 +94,8 @@ theorem clear_insertRat {n : Nat} (f : DefaultFormula n) specialize h ⟨i, i_lt_n⟩ rcases h with h | h | h · exact h.1 - · omega - · omega + · omega -- FIXME why can't `grind` do this? + · omega -- FIXME why can't `grind` do this? theorem formula_performRatCheck {n : Nat} (f : DefaultFormula n) (hf : f.ratUnits = #[] ∧ f.assignments.size = n) (p : Literal (PosFin n)) @@ -166,7 +116,7 @@ theorem formula_performRatCheck {n : Nat} (f : DefaultFormula n) simp only [clauses_performRupCheck, rupUnits_performRupCheck, ratUnits_performRupCheck] rw [restoreAssignments_performRupCheck fc fc_assignments_size ratHint.2, ← insertRatUnits_rw, clear_insertRat f hf (negate (DefaultClause.delete c p))] - split <;> rfl + grind · rfl theorem performRatCheck_fold_formula_eq {n : Nat} (f : DefaultFormula n) @@ -184,6 +134,8 @@ theorem performRatCheck_fold_formula_eq {n : Nat} (f : DefaultFormula n) have h_base : motive 0 (f, true) := rfl have h_inductive (idx : Fin ratHints.size) (acc : DefaultFormula n × Bool) : motive idx.1 acc → motive (idx.1 + 1) (if acc.2 then performRatCheck acc.1 p ratHints[idx] else (acc.1, false)) := by + -- FIXME: this causes an internal `grind` error: + -- grind [formula_performRatCheck] intro ih rw [ih] split @@ -199,13 +151,13 @@ theorem ratAdd_result {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) (p simp only [Bool.not_eq_true'] at ratAddSuccess split at ratAddSuccess · split at ratAddSuccess - · simp at ratAddSuccess + · grind · split at ratAddSuccess - · simp at ratAddSuccess + · grind · split at ratAddSuccess - · simp at ratAddSuccess + · grind · split at ratAddSuccess - · simp at ratAddSuccess + · grind · next performRatCheck_fold_success => simp only [Bool.not_eq_false] at performRatCheck_fold_success let fc := (insertRupUnits f (negate c)).1 @@ -228,7 +180,7 @@ theorem ratAdd_result {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) (p clauses_performRupCheck, rupUnits_performRupCheck, ratUnits_performRupCheck, restoreAssignments_performRupCheck fc fc_assignments_size, ← insertRupUnits_rw, clear_insertRup f f_readyForRatAdd.2 (negate c), fc, performRupCheck_res] - · simp at ratAddSuccess + · grind end DefaultFormula diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean index fa86697d74..ba493245e9 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean +++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean @@ -11,6 +11,8 @@ This module contains the verification of RAT-based clause adding for the default implementation. -/ +set_option grind.warning false -- I've only made a partial effort to use grind here so far. + namespace Std.Tactic.BVDecide namespace LRAT namespace Internal @@ -51,22 +53,12 @@ theorem entails_of_irrelevant_assignment {n : Nat} {p : (PosFin n) → Bool} {c left constructor · simp [Clause.toList, delete_iff, negl_ne_v, v_in_c_del_l] - · split - · next heq => - simp only [heq, Literal.negate, ne_eq, Prod.mk.injEq, true_and] at negl_ne_v - simp_all - · next hne => - exact pv + · grind · exists v right constructor · simp [Clause.toList, delete_iff, negl_ne_v, v_in_c_del_l] - · split - · next heq => - simp only [heq, Literal.negate, ne_eq, Prod.mk.injEq, true_and] at negl_ne_v - simp_all - · next hne => - exact pv + · grind theorem assignmentsInvariant_insertRatUnits {n : Nat} (f : DefaultFormula n) (hf : f.ratUnits = #[] ∧ AssignmentsInvariant f) (units : CNF.Clause (PosFin n)) : @@ -90,7 +82,7 @@ theorem assignmentsInvariant_insertRatUnits {n : Nat} (f : DefaultFormula n) exact hp · specialize hp c <| (Or.inr ∘ Or.inl) cf exact hp - · simp [hf.1] at cf + · grind rcases h ⟨i.1, i.2.2⟩ with ⟨h1, h2⟩ | ⟨j, b', i_gt_zero, h1, h2, h3, h4⟩ | ⟨j1, j2, i_gt_zero, h1, h2, _, _, _⟩ · rw [h1] at hb exact hf.2.2 i b hb p pf @@ -222,35 +214,25 @@ theorem sat_of_confirmRupHint_of_insertRat_fold {n : Nat} (f : DefaultFormula n) rcases v_in_neg_c with ⟨v', ⟨_, v'_eq_v⟩ | ⟨v'_in_c, v'_eq_v⟩⟩ · simp [Literal.negate] at v'_eq_v · simp only [Literal.negate, Bool.not_true, Prod.mk.injEq, and_true] at v'_eq_v - simp only [(· ⊨ ·), Clause.eval, List.any_eq_true, decide_eq_true_eq, Prod.exists, - Bool.exists_bool, ← unsat_c_eq, not_exists, not_or, not_and] at p_unsat_c - specialize p_unsat_c v - rw [Clause.unit_eq] at p_unsat_c - simp only [List.mem_singleton, forall_const, Prod.mk.injEq, and_false, false_implies, and_true] at p_unsat_c - simp only [(· ⊨ ·), Bool.not_eq_false] at p_unsat_c + simp only [(· ⊨ ·), Clause.eval] at p_unsat_c specialize pc v rw [v'_eq_v] at v'_in_c have pv := pc.2 v'_in_c - simp only [(· ⊨ ·), Bool.not_eq_true] at pv - simp only [p_unsat_c] at pv - cases pv + grind · simp only [negate_eq, List.mem_map, Prod.exists, Bool.exists_bool] at v_in_neg_c rcases v_in_neg_c with ⟨v', ⟨v'_in_c, v'_eq_v⟩ | ⟨_, v'_eq_v⟩⟩ · simp only [Literal.negate, Bool.not_false, Prod.mk.injEq, and_true] at v'_eq_v - simp only [(· ⊨ ·), Clause.eval, List.any_eq_true, decide_eq_true_eq, Prod.exists, - Bool.exists_bool, ← unsat_c_eq, not_exists, not_or, not_and] at p_unsat_c + simp only [(· ⊨ ·), Clause.eval, List.any_eq_true, Prod.exists, ← unsat_c_eq, + not_exists] at p_unsat_c specialize p_unsat_c v rw [Clause.unit_eq] at p_unsat_c - simp only [List.mem_singleton, forall_const, Prod.mk.injEq, and_false, false_implies, and_true] at p_unsat_c + simp only [List.mem_singleton] at p_unsat_c specialize pc v rw [v'_eq_v] at v'_in_c have pv := pc.1 v'_in_c - simp only [(· ⊨ ·), Bool.not_eq_true] at pv - simp only [p_unsat_c] at pv - cases pv - · simp [Literal.negate] at v'_eq_v - · simp only [formulaEntails_def, List.all_eq_true, decide_eq_true_eq] at pf - exact p_unsat_c <| pf unsat_c unsat_c_in_f + grind + · grind + · grind [formulaEntails_def] theorem sat_of_insertRat {n : Nat} (f : DefaultFormula n) (hf : f.ratUnits = #[] ∧ AssignmentsInvariant f) (c : DefaultClause n) (p : PosFin n → Bool) @@ -389,28 +371,15 @@ theorem assignmentsInvariant_performRupCheck_of_assignmentsInvariant {n : Nat} ( simp only [f_AssignmentsInvariant.1, in_bounds_motive] have in_bounds_inductive (idx : Fin rupHints.size) (acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool) (ih : in_bounds_motive idx.1 acc) : in_bounds_motive (idx.1 + 1) (confirmRupHint f.clauses acc rupHints[idx]) := by - have h := size_assignemnts_confirmRupHint f.clauses acc.1 acc.2.1 acc.2.2.1 acc.2.2.2 rupHints[idx] + have h := size_assignments_confirmRupHint f.clauses acc.1 acc.2.1 acc.2.2.1 acc.2.2.2 rupHints[idx] have : (acc.fst, acc.snd.fst, acc.snd.snd.fst, acc.snd.snd.snd) = acc := rfl simp [this] at * - omega + omega -- FIXME `grind` fails here with an internal error + -- reported as https://github.com/leanprover/lean4/pull/8608 rw [Array.foldl_induction in_bounds_motive in_bounds_base in_bounds_inductive] exact i.2.2 - simp only [getElem!_def, i_in_bounds, Array.getElem?_eq_getElem] at h1 - simp only [( · ⊨ ·), Entails.eval.eq_1] - by_cases hb : b - · rw [hb] - rw [hb] at h - by_cases pi : p i - · exact pi - · simp only at pi - simp [pi, h] at h1 - · simp only [Bool.not_eq_true] at hb - rw [hb] - rw [hb] at h - by_cases pi : p i - · simp [pi, h] at h1 - · simp at pi - exact pi + simp only [( · ⊨ ·)] + grind [cases Bool] theorem c_without_negPivot_of_performRatCheck_success {n : Nat} (f : DefaultFormula n) (hf : f.ratUnits = #[] ∧ AssignmentsInvariant f) (negPivot : Literal (PosFin n)) @@ -442,22 +411,16 @@ theorem existsRatHint_of_ratHintsExhaustive {n : Nat} (f : DefaultFormula n) rw [List.mem_iff_getElem] at c'_in_f rcases c'_in_f with ⟨i, hi, c'_in_f⟩ simp only [ratHintsExhaustive, getRatClauseIndices] at ratHintsExhaustive_eq_true - have i_in_bounds : i < Array.size (Array.range (Array.size f.clauses)) := by - rw [Array.size_range] - simpa using hi - have i_lt_f_clauses_size : i < f.clauses.size := by - rw [Array.size_range] at i_in_bounds - exact i_in_bounds + have i_in_bounds : i < Array.size (Array.range (Array.size f.clauses)) := by grind + have i_lt_f_clauses_size : i < f.clauses.size := by grind have h : i ∈ (ratHints.map (fun x => x.1)).toList := by rw [← of_decide_eq_true ratHintsExhaustive_eq_true] - have i_eq_range_i : i = (Array.range f.clauses.size)[i]'i_in_bounds := by - rw [Array.getElem_range] + have i_eq_range_i : i = (Array.range f.clauses.size)[i]'i_in_bounds := by grind rw [i_eq_range_i] rw [Array.mem_toList_iff] rw [Array.mem_filter] constructor - · rw [← Array.mem_toList_iff] - apply Array.getElem_mem_toList + · grind · rw [Array.getElem_toList] at c'_in_f simp only [Array.getElem_range, getElem!_def, i_lt_f_clauses_size, Array.getElem?_eq_getElem, c'_in_f, contains_iff] @@ -465,14 +428,9 @@ theorem existsRatHint_of_ratHintsExhaustive {n : Nat} (f : DefaultFormula n) rcases List.get_of_mem h with ⟨j, h'⟩ have j_in_bounds : j < ratHints.size := by have j_property := j.2 - simp only [Array.toList_map, List.length_map] at j_property - dsimp at * - omega - simp only [List.get_eq_getElem, Array.toList_map, Array.length_toList, List.getElem_map] at h' - rw [Array.getElem_toList] at h' - rw [Array.getElem_toList] at c'_in_f + grind exists ⟨j.1, j_in_bounds⟩ - simp [getElem!_def, h', i_lt_f_clauses_size, dite_true, c'_in_f] + grind theorem performRatCheck_success_of_performRatCheck_fold_success {n : Nat} (f : DefaultFormula n) (hf : f.ratUnits = #[] ∧ f.assignments.size = n) (p : Literal (PosFin n)) @@ -496,15 +454,16 @@ theorem performRatCheck_success_of_performRatCheck_fold_success {n : Nat} (f : D motive (idx.1 + 1) (fold_fn acc ratHints[idx]) := by constructor · simp only [Fin.getElem_fin, fold_fn_def, ih.1] + -- grind [formula_performRatCheck] -- FIXME: internal grind error split - · rw [formula_performRatCheck] - exact hf + · grind [formula_performRatCheck] · rfl · intro h i rw [fold_fn_def] at h split at h · next acc_eq_true => have i_lt_or_eq_idx : i.1 < idx.1 ∨ i.1 = idx.1 := by + -- grind -- FIXME: internal grind error omega rcases i_lt_or_eq_idx with i_lt_idx | i_eq_idx · exact ih.2 acc_eq_true ⟨i.1, i_lt_idx⟩ diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean index 11b6fdca7a..619b0d8fb5 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean +++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean @@ -11,6 +11,8 @@ This module contains the implementation of RUP-based clause adding for the defau implementation. -/ +set_option grind.warning false -- I've only made a partial effort to use grind here so far. + namespace Std.Tactic.BVDecide namespace LRAT namespace Internal @@ -24,19 +26,12 @@ theorem size_insertUnit {n : Nat} (units : Array (Literal (PosFin n))) (assignments : Array Assignment) (b : Bool) (l : Literal (PosFin n)) : (insertUnit (units, assignments, b) l).2.1.size = assignments.size := by simp only [insertUnit] - split <;> simp + grind theorem size_insertUnit_fold : ∀ unitsAcc : Array (Literal (PosFin n)), ∀ assignments : Array Assignment, ∀ b : Bool, Array.size (List.foldl insertUnit (unitsAcc, assignments, b) units).2.1 = assignments.size := by - induction units - · simp only [List.foldl, forall_const] - · next hd tl ih => - intro unitsAcc assignments b - simp only [List.foldl] - let hd_res := insertUnit (unitsAcc, assignments, b) hd - specialize ih hd_res.1 hd_res.2.1 hd_res.2.2 - rw [ih, size_insertUnit] + induction units with grind [size_insertUnit] theorem size_assignments_insertRupUnits {n : Nat} (f : DefaultFormula n) (units : CNF.Clause (PosFin n)) : @@ -104,9 +99,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen apply Or.inr ∘ Or.inl have units_size_lt_updatedUnits_size : units.size < (insertUnit (units, assignments, foundContradiction) l).1.size := by simp only [insertUnit] - split - · contradiction - · simp only [Array.size_push, Nat.lt_succ_self] + grind let mostRecentUnitIdx : Fin (insertUnit (units, assignments, foundContradiction) l).1.size := ⟨units.size, units_size_lt_updatedUnits_size⟩ have i_gt_zero : i.1 > 0 := by rw [i_eq_l]; exact l.1.2.1 @@ -115,20 +108,14 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen constructor · rfl · constructor - · rw [Array.getElem_modify_self] - simp only [← i_eq_l, h1] + · grind · constructor - · simp only [getElem!_def, l_in_bounds, Array.getElem?_eq_getElem, - Bool.not_eq_true] at h3 - simp only [← i_eq_l, ← h1] - simp only [i_eq_l, h3] + · grind · intro k hk have k_in_bounds : k.1 < units.size := by apply Nat.lt_of_le_of_ne - · apply Nat.le_of_lt_succ - have k_property := k.2 - simp only [insertUnit, h3, ite_false, Array.size_push, reduceCtorEq] at k_property - exact k_property + · have k_property := k.2 + grind · intro h simp only [← h, not_true, mostRecentUnitIdx] at hk rw [Array.getElem_push_lt k_in_bounds] @@ -145,8 +132,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen by_cases h : j.val < Array.size units · simp only [h, dite_true] exact h2 ⟨j.1, h⟩ - · simp only [h, dite_false] - exact Ne.symm i_ne_l + · grind · by_cases hasAssignment l.2 assignments[l.1.1]! · next h5 => apply Or.inr ∘ Or.inl @@ -159,8 +145,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen intro k k_ne_j have k_size : k.1 < units.size := by have k_property := k.2 - simp only [insertUnit, h5, ite_true] at k_property - exact k_property + grind have k_ne_j : { val := k.val, isLt := k_size } ≠ j := by intro k_eq_j simp only [← Fin.val_eq_of_eq k_eq_j, not_true] at k_ne_j @@ -171,9 +156,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen apply Or.inr ∘ Or.inr have units_size_lt_updatedUnits_size : units.size < (insertUnit (units, assignments, foundContradiction) l).1.size := by simp only [insertUnit] - split - · contradiction - · simp only [Array.size_push, Nat.lt_succ_self] + grind let mostRecentUnitIdx : Fin (insertUnit (units, assignments, foundContradiction) l).1.size := ⟨units.size, units_size_lt_updatedUnits_size⟩ have j_lt_updatedUnits_size : j.1 < (insertUnit (units, assignments, foundContradiction) l).1.size := by @@ -275,7 +258,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen constructor · rw [Array.getElem_push_lt, h1] · constructor - · rw [Array.getElem_modify_of_ne (Ne.symm i_ne_l), h2] + · grind · constructor · exact h3 · intro k k_ne_j @@ -319,7 +302,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen simp only [i_eq_l] rw [Array.getElem_modify_self] simp only [← i_eq_l, h3, add_both_eq_both] - · next i_ne_l => rw [Array.getElem_modify_of_ne (Ne.symm i_ne_l), h3] + · next i_ne_l => grind · constructor · exact h4 · intro k k_ne_j1 k_ne_j2 @@ -340,21 +323,15 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen · next k_not_lt_units_size => split · next h => - exfalso have k_property := k.2 - simp only [insertUnit, h, ite_true] at k_property - exact k_not_lt_units_size k_property + grind · next h => simp only have k_eq_units_size : k.1 = units.size := by have k_property := k.2 - simp only [insertUnit, h, ite_false, Array.size_push, reduceCtorEq] at k_property - rcases Nat.lt_or_eq_of_le <| Nat.le_of_lt_succ k_property with k_lt_units_size | k_eq_units_size - · exfalso; exact k_not_lt_units_size k_lt_units_size - · exact k_eq_units_size - simp only [k_eq_units_size, Array.getElem_push_eq, ne_eq] - intro l_eq_i - simp [getElem!_def, l_eq_i, i_in_bounds, h3, has_both] at h + grind + simp only [k_eq_units_size, Array.getElem_push_eq] + grind [has_both] theorem insertUnitInvariant_insertUnit_fold {n : Nat} (assignments0 : Array Assignment) (assignments0_size : assignments0.size = n) (rupUnits : Array (Literal (PosFin n))) @@ -408,63 +385,13 @@ theorem nodup_insertRupUnits {n : Nat} (f : DefaultFormula n) (f_readyForRupAdd have h := insertUnitInvariant_insertRupUnits f f_readyForRupAdd units ⟨li.1, li.2.2⟩ simp only [ne_eq, Bool.not_eq_true, exists_and_right] at h rcases h with ⟨_, h2⟩ | ⟨k, b, _, _, _, h4⟩ | ⟨k1, k2, li_gt_zero, h1, h2, h3, h4, h5⟩ - · specialize h2 j - rw [hj, li_eq_lj] at h2 - simp only [not_true] at h2 - · by_cases i = k - · next i_eq_k => - have j_ne_k : j ≠ k := by rw [← i_eq_k]; exact i_ne_j.symm - specialize h4 j j_ne_k - rw [hj, li_eq_lj] at h4 - simp +decide only at h4 - · next i_ne_k => - specialize h4 i i_ne_k - rw [hi] at h4 - simp only [not_true] at h4 + · grind + · by_cases i = k <;> grind · by_cases bi - · next bi_eq_true => - by_cases i = k1 - · next i_eq_k1 => - have j_ne_k1 : j ≠ k1 := by rw [← i_eq_k1]; exact i_ne_j.symm - by_cases j = k2 - · next j_eq_k2 => - rw [← j_eq_k2, hj, ← bi_eq_bj, bi_eq_true] at h2 - simp at h2 - · next j_ne_k2 => - specialize h5 j j_ne_k1 j_ne_k2 - rw [hj, li_eq_lj] at h5 - simp +decide only at h5 - · next i_ne_k1 => - by_cases i = k2 - · next i_eq_k2 => - rw [← i_eq_k2, hi, bi_eq_true] at h2 - simp at h2 - · next i_ne_k2 => - specialize h5 i i_ne_k1 i_ne_k2 - rw [hi] at h5 - simp only [not_true] at h5 - · next bi_eq_false => - simp only [Bool.not_eq_true] at bi_eq_false - by_cases i = k2 - · next i_eq_k2 => - have j_ne_k2 : j ≠ k2 := by rw [← i_eq_k2]; exact i_ne_j.symm - by_cases j = k1 - · next j_eq_k1 => - rw [← j_eq_k1, hj, ← bi_eq_bj, bi_eq_false] at h1 - simp at h1 - · next j_ne_k1 => - specialize h5 j j_ne_k1 j_ne_k2 - rw [hj, li_eq_lj] at h5 - simp +decide only at h5 - · next i_ne_k2 => - by_cases i = k1 - · next i_eq_k1 => - rw [← i_eq_k1, hi, bi_eq_false] at h1 - simp at h1 - · next i_ne_k1 => - specialize h5 i i_ne_k1 i_ne_k2 - rw [hi] at h5 - simp only [not_true] at h5 + · by_cases i = k1 + · by_cases j = k2 <;> grind + · by_cases i = k2 <;> grind + · by_cases i = k2 <;> grind theorem size_clearUnit (assignments : Array Assignment) (l : Literal (PosFin n)) : (clearUnit assignments l).size = assignments.size := by @@ -534,9 +461,7 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme rw [hsize] exact i.2 have h := Array.getElem_modify_of_ne ih2 (removeAssignment units[idx.val].2) (by simpa using i_in_bounds) - simp only [Fin.getElem_fin] at h - rw [h] - exact ih1 + grind · intro j j_ge_idx_add_one exact ih2 j (Nat.le_of_succ_le j_ge_idx_add_one) · by_cases idx = j @@ -547,36 +472,25 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme rw [Array.getElem_modify_self, ih2, remove_add_cancel] exact ih3 · intro k k_ge_idx_add_one - have k_ge_idx : k.val ≥ idx.val := Nat.le_of_succ_le k_ge_idx_add_one - have k_ne_j : k ≠ j := by - intro k_eq_j - rw [k_eq_j, idx_eq_j] at k_ge_idx_add_one - exact Nat.not_succ_le_self j.val k_ge_idx_add_one + have k_ge_idx : k.val ≥ idx.val := by grind + have k_ne_j : k ≠ j := by grind exact ih4 k k_ge_idx k_ne_j · next idx_ne_j => refine Or.inr <| Or.inl <| ⟨j,b,i_gt_zero,?_⟩ constructor - · rw [← Nat.succ_eq_add_one] - apply Nat.succ_le_of_lt ∘ Nat.lt_of_le_of_ne j_ge_idx - intro idx_eq_j - exact idx_ne_j (Fin.eq_of_val_eq idx_eq_j) + · grind · constructor · exact ih1 · constructor · simp only [clearUnit, Array.getInternal_eq_getElem] - specialize ih4 idx (Nat.le_refl idx.1) idx_ne_j - rw [Array.getElem_modify_of_ne ih4] - exact ih2 + grind · constructor · exact ih3 · intro k k_ge_idx_add_one k_ne_j exact ih4 k (Nat.le_of_succ_le k_ge_idx_add_one) k_ne_j · by_cases idx = j1 · next idx_eq_j1 => - have idx_ne_j2 : idx ≠ j2 := by - rw [idx_eq_j1] - intro j1_eq_j2 - simp [j1_eq_j2, ih2] at ih1 + have idx_ne_j2 : idx ≠ j2 := by grind refine Or.inr <| Or.inl <| ⟨j2, false, i_gt_zero, ?_⟩ constructor · apply Nat.le_of_lt_succ @@ -597,11 +511,7 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme intro h1 by_cases units[k.1].2 · next h2 => - have k_ne_j1 : k ≠ j1 := by - rw [← idx_eq_j1] - intro k_eq_idx - rw [k_eq_idx] at k_ge_idx_add_one - exact Nat.lt_irrefl idx.1 <| Nat.lt_of_succ_le k_ge_idx_add_one + have k_ne_j1 : k ≠ j1 := by grind have h3 := units_nodup k j1 k_ne_j1 simp only [Fin.getElem_fin, ih1, ← h1, ← h2, ne_eq] at h3 exact h3 rfl @@ -638,11 +548,7 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme simp only [Fin.getElem_fin, ih1, ← h1, ← h2, ne_eq] at h3 exact h3 rfl · next h2 => - have k_ne_j2 : k ≠ j2 := by - rw [← idx_eq_j2] - intro k_eq_idx - rw [k_eq_idx] at k_ge_idx_add_one - exact Nat.lt_irrefl idx.1 <| Nat.lt_of_succ_le k_ge_idx_add_one + have k_ne_j2 : k ≠ j2 := by grind have h3 := units_nodup k j2 k_ne_j2 simp only [Bool.not_eq_true] at h2 simp only [Fin.getElem_fin, ih2, ← h1, ← h2, ne_eq] at h3 @@ -650,17 +556,9 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme · next idx_ne_j2 => refine Or.inr <| Or.inr <| ⟨j1, j2,i_gt_zero, ?_⟩ constructor - · apply Nat.le_of_lt_succ - rw [← Nat.succ_eq_add_one] - apply Nat.succ_lt_succ ∘ Nat.lt_of_le_of_ne j1_ge_idx - intro idx_eq_j1 - exact idx_ne_j1 (Fin.eq_of_val_eq idx_eq_j1) + · grind · constructor - · apply Nat.le_of_lt_succ - rw [← Nat.succ_eq_add_one] - apply Nat.succ_lt_succ ∘ Nat.lt_of_le_of_ne j2_ge_idx - intro idx_eq_j2 - exact idx_ne_j2 (Fin.eq_of_val_eq idx_eq_j2) + · grind · constructor · simp only [Fin.getElem_fin] exact ih1 @@ -669,20 +567,7 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme exact ih2 · constructor · simp only [clearUnit, Array.getInternal_eq_getElem] - have idx_res_ne_i : units[idx.1].1.1 ≠ i.1 := by - intro h1 - by_cases units[idx.1].2 - · next h2 => - have h3 := units_nodup idx j1 idx_ne_j1 - simp only [Fin.getElem_fin, ih1, ← h1, ← h2, ne_eq] at h3 - exact h3 rfl - · next h2 => - have h3 := units_nodup idx j2 idx_ne_j2 - simp only [Bool.not_eq_true] at h2 - simp only [Fin.getElem_fin, ih2, ← h1, ← h2, ne_eq] at h3 - exact h3 rfl - rw [Array.getElem_modify_of_ne idx_res_ne_i] - exact ih3 + grind · constructor · exact ih4 · intro k k_ge_idx_add_one @@ -711,7 +596,7 @@ theorem clear_insertRup {n : Nat} (f : DefaultFormula n) (f_readyForRupAdd : Rea specialize h ⟨i, i_lt_n⟩ rcases h with ⟨h,_⟩ · exact h - · omega + · omega -- FIXME: `grind` doesn't work here theorem clauses_performRupCheck {n : Nat} (f : DefaultFormula n) (rupHints : Array Nat) : (performRupCheck f rupHints).1.clauses = f.clauses := by @@ -725,14 +610,11 @@ theorem ratUnits_performRupCheck {n : Nat} (f : DefaultFormula n) (rupHints : Ar (performRupCheck f rupHints).1.ratUnits = f.ratUnits := by simp only [performRupCheck] -theorem size_assignemnts_confirmRupHint {n : Nat} (clauses : Array (Option (DefaultClause n))) +theorem size_assignments_confirmRupHint {n : Nat} (clauses : Array (Option (DefaultClause n))) (assignments : Array Assignment) (derivedLits : CNF.Clause (PosFin n)) (b1 b2 : Bool) (id : Nat) : (confirmRupHint clauses (assignments, derivedLits, b1, b2) id).1.size = assignments.size := by simp only [confirmRupHint] - repeat first - | rfl - | simp only [Array.size_modify] - | split + grind theorem size_assignments_performRupCheck {n : Nat} (f : DefaultFormula n) (rupHints : Array Nat) : (performRupCheck f rupHints).1.assignments.size = f.assignments.size := by @@ -741,11 +623,11 @@ theorem size_assignments_performRupCheck {n : Nat} (f : DefaultFormula n) (rupHi have hb : (f.assignments, ([] : CNF.Clause (PosFin n)), false, false).1.size = f.assignments.size := rfl have hl (acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool) (hsize : acc.1.size = f.assignments.size) (id : Nat) (_ : id ∈ rupHints.toList) : (confirmRupHint f.clauses acc id).1.size = f.assignments.size := by - have h := size_assignemnts_confirmRupHint f.clauses acc.1 acc.2.1 acc.2.2.1 acc.2.2.2 id + have h := size_assignments_confirmRupHint f.clauses acc.1 acc.2.1 acc.2.2.1 acc.2.2.2 id rw [h, hsize] exact List.foldlRecOn rupHints.toList (confirmRupHint f.clauses) hb hl -def DerivedLitsInvariant {n : Nat} (f : DefaultFormula n) +@[local grind] def DerivedLitsInvariant {n : Nat} (f : DefaultFormula n) (fassignments_size : f.assignments.size = n) (assignments : Array Assignment) (assignments_size : assignments.size = n) (derivedLits : CNF.Clause (PosFin n)) : Prop := @@ -789,10 +671,7 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula · constructor · simp only [l_eq_i, Array.getElem_modify_self, List.get, h1] · constructor - · simp only [List.get, Bool.not_eq_true] - simp only [getElem!_def, l_in_bounds, Array.getElem?_eq_getElem, Bool.not_eq_true] at h - simp only [l_eq_i, h1] at h - exact h + · grind · intro k k_ne_zero have k_eq_succ : ∃ k' : Nat, ∃ k'_succ_in_bounds : k' + 1 < (l :: acc.2.1).length, k = ⟨k' + 1, k'_succ_in_bounds⟩ := by have k_val_ne_zero : k.1 ≠ 0 := by @@ -809,36 +688,18 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula exact k_eq_k'_succ rcases k_eq_succ with ⟨k', k'_succ_in_bounds, k_eq_succ⟩ rw [k_eq_succ, List.get_cons_succ] - have k'_in_bounds : k' < acc.2.1.length := by - simp only [List.length_cons, Nat.succ_eq_add_one] at k'_succ_in_bounds - exact Nat.lt_of_succ_lt_succ k'_succ_in_bounds - exact h2 (acc.2.1.get ⟨k', k'_in_bounds⟩) <| List.get_mem acc.snd.fst ⟨k', k'_in_bounds⟩ - · next l_ne_i => - apply Or.inl - constructor - · rw [Array.getElem_modify_of_ne l_ne_i] - exact h1 - · intro l' l'_in_list - simp only [List.find?, List.mem_cons] at l'_in_list - rcases l'_in_list with l'_eq_l | l'_in_acc - · rw [l'_eq_l] - exact l_ne_i - · exact h2 l' l'_in_acc + have k'_in_bounds : k' < acc.2.1.length := by grind + exact h2 (acc.2.1.get ⟨k', k'_in_bounds⟩) (by grind) + · next l_ne_i => grind · let l' := acc.2.1.get j - have zero_in_bounds : 0 < (l :: acc.2.1).length := by - simp only [List.length_cons] - exact Nat.zero_lt_succ (List.length acc.snd.fst) + have zero_in_bounds : 0 < (l :: acc.2.1).length := by grind have j_succ_in_bounds : j.1 + 1 < (l :: acc.2.1).length := by simp only [List.length_cons, Nat.succ_eq_add_one] exact Nat.succ_lt_succ j.2 by_cases l.1.1 = i.1 · next l_eq_i => apply Or.inr ∘ Or.inr - have l_ne_l' : l.2 ≠ l'.2 := by - intro l_eq_l' - rw [l_eq_i] at h - simp only [l'] at l_eq_l' - simp [getElem!_def, i_in_bounds, h1, l_eq_l', has_add] at h + have l_ne_l' : l.2 ≠ l'.2 := by grind [has_add] by_cases l.2 · next l_eq_true => rw [l_eq_true] at l_ne_l' @@ -846,11 +707,9 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula apply Exists.intro ⟨0, zero_in_bounds⟩ apply Exists.intro ⟨j.1 + 1, j_succ_in_bounds⟩ constructor - · simp only [List.get] - exact l_eq_i + · grind · constructor - · simp only [List.get, Nat.add_eq, Nat.add_zero] - exact j_eq_i + · grind · simp only [List.get, Nat.add_eq, Nat.add_zero, List.length_cons, ne_eq] apply And.intro l_eq_true ∘ And.intro l'_eq_false constructor @@ -879,27 +738,18 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula rcases k_eq_succ with ⟨k', k'_succ_in_bounds, k_eq_succ⟩ rw [k_eq_succ] simp only [List.get, Nat.add_eq, Nat.add_zero, ne_eq] - have k'_in_bounds : k' < acc.2.1.length := by - simp only [List.length_cons, Nat.succ_eq_add_one] at k'_succ_in_bounds - exact Nat.lt_of_succ_lt_succ k'_succ_in_bounds - have k'_ne_j : ⟨k', k'_in_bounds⟩ ≠ j := by - simp only [k_eq_succ, List.length_cons, Fin.mk.injEq, Nat.succ.injEq] at k_ne_j_succ - exact Fin.ne_of_val_ne k_ne_j_succ + have k'_in_bounds : k' < acc.2.1.length := by grind + have k'_ne_j : ⟨k', k'_in_bounds⟩ ≠ j := by grind exact h3 ⟨k', k'_in_bounds⟩ k'_ne_j · next l_eq_false => simp only [Bool.not_eq_true] at l_eq_false rw [l_eq_false] at l_ne_l' - have l'_eq_true : l'.2 = true := by - have l'_ne_false : l'.2 ≠ false := Ne.symm l_ne_l' - simp only [ne_eq, Bool.not_eq_false] at l'_ne_false - exact l'_ne_false + have l'_eq_true : l'.2 = true := by grind refine ⟨⟨j.1 + 1, j_succ_in_bounds⟩, ⟨0, zero_in_bounds⟩, ?_⟩ constructor - · simp only [List.get, Nat.add_eq, Nat.add_zero] - exact j_eq_i + · grind · constructor - · simp only [List.get] - exact l_eq_i + · grind · simp only [List.get, Nat.add_eq, Nat.add_zero, List.length_cons, ne_eq] apply And.intro l'_eq_true ∘ And.intro l_eq_false constructor @@ -928,12 +778,8 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula rcases k_eq_succ with ⟨k', k'_succ_in_bounds, k_eq_succ⟩ rw [k_eq_succ] simp only [List.get, Nat.add_eq, Nat.add_zero, ne_eq] - have k'_in_bounds : k' < acc.2.1.length := by - simp only [List.length_cons, Nat.succ_eq_add_one] at k'_succ_in_bounds - exact Nat.lt_of_succ_lt_succ k'_succ_in_bounds - have k'_ne_j : ⟨k', k'_in_bounds⟩ ≠ j := by - simp only [k_eq_succ, List.length_cons, Fin.mk.injEq, Nat.succ.injEq] at k_ne_j_succ - exact Fin.ne_of_val_ne k_ne_j_succ + have k'_in_bounds : k' < acc.2.1.length := by grind + have k'_ne_j : ⟨k', k'_in_bounds⟩ ≠ j := by grind exact h3 ⟨k', k'_in_bounds⟩ k'_ne_j · next l_ne_i => apply Or.inr ∘ Or.inl ∘ Exists.intro ⟨j.1 + 1, j_succ_in_bounds⟩ @@ -941,8 +787,7 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula constructor · exact j_eq_i · constructor - · rw [Array.getElem_modify_of_ne l_ne_i] - exact h1 + · grind · apply And.intro h2 intro k k_ne_j_succ by_cases k.1 = 0 @@ -955,9 +800,7 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula exact l_ne_i · next k_ne_zero => have k_eq_succ : ∃ k' : Nat, ∃ k'_succ_in_bounds : k' + 1 < (l :: acc.2.1).length, k = ⟨k' + 1, k'_succ_in_bounds⟩ := by - have k_val_ne_zero : k.1 ≠ 0 := by - intro k_eq_zero - simp only [List.length_cons, ← k_eq_zero, ne_eq, not_true] at k_ne_zero + have k_val_ne_zero : k.1 ≠ 0 := by grind rcases Nat.exists_eq_succ_of_ne_zero k_val_ne_zero with ⟨k', k_eq_k'_succ⟩ rw [Nat.succ_eq_add_one] at k_eq_k'_succ have k'_succ_in_bounds : k' + 1 < (l :: acc.2.1).length := by rw [← k_eq_k'_succ]; exact k.2 @@ -967,13 +810,8 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula rcases k_eq_succ with ⟨k', k'_succ_in_bounds, k_eq_succ⟩ rw [k_eq_succ] simp only [List.get, Nat.add_eq, Nat.add_zero, ne_eq] - have k'_in_bounds : k' < acc.2.1.length := by - simp only [List.length_cons, Nat.succ_eq_add_one] at k'_succ_in_bounds - exact Nat.lt_of_succ_lt_succ k'_succ_in_bounds - have k'_ne_j : ⟨k', k'_in_bounds⟩ ≠ j := by - simp only [List.length_cons] at k_eq_succ - simp only [List.length_cons, k_eq_succ, ne_eq, Fin.mk.injEq, Nat.succ.injEq] at k_ne_j_succ - exact Fin.ne_of_val_ne k_ne_j_succ + have k'_in_bounds : k' < acc.2.1.length := by grind + have k'_ne_j : ⟨k', k'_in_bounds⟩ ≠ j := by grind exact h3 ⟨k', k'_in_bounds⟩ k'_ne_j · have j1_succ_in_bounds : j1.1 + 1 < (l :: acc.2.1).length := by simp only [List.length_cons, Nat.succ_eq_add_one] @@ -993,18 +831,13 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula all_goals simp +decide [getElem!_def, l_eq_i, i_in_bounds, h1] at h constructor - · rw [Array.getElem_modify_of_ne l_ne_i] - exact h1 + · grind · constructor · exact h2 · intro k k_ne_j1_succ k_ne_j2_succ - have zero_in_bounds : 0 < (l :: acc.2.1).length := by - simp only [List.length_cons] - exact Nat.zero_lt_succ (List.length acc.snd.fst) + have zero_in_bounds : 0 < (l :: acc.2.1).length := by grind by_cases k = ⟨0, zero_in_bounds⟩ - · next k_eq_zero => - simp only [k_eq_zero, List.length_cons, List.get, ne_eq] - exact l_ne_i + · next k_eq_zero => grind · next k_ne_zero => have k_eq_succ : ∃ k' : Nat, ∃ k'_succ_in_bounds : k' + 1 < (l :: acc.2.1).length, k = ⟨k' + 1, k'_succ_in_bounds⟩ := by have k_val_ne_zero : k.1 ≠ 0 := by @@ -1019,15 +852,9 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula rcases k_eq_succ with ⟨k', k'_succ_in_bounds, k_eq_succ⟩ rw [k_eq_succ] simp only [List.get, Nat.add_eq, Nat.add_zero, ne_eq] - have k'_in_bounds : k' < acc.2.1.length := by - simp only [List.length_cons, Nat.succ_eq_add_one] at k'_succ_in_bounds - exact Nat.lt_of_succ_lt_succ k'_succ_in_bounds - have k'_ne_j1 : ⟨k', k'_in_bounds⟩ ≠ j1 := by - simp only [List.length_cons, k_eq_succ, ne_eq, Fin.mk.injEq, Nat.succ.injEq, j1_succ] at k_ne_j1_succ - exact Fin.ne_of_val_ne k_ne_j1_succ - have k'_ne_j2 : ⟨k', k'_in_bounds⟩ ≠ j2 := by - simp only [List.length_cons, k_eq_succ, ne_eq, Fin.mk.injEq, Nat.succ.injEq, j2_succ] at k_ne_j2_succ - exact Fin.ne_of_val_ne k_ne_j2_succ + have k'_in_bounds : k' < acc.2.1.length := by grind + have k'_ne_j1 : ⟨k', k'_in_bounds⟩ ≠ j1 := by grind + have k'_ne_j2 : ⟨k', k'_in_bounds⟩ ≠ j2 := by grind exact h3 ⟨k', k'_in_bounds⟩ k'_ne_j1 k'_ne_j2 theorem derivedLitsInvariant_confirmRupHint {n : Nat} (f : DefaultFormula n) (f_assignments_size : f.assignments.size = n) @@ -1038,8 +865,7 @@ theorem derivedLitsInvariant_confirmRupHint {n : Nat} (f : DefaultFormula n) (f_ ∃ hsize : rupHint_res.1.size = n, DerivedLitsInvariant f f_assignments_size rupHint_res.1 hsize rupHint_res.2.1 := by rcases ih with ⟨hsize, ih⟩ have hsize' : Array.size ((confirmRupHint f.clauses) acc rupHints[i]).1 = n := by - rw [size_assignemnts_confirmRupHint] - exact hsize + grind [size_assignments_confirmRupHint] apply Exists.intro hsize' simp only [confirmRupHint, Fin.getElem_fin] split @@ -1051,10 +877,8 @@ theorem derivedLitsInvariant_confirmRupHint {n : Nat} (f : DefaultFormula n) (f_ | some none => exact Or.inr <| Or.inl rfl | some (some c) => exact (Or.inr ∘ Or.inr ∘ Exists.intro c) rfl rcases rupHint_clause_options with rupHint_clause_eq_none | rupHint_clause_eq_some_none | ⟨c, rupHint_clause_eq_c⟩ - · simp only [rupHint_clause_eq_none] - exact ih - · simp only [rupHint_clause_eq_some_none] - exact ih + · grind + · grind · simp only [rupHint_clause_eq_c] have reduce_c_options : reduce c acc.1 = ReduceResult.encounteredBoth ∨ reduce c acc.1 = ReduceResult.reducedToEmpty ∨ (∃ l : Literal (PosFin n), reduce c acc.1 = ReduceResult.reducedToUnit l) ∨ reduce c acc.1 = ReduceResult.reducedToNonunit := by @@ -1064,18 +888,14 @@ theorem derivedLitsInvariant_confirmRupHint {n : Nat} (f : DefaultFormula n) (f_ | ReduceResult.reducedToUnit l => exact (Or.inr ∘ Or.inr ∘ Or.inl ∘ Exists.intro l) rfl | ReduceResult.reducedToNonunit => exact (Or.inr ∘ Or.inr ∘ Or.inr) rfl rcases reduce_c_options with hencounteredBoth | hreducedToEmpty | ⟨l, hreducedToUnit⟩ | hreducedToNonunit - · simp only [hencounteredBoth] - exact ih - · simp only [hreducedToEmpty] - exact ih + · grind + · grind · simp only [hreducedToUnit] by_cases h : hasAssignment l.snd acc.fst[l.fst.val]! - · simp only [h, ite_true] - exact ih + · grind · simp only [h, ite_false] exact confirmRupHint_preserves_invariant_helper f f_assignments_size acc hsize l ih h - · simp only [hreducedToNonunit] - exact ih + · grind theorem derivedLitsInvariant_performRupCheck {n : Nat} (f : DefaultFormula n) (f_assignments_size : f.assignments.size = n) (rupHints : Array Nat) @@ -1084,14 +904,7 @@ theorem derivedLitsInvariant_performRupCheck {n : Nat} (f : DefaultFormula n) (f DerivedLitsInvariant f f_assignments_size rupCheckRes.1.assignments f'_assignments_size rupCheckRes.2.1 := by let motive := fun (_ : Nat) (acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool) => ∃ hsize : acc.1.size = n, DerivedLitsInvariant f f_assignments_size acc.1 hsize acc.2.1 - have h_base : motive 0 (f.assignments, [], false, false) := by - apply Exists.intro f_assignments_size - intro i - apply Or.inl - constructor - · rfl - · intro l l_in_nil - simp only [List.find?, List.not_mem_nil] at l_in_nil + have h_base : motive 0 (f.assignments, [], false, false) := by grind have h_inductive (i : Fin rupHints.size) (acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool) (ih : motive i.1 acc) := derivedLitsInvariant_confirmRupHint f f_assignments_size rupHints i acc ih rcases Array.foldl_induction motive h_base h_inductive with ⟨_, h⟩ @@ -1113,12 +926,10 @@ theorem nodup_derivedLits {n : Nat} (f : DefaultFormula n) simp [li, Array.getElem_mem] have i_in_bounds : i.1 < derivedLits.length := by have i_property := i.2 - simp only [derivedLits_arr_def, List.size_toArray] at i_property - exact i_property + grind have j_in_bounds : j.1 < derivedLits.length := by have j_property := j.2 - simp only [derivedLits_arr_def, List.size_toArray] at j_property - exact j_property + grind rcases derivedLits_satisfies_invariant ⟨li.1.1, li.1.2.2⟩ with ⟨_, h2⟩ | ⟨k, _, _, _, h3⟩ | ⟨k1, k2, _, _, k1_eq_true, k2_eq_false, _, _, h3⟩ · exact h2 li li_in_derivedLits rfl @@ -1135,7 +946,7 @@ theorem nodup_derivedLits {n : Nat} (f : DefaultFormula n) · next k_ne_i => have i_ne_k : ⟨i.1, i_in_bounds⟩ ≠ k := by intro i_eq_k; simp only [← i_eq_k, not_true] at k_ne_i specialize h3 ⟨i.1, i_in_bounds⟩ i_ne_k - simp +decide [Fin.getElem_fin, derivedLits_arr_def, ne_eq, li] at h3 + grind [Fin.getElem_fin] · by_cases li.2 = true · next li_eq_true => have i_ne_k2 : ⟨i.1, i_in_bounds⟩ ≠ k2 := by @@ -1210,8 +1021,8 @@ theorem restoreAssignments_performRupCheck_base_case {n : Nat} (f : DefaultFormu · intro j _ have idx_in_list : derivedLits_arr[j] ∈ derivedLits := by simp only [derivedLits_arr_def, Fin.getElem_fin] - apply Array.getElem_mem_toList - exact h2 derivedLits_arr[j] idx_in_list + grind + grind · apply Or.inr ∘ Or.inl have j_lt_derivedLits_arr_size : j.1 < derivedLits_arr.size := by simp only [derivedLits_arr_def, List.size_toArray] @@ -1227,8 +1038,7 @@ theorem restoreAssignments_performRupCheck_base_case {n : Nat} (f : DefaultFormu intro k _ k_ne_j have k_in_bounds : k < derivedLits.length := by have k_property := k.2 - simp only [derivedLits_arr_def, List.size_toArray] at k_property - exact k_property + grind have k_ne_j : ⟨k.1, k_in_bounds⟩ ≠ j := by apply Fin.ne_of_val_ne simp only @@ -1258,8 +1068,7 @@ theorem restoreAssignments_performRupCheck_base_case {n : Nat} (f : DefaultFormu intro k _ k_ne_j1 k_ne_j2 have k_in_bounds : k < derivedLits.length := by have k_property := k.2 - simp only [derivedLits_arr_def, List.size_toArray] at k_property - exact k_property + grind have k_ne_j1 : ⟨k.1, k_in_bounds⟩ ≠ j1 := by apply Fin.ne_of_val_ne simp only @@ -1303,8 +1112,7 @@ theorem restoreAssignments_performRupCheck {n : Nat} (f : DefaultFormula n) (f_a rw [f_assignments_size] at hi2 specialize h ⟨i, hi2⟩ rcases h with ⟨h1, _⟩ | ⟨j, b, i_gt_zero, j_ge_derivedLits_size, _⟩ | ⟨j1, j2, i_gt_zero, j1_ge_derivedLits_size, _⟩ - · simp only [← derivedLits_arr_def] - exact h1 + · grind · exfalso exact (Nat.not_lt_of_le j_ge_derivedLits_size) j.2 · exfalso @@ -1319,9 +1127,9 @@ theorem rupAdd_result {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) (ru · simp only [clear_insertRup f f_readyForRupAdd (negate c), Prod.mk.injEq, and_true] at rupAddSuccess exact rupAddSuccess.symm · split at rupAddSuccess - · simp at rupAddSuccess + · grind · split at rupAddSuccess - · simp at rupAddSuccess + · grind · let fc := (insertRupUnits f (negate c)).1 have fc_assignments_size : (insertRupUnits f (negate c)).1.assignments.size = n := by rw [size_assignments_insertRupUnits f (negate c)] diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean index 1ca41b01ba..9b5c982f28 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean +++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean @@ -11,6 +11,7 @@ This module contains the verification of RUP-based clause adding for the default implementation. -/ +set_option grind.warning false -- I've only made a partial effort to use grind here so far. namespace Std.Tactic.BVDecide namespace LRAT namespace Internal @@ -98,26 +99,19 @@ theorem mem_insertUnit_units {n : Nat} (units : Array (Literal (PosFin n))) (ass intro insertUnit_res l' l'_in_insertUnit_res simp only [insertUnit_res] at * simp only [insertUnit] at l'_in_insertUnit_res - split at l'_in_insertUnit_res - · exact Or.inr l'_in_insertUnit_res - · simp only [Array.toList_push, List.mem_append, List.mem_singleton] at l'_in_insertUnit_res - exact Or.symm l'_in_insertUnit_res + grind theorem mem_insertUnit_fold_units {n : Nat} (units : Array (Literal (PosFin n))) (assignments : Array Assignment) (foundContradiction : Bool) (l : CNF.Clause (PosFin n)) : let insertUnit_fold_res := List.foldl insertUnit (units, assignments, foundContradiction) l ∀ l' : Literal (PosFin n), l' ∈ insertUnit_fold_res.1.toList → l' ∈ l ∨ l' ∈ units.toList := by have hb (l' : Literal (PosFin n)) : l' ∈ (units, assignments, foundContradiction).1.toList → l' ∈ l ∨ l' ∈ units.toList := by - intro h - exact Or.inr h + grind have hl (acc : Array (Literal (PosFin n)) × Array Assignment × Bool) (h : ∀ l' : Literal (PosFin n), l' ∈ acc.1.toList → l' ∈ l ∨ l' ∈ units.toList) (l'' : Literal (PosFin n)) (l''_in_l : l'' ∈ l) : ∀ l' : Literal (PosFin n), l' ∈ (insertUnit acc l'').1.toList → l' ∈ l ∨ l' ∈ units.toList := by intro l' l'_in_res - rcases mem_insertUnit_units acc.1 acc.2.1 acc.2.2 l'' l' l'_in_res with l'_eq_l'' | l'_in_acc - · rw [l'_eq_l''] - exact Or.inl l''_in_l - · exact h l' l'_in_acc + rcases mem_insertUnit_units acc.1 acc.2.1 acc.2.2 l'' l' l'_in_res with l'_eq_l'' | l'_in_acc <;> grind exact List.foldlRecOn l insertUnit hb hl theorem sat_of_insertRup {n : Nat} (f : DefaultFormula n) (f_readyForRupAdd : ReadyForRupAdd f) (c : DefaultClause n) @@ -126,8 +120,7 @@ theorem sat_of_insertRup {n : Nat} (f : DefaultFormula n) (f_readyForRupAdd : Re simp only [insertRupUnits] intro insertUnit_fold_success have false_imp : false → ∃ i : PosFin n, f.assignments[i.1]'(by rw [f_readyForRupAdd.2.1]; exact i.2.2) = both := by - intro h - simp at h + grind rcases contradiction_of_insertUnit_fold_success f.assignments f_readyForRupAdd.2.1 f.rupUnits false (negate c) false_imp insertUnit_fold_success with ⟨i, hboth⟩ have i_in_bounds : i.1 < f.assignments.size := by rw [f_readyForRupAdd.2.1]; exact i.2.2 @@ -216,10 +209,7 @@ theorem sat_of_insertRup {n : Nat} (f : DefaultFormula n) (f_readyForRupAdd : Re Bool.not_eq_false'] at i_true_in_insertUnit_fold i_false_in_insertUnit_fold have c_not_tautology := Clause.not_tautology c (i, true) simp only [Clause.toList, (· ⊨ ·)] at c_not_tautology - rw [DefaultClause.toList] at c_not_tautology - rcases c_not_tautology with i_true_not_in_c | i_false_not_in_c - · exact i_true_not_in_c i_false_in_insertUnit_fold - · exact i_false_not_in_c i_true_in_insertUnit_fold + grind theorem safe_insert_of_insertRup {n : Nat} (f : DefaultFormula n) (f_readyForRupAdd : ReadyForRupAdd f) (c : DefaultClause n) : @@ -376,24 +366,24 @@ theorem unsat_of_encounteredBoth {n : Nat} (c : DefaultClause n) split at h · exact ih rfl · split at h - · split at h <;> simp at h - · split at h <;> simp at h + · grind + · grind · next heq => intro p hp simp only [(· ⊨ ·), Bool.not_eq_true] at hp specialize hp l.1 simp [heq, has_both] at hp - · simp at h + · grind · split at h - · split at h <;> simp at h - · split at h <;> simp at h + · grind + · grind · next heq => intro p hp simp only [(· ⊨ ·), Bool.not_eq_true] at hp specialize hp l.1 simp [heq, has_both] at hp - · simp at h - · simp at h + · grind + · grind exact List.foldlRecOn c.clause (reduce_fold_fn assignment) hb hl def ReducePostconditionInductionMotive (c_arr : Array (Literal (PosFin n))) @@ -413,11 +403,11 @@ theorem reduce_fold_fn_preserves_induction_motive {c_arr : Array (Literal (PosFi · intro h p rw [reduce_fold_fn.eq_def] at h split at h - · simp at h + · grind · split at h · next heq => split at h - · simp at h + · grind · next c_arr_idx_eq_false => simp only [Bool.not_eq_true] at c_arr_idx_eq_false rcases ih.1 rfl p with ih1 | ih1 @@ -453,19 +443,14 @@ theorem reduce_fold_fn_preserves_induction_motive {c_arr : Array (Literal (PosFi · next h => exact Or.inr h · exact Or.inr ih1 - · simp at h - · simp at h - · next l => - split at h - · split at h <;> contradiction - · split at h <;> contradiction - · simp at h - · simp at h - · simp at h + · grind + · grind + · grind + · grind · intro i b h p hp j j_lt_idx_add_one p_entails_c_arr_j rw [reduce_fold_fn.eq_def] at h split at h - · simp at h + · grind · split at h · next heq => split at h @@ -482,7 +467,7 @@ theorem reduce_fold_fn_preserves_induction_motive {c_arr : Array (Literal (PosFi · next p_c_arr_idx_eq_false => simp only [h, Bool.not_eq_true] at p_c_arr_idx_eq_false simp +decide only [h, p_c_arr_idx_eq_false] at hp - · simp at h + · grind · next heq => split at h · next c_arr_idx_eq_true => @@ -498,8 +483,8 @@ theorem reduce_fold_fn_preserves_induction_motive {c_arr : Array (Literal (PosFi · next p_c_arr_idx_eq_false => simp only [h] at p_c_arr_idx_eq_false simp only [(· ⊨ ·), c_arr_idx_eq_true, p_c_arr_idx_eq_false] - · simp at h - · simp at h + · grind + · grind · simp only [reducedToUnit.injEq] at h rw [← h] rcases Nat.lt_or_eq_of_le <| Nat.le_of_lt_succ j_lt_idx_add_one with j_lt_idx | j_eq_idx @@ -507,13 +492,12 @@ theorem reduce_fold_fn_preserves_induction_motive {c_arr : Array (Literal (PosFi rcases ih.1 rfl p with ih1 | ih1 · exact ih1 j j_lt_idx p_entails_c_arr_j · exact ih1 hp - · simp only [j_eq_idx] at p_entails_c_arr_j - exact p_entails_c_arr_j + · grind · next l => split at h · next heq => split at h - · simp at h + · grind · next c_arr_idx_eq_false => simp only [Bool.not_eq_true] at c_arr_idx_eq_false simp only [reducedToUnit.injEq] at h @@ -528,7 +512,7 @@ theorem reduce_fold_fn_preserves_induction_motive {c_arr : Array (Literal (PosFi simp +decide only [p_entails_c_arr_j, decide_true, heq] at hp · next heq => split at h - · simp at h + · grind · next c_arr_idx_eq_true => simp only [Bool.not_eq_true', Bool.not_eq_false] at c_arr_idx_eq_true simp only [reducedToUnit.injEq] at h @@ -541,9 +525,9 @@ theorem reduce_fold_fn_preserves_induction_motive {c_arr : Array (Literal (PosFi simp only [(· ⊨ ·), Bool.not_eq_true] at hp specialize hp c_arr[idx.1].1 simp +decide only [p_entails_c_arr_j, decide_true, heq] at hp - · simp at h - · simp at h - · simp at h + · grind + · grind + · grind theorem reduce_postcondition {n : Nat} (c : DefaultClause n) (assignment : Array Assignment) : (reduce c assignment = reducedToEmpty → Incompatible (PosFin n) c assignment) ∧ @@ -553,14 +537,7 @@ theorem reduce_postcondition {n : Nat} (c : DefaultClause n) (assignment : Array rw [reduce, c_clause_rw, Array.foldl_toList] let motive := ReducePostconditionInductionMotive c_arr assignment have h_base : motive 0 reducedToEmpty := by - have : ∀ (a : PosFin n) (b : Bool), (reducedToEmpty = reducedToUnit (a, b)) = False := by intros; simp - simp only [ReducePostconditionInductionMotive, Fin.getElem_fin, forall_exists_index, and_imp, Prod.forall, - forall_const, false_implies, implies_true, and_true, motive, this] - intro p - apply Or.inl - intro i i_lt_zero - exfalso - exact Nat.not_lt_zero i.1 i_lt_zero + grind [ReducePostconditionInductionMotive] have h_inductive (idx : Fin c_arr.size) (res : ReduceResult (PosFin n)) (ih : motive idx.1 res) : motive (idx.1 + 1) (reduce_fold_fn assignment res c_arr[idx]) := reduce_fold_fn_preserves_induction_motive idx res ih rcases Array.foldl_induction motive h_base h_inductive with ⟨h1, h2⟩ @@ -577,6 +554,7 @@ theorem reduce_postcondition {n : Nat} (c : DefaultClause n) (assignment : Array have idx_exists : ∃ idx : Fin c_arr.size, c_arr[idx] = (i, false) := by rcases List.get_of_mem pc1 with ⟨idx, hidx⟩ simp only [List.get_eq_getElem] at hidx + -- grind -- FIXME: internal grind error exact Exists.intro idx hidx rcases idx_exists with ⟨idx, hidx⟩ specialize h1 idx idx.2 @@ -587,6 +565,7 @@ theorem reduce_postcondition {n : Nat} (c : DefaultClause n) (assignment : Array have idx_exists : ∃ idx : Fin c_arr.size, c_arr[idx] = (i, true) := by rcases List.get_of_mem pc1 with ⟨idx, hidx⟩ simp only [List.get_eq_getElem] at hidx + -- grind -- FIXME: internal grind error exact Exists.intro idx hidx rcases idx_exists with ⟨idx, hidx⟩ specialize h1 idx idx.2 @@ -643,15 +622,8 @@ theorem confirmRupHint_preserves_motive {n : Nat} (f : DefaultFormula n) (rupHin split · next c hc => have c_in_f : c ∈ toList f := by - simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq, - exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool] - apply Or.inl - simp only [getElem?, decidableGetElem?] at hc - split at hc - · simp only [Option.some.injEq] at hc - rw [← hc] - apply Array.getElem_mem_toList - · simp at hc + simp only [toList, List.mem_append, List.mem_filterMap, id_eq, exists_eq_right] + grind split · next heq => simp only [ConfirmRupHintFoldEntailsMotive, h1, imp_self, and_self, hsize, @@ -660,12 +632,8 @@ theorem confirmRupHint_preserves_motive {n : Nat} (f : DefaultFormula n) (rupHin simp only [ConfirmRupHintFoldEntailsMotive, h1, hsize, forall_const, true_and] intro p rcases incompatible_of_reducedToEmpty c acc.1 heq p with pc | pacc - · apply Or.inr - intro pf - simp only [(· ⊨ ·), List.all_eq_true] at pf - specialize pf c c_in_f - simp only [(· ⊨ ·)] at pc - exact pc <| of_decide_eq_true pf + · simp only [(· ⊨ ·)] at pc ⊢ + grind · exact Or.inl pacc · next l b heq => simp only [ConfirmRupHintFoldEntailsMotive] @@ -692,11 +660,7 @@ theorem confirmRupHint_preserves_motive {n : Nat} (f : DefaultFormula n) (rupHin · simp only [pi, decide_false] simp only [hasAssignment, pi, decide_false, ite_false] at pacc by_cases hb : b - · simp only [hasAssignment, ↓reduceIte, addAssignment] - simp only [hb] - simp only [Bool.true_eq_false, decide_false, Bool.false_eq_true, ↓reduceIte, - hasNeg_addPos] - exact pacc + · grind [hasAssignment, addAssignment, hasNeg_addPos] · simp only [Bool.not_eq_true] at hb simp [(· ⊨ ·), hb, Subtype.ext l_eq_i, pi] at plb · simp only [Bool.not_eq_true] at pi @@ -704,15 +668,8 @@ theorem confirmRupHint_preserves_motive {n : Nat} (f : DefaultFormula n) (rupHin simp only [pi, decide_true] at pacc by_cases hb : b · simp [(· ⊨ ·), hb, Subtype.ext l_eq_i, pi] at plb - · simp only [Bool.not_eq_true] at hb - simp only [hasAssignment, addAssignment, hb, ite_false, ite_true, hasPos_addNeg, reduceCtorEq] - simp only [hasAssignment, ite_true] at pacc - exact pacc - · next l_ne_i => - simp only [getElem!_def, Array.size_modify, i_in_bounds, Array.getElem?_eq_getElem, - Array.getElem_modify_of_ne l_ne_i] - simp only [getElem!_def, i_in_bounds, Array.getElem?_eq_getElem] at pacc - exact pacc + · grind [hasAssignment, addAssignment, hasPos_addNeg] + · next l_ne_i => grind · apply And.intro hsize ∘ And.intro h1 simp · apply And.intro hsize ∘ And.intro h1 @@ -782,9 +739,8 @@ theorem sat_of_confirmRupHint_insertRup_fold {n : Nat} (f : DefaultFormula n) simp only [(· ⊨ ·), Bool.not_eq_true] at pv simp only [p_unsat_c] at pv cases pv - · simp [Literal.negate, Bool.not_true] at v'_eq_v - · simp only [formulaEntails_def, List.all_eq_true, decide_eq_true_eq] at pf - exact p_unsat_c <| pf unsat_c unsat_c_in_f + · grind [Literal.negate] + · grind [formulaEntails_def] theorem safe_insert_of_performRupCheck_insertRup {n : Nat} (f : DefaultFormula n) (f_readyForRupAdd : ReadyForRupAdd f) (c : DefaultClause n) (rupHints : Array Nat) : @@ -799,8 +755,7 @@ theorem safe_insert_of_performRupCheck_insertRup {n : Nat} (f : DefaultFormula n rcases c'_in_fc with c'_eq_c | c'_in_f · rw [c'_eq_c] exact sat_of_confirmRupHint_insertRup_fold f f_readyForRupAdd c rupHints p pf performRupCheck_success - · simp only [formulaEntails_def, List.all_eq_true, decide_eq_true_eq] at pf - exact pf c' c'_in_f + · grind [formulaEntails_def] theorem rupAdd_sound {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) (rupHints : Array Nat) (f' : DefaultFormula n) (f_readyForRupAdd : ReadyForRupAdd f) @@ -818,9 +773,9 @@ theorem rupAdd_sound {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) (rup · exact f_limplies_fc · exact limplies_insert f c p · split at rupAddSuccess - · simp at rupAddSuccess + · grind · split at rupAddSuccess - · simp at rupAddSuccess + · grind · next performRupCheck_success => rw [Bool.not_eq_false] at performRupCheck_success have f_limplies_fc := safe_insert_of_performRupCheck_insertRup f f_readyForRupAdd c rupHints performRupCheck_success diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/LRATCheckerSound.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/LRATCheckerSound.lean index c484500d29..eca52b6683 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/LRATCheckerSound.lean +++ b/src/Std/Tactic/BVDecide/LRAT/Internal/LRATCheckerSound.lean @@ -8,6 +8,8 @@ import Std.Tactic.BVDecide.LRAT.Internal.LRATChecker import Std.Tactic.BVDecide.LRAT.Internal.CNF import Std.Tactic.BVDecide.LRAT.Internal.Actions +set_option grind.warning false + namespace Std.Tactic.BVDecide namespace LRAT namespace Internal @@ -18,85 +20,51 @@ theorem addEmptyCaseSound [DecidableEq α] [Clause α β] [Entails α σ] [Formu (f_readyForRupAdd : ReadyForRupAdd f) (rupHints : Array Nat) (rupAddSuccess : (Formula.performRupAdd f Clause.empty rupHints).snd = true) : Unsatisfiable α f := by - let f' := (performRupAdd f empty rupHints).1 - have f'_def := rupAdd_result f empty rupHints f' f_readyForRupAdd - rw [← rupAddSuccess] at f'_def - specialize f'_def rfl - have f_liff_f' := rupAdd_sound f empty rupHints f' f_readyForRupAdd - rw [← rupAddSuccess] at f_liff_f' - specialize f_liff_f' rfl - rw [f'_def] at f_liff_f' intro p pf + let f' := (performRupAdd f empty rupHints).1 + have f'_def : f' = Formula.insert f empty := by grind + have f_liff_f' : Liff α f (Formula.insert f empty) := by grind specialize f_liff_f' p rw [f_liff_f', sat_iff_forall] at pf - have empty_in_f' : empty ∈ toList (Formula.insert f empty) := by - rw [Formula.insert_iff] - exact Or.inl rfl - specialize pf empty empty_in_f' - simp [(· ⊨ ·), Clause.eval, List.any_eq_true, decide_eq_true_eq, Prod.exists, Bool.exists_bool, - empty_eq, List.any_nil] at pf + have empty_in_f' : empty ∈ toList (Formula.insert f empty) := by grind + simp only [(· ⊨ ·)] at pf + grind [Clause.eval] theorem addRupCaseSound [DecidableEq α] [Clause α β] [Entails α σ] [Formula α β σ] (f : σ) (f_readyForRupAdd : ReadyForRupAdd f) (f_readyForRatAdd : ReadyForRatAdd f) (c : β) (f' : σ) (rupHints : Array Nat) (heq : performRupAdd f c rupHints = (f', true)) (restPrf : List (Action β α)) (restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → WellFormedAction a) - (ih : ∀ (f : σ), - ReadyForRupAdd f → ReadyForRatAdd f → (∀ (a : Action β α), a ∈ restPrf → WellFormedAction a) → - lratChecker f restPrf = success → Unsatisfiable α f) + (ih : + ReadyForRupAdd f' → ReadyForRatAdd f' → (∀ (a : Action β α), a ∈ restPrf → WellFormedAction a) → + lratChecker f' restPrf = success → Unsatisfiable α f') (f'_success : lratChecker f' restPrf = success) : Unsatisfiable α f := by - have f'_def := rupAdd_result f c rupHints f' f_readyForRupAdd heq - have f'_readyForRupAdd : ReadyForRupAdd f' := by - rw [f'_def] - exact readyForRupAdd_insert f c f_readyForRupAdd - have f'_readyForRatAdd : ReadyForRatAdd f' := by - rw [f'_def] - exact readyForRatAdd_insert f c f_readyForRatAdd - specialize ih f' f'_readyForRupAdd f'_readyForRatAdd restPrfWellFormed f'_success - have f_liff_f' : Liff α f f' := rupAdd_sound f c rupHints f' f_readyForRupAdd heq - intro p pf - rw [f_liff_f' p] at pf - exact ih p pf + grind [Unsatisfiable, Liff] theorem addRatCaseSound [DecidableEq α] [Clause α β] [Entails α σ] [Formula α β σ] (f : σ) (f_readyForRupAdd : ReadyForRupAdd f) (f_readyForRatAdd : ReadyForRatAdd f) (c : β) (pivot : Literal α) (f' : σ) (rupHints : Array Nat) (ratHints : Array (Nat × Array Nat)) (pivot_limplies_c : Limplies α pivot c) (heq : performRatAdd f c pivot rupHints ratHints = (f', true)) (restPrf : List (Action β α)) (restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → WellFormedAction a) - (ih : ∀ (f : σ), - ReadyForRupAdd f → ReadyForRatAdd f → (∀ (a : Action β α), a ∈ restPrf → WellFormedAction a) → - lratChecker f restPrf = success → Unsatisfiable α f) + (ih : + ReadyForRupAdd f' → ReadyForRatAdd f' → (∀ (a : Action β α), a ∈ restPrf → WellFormedAction a) → + lratChecker f' restPrf = success → Unsatisfiable α f') (f'_success : lratChecker f' restPrf = success) : Unsatisfiable α f := by - rw [limplies_iff_mem] at pivot_limplies_c - have f'_def := ratAdd_result f c pivot rupHints ratHints f' f_readyForRatAdd pivot_limplies_c heq - have f'_readyForRupAdd : ReadyForRupAdd f' := by - rw [f'_def] - exact readyForRupAdd_insert f c f_readyForRupAdd - have f'_readyForRatAdd : ReadyForRatAdd f' := by - rw [f'_def] - exact readyForRatAdd_insert f c f_readyForRatAdd - specialize ih f' f'_readyForRupAdd f'_readyForRatAdd restPrfWellFormed f'_success - have f_equisat_f' : Equisat α f f' := ratAdd_sound f c pivot rupHints ratHints f' f_readyForRatAdd pivot_limplies_c heq - intro p pf - rw [Equisat] at f_equisat_f' - rw [← f_equisat_f'] at ih - exact ih p pf + grind [Equisat, limplies_iff_mem] theorem delCaseSound [DecidableEq α] [Clause α β] [Entails α σ] [Formula α β σ] (f : σ) (f_readyForRupAdd : ReadyForRupAdd f) (f_readyForRatAdd : ReadyForRatAdd f) (ids : Array Nat) (restPrf : List (Action β α)) (restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → WellFormedAction a) - (ih : ∀ (f : σ), - ReadyForRupAdd f → ReadyForRatAdd f → (∀ (a : Action β α), a ∈ restPrf → WellFormedAction a) → - lratChecker f restPrf = success → Unsatisfiable α f) + (ih : + ReadyForRupAdd (delete f ids) → ReadyForRatAdd (delete f ids) → (∀ (a : Action β α), a ∈ restPrf → WellFormedAction a) → + lratChecker (delete f ids) restPrf = success → Unsatisfiable α (delete f ids)) (h : lratChecker (Formula.delete f ids) restPrf = success) : Unsatisfiable α f := by intro p pf - have f_del_readyForRupAdd : ReadyForRupAdd (Formula.delete f ids) := readyForRupAdd_delete f ids f_readyForRupAdd - have f_del_readyForRatAdd : ReadyForRatAdd (Formula.delete f ids) := readyForRatAdd_delete f ids f_readyForRatAdd - exact ih (delete f ids) f_del_readyForRupAdd f_del_readyForRatAdd restPrfWellFormed h p (limplies_delete p pf) + exact ih (by grind) (by grind) restPrfWellFormed h p (limplies_delete p pf) theorem lratCheckerSound [DecidableEq α] [Clause α β] [Entails α σ] [Formula α β σ] (f : σ) (f_readyForRupAdd : ReadyForRupAdd f) (f_readyForRatAdd : ReadyForRatAdd f) @@ -104,48 +72,10 @@ theorem lratCheckerSound [DecidableEq α] [Clause α β] [Entails α σ] [Formul lratChecker f prf = success → Unsatisfiable α f := by induction prf generalizing f · unfold lratChecker - simp [false_implies] - · next action restPrf ih => - simp only [List.find?, List.mem_cons, forall_eq_or_imp] at prfWellFormed - rcases prfWellFormed with ⟨actionWellFormed, restPrfWellFormed⟩ + grind + · simp only [List.mem_cons, forall_eq_or_imp] at prfWellFormed unfold lratChecker - split - · intro h - exfalso - simp at h - · next id rupHints restPrf' _ => - simp [ite_eq_left_iff, Bool.not_eq_true] - intro rupAddSuccess - exact addEmptyCaseSound f f_readyForRupAdd rupHints rupAddSuccess - · next id c rupHints restPrf' hprf => - split - next f' checkSuccess heq => - split - · next hCheckSuccess => - intro f'_success - simp only [List.cons.injEq] at hprf - rw [← hprf.2] at f'_success - rw [hCheckSuccess] at heq - exact addRupCaseSound f f_readyForRupAdd f_readyForRatAdd c f' rupHints heq restPrf restPrfWellFormed ih f'_success - · simp [false_implies] - · next id c pivot rupHints ratHints restPrf' hprf => - split - next f' checkSuccess heq => - split - · next hCheckSuccess => - intro f'_success - simp only [List.cons.injEq] at hprf - rw [← hprf.2] at f'_success - rw [hCheckSuccess] at heq - simp only [WellFormedAction, hprf.1] at actionWellFormed - exact addRatCaseSound f f_readyForRupAdd f_readyForRatAdd c pivot f' rupHints ratHints actionWellFormed heq restPrf - restPrfWellFormed ih f'_success - · simp [false_implies] - · next ids restPrf' hprf => - intro h - simp only [List.cons.injEq] at hprf - rw [← hprf.2] at h - exact delCaseSound f f_readyForRupAdd f_readyForRatAdd ids restPrf restPrfWellFormed ih h + grind [addEmptyCaseSound, addRupCaseSound, addRatCaseSound, delCaseSound, WellFormedAction] end Internal end LRAT