diff --git a/.gitignore b/.gitignore index 5b1b1f7d..7d4017d5 100644 --- a/.gitignore +++ b/.gitignore @@ -1,2 +1,3 @@ /.lake .DS_Store +/build \ No newline at end of file diff --git a/LeanSAT/LRAT/Clause.lean b/LeanSAT/LRAT/Clause.lean index 2ef1af23..03573048 100644 --- a/LeanSAT/LRAT/Clause.lean +++ b/LeanSAT/LRAT/Clause.lean @@ -111,7 +111,7 @@ def empty {n : Nat} : DefaultClause n := have nodup := by simp only [List.nodup_nil] ⟨clause, nodupkey, nodup⟩ -theorem empty_eq {n : Nat} : toList (empty : DefaultClause n) = [] := by rfl +theorem empty_eq {n : Nat} : toList (empty : DefaultClause n) = [] := rfl def unit {n : Nat} (l : Literal (PosFin n)) : DefaultClause n := let clause := [l] @@ -127,7 +127,7 @@ def unit {n : Nat} (l : Literal (PosFin n)) : DefaultClause n := have nodup : List.Nodup clause:= by simp ⟨clause, nodupkey, nodup⟩ -theorem unit_eq {n : Nat} (l : Literal (PosFin n)) : toList (unit l) = [l] := by rfl +theorem unit_eq {n : Nat} (l : Literal (PosFin n)) : toList (unit l) = [l] := rfl def isUnit {n : Nat} (c : DefaultClause n) : Option (Literal (PosFin n)) := match c.clause with @@ -146,7 +146,7 @@ theorem isUnit_iff {n : Nat} (c : DefaultClause n) (l : Literal (PosFin n)) : def negate {n : Nat} (c : DefaultClause n) : List (Literal (PosFin n)) := c.clause.map negateLiteral -theorem negate_iff {n : Nat} (c : DefaultClause n) : negate c = (toList c).map negateLiteral := by rfl +theorem negate_iff {n : Nat} (c : DefaultClause n) : negate c = (toList c).map negateLiteral := rfl /-- Attempts to add the literal (idx, b) to clause c. Returns none if doing so would make c a tautology -/ def insert {n : Nat} (c : DefaultClause n) (l : Literal (PosFin n)) : Option (DefaultClause n) := @@ -230,7 +230,7 @@ theorem ofArray_eq (arr : Array (Literal (PosFin n))) (arrNodup : ∀ i : Fin ar split at heq . simp only at heq . next acc => - specialize ih acc (by rfl) + specialize ih acc rfl rcases ih with ⟨hsize, ih⟩ simp only at ih simp only [insert] at heq diff --git a/LeanSAT/LRAT/Formula/Basic.lean b/LeanSAT/LRAT/Formula/Basic.lean index 3dc2824b..c1266622 100644 --- a/LeanSAT/LRAT/Formula/Basic.lean +++ b/LeanSAT/LRAT/Formula/Basic.lean @@ -36,8 +36,7 @@ def assignments_invariant {n : Nat} (f : DefaultFormula n) : Prop := theorem assignments_invariant_of_strong_assignments_invariant {n : Nat} (f : DefaultFormula n) : strong_assignments_invariant f → assignments_invariant f := by - intro h - rcases h with ⟨hsize, h⟩ + intro ⟨hsize, h⟩ apply Exists.intro hsize intro i b hb p pf specialize h i b hb @@ -131,7 +130,7 @@ theorem ofArray_readyForRupAdd {n : Nat} (arr : Array (Option (DefaultClause n)) simp only [toList, ofArray, Array.toList_eq, List.map, List.append_nil, List.mem_filterMap, id_eq, exists_eq_right] have i_eq_l : i = l := Subtype.ext i_eq_l simp only [unit, b_eq_true, i_eq_l] - have c_def : c = ⟨c.clause, c.nodupkey, c.nodup⟩ := by rfl + 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 @@ -165,7 +164,7 @@ theorem ofArray_readyForRupAdd {n : Nat} (arr : Array (Option (DefaultClause n)) simp only [toList, ofArray, Array.toList_eq, List.map, List.append_nil, List.mem_filterMap, id_eq, exists_eq_right] have i_eq_l : i = l := Subtype.ext i_eq_l simp only [unit, b_eq_false, i_eq_l] - have c_def : c = ⟨c.clause, c.nodupkey, c.nodup⟩ := by rfl + 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 @@ -245,7 +244,7 @@ theorem insert_readyForRupAdd {n : Nat} (f : DefaultFormula n) (c : DefaultClaus intro f_readyForRupAdd simp only [insert] split - . apply And.intro f_readyForRupAdd.1 ∘ Exists.intro f_readyForRupAdd.2.1 + . refine ⟨f_readyForRupAdd.1, f_readyForRupAdd.2.1, ?_⟩ intro i b hb have hf := f_readyForRupAdd.2.2 i b hb simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq, exists_eq_right, @@ -258,7 +257,7 @@ theorem insert_readyForRupAdd {n : Nat} (f : DefaultFormula n) (c : DefaultClaus . next l hc => have hsize : (Array.modify f.assignments l.1 addPosAssignment).size = n := by rw [Array.modify_preserves_size, f_readyForRupAdd.2.1] - apply And.intro f_readyForRupAdd.1 ∘ Exists.intro hsize + refine ⟨f_readyForRupAdd.1, hsize, ?_⟩ intro i b hb have hf := f_readyForRupAdd.2.2 i b have i_in_bounds : i.1 < f.assignments.size := by rw [f_readyForRupAdd.2.1]; exact i.2.2 @@ -299,7 +298,7 @@ theorem insert_readyForRupAdd {n : Nat} (f : DefaultFormula n) (c : DefaultClaus . next l hc => have hsize : (Array.modify f.assignments l.1 addNegAssignment).size = n := by rw [Array.modify_preserves_size, f_readyForRupAdd.2.1] - apply And.intro f_readyForRupAdd.1 ∘ Exists.intro hsize + refine ⟨f_readyForRupAdd.1, hsize, ?_⟩ intro i b hb have hf := f_readyForRupAdd.2.2 i b have i_in_bounds : i.1 < f.assignments.size := by rw [f_readyForRupAdd.2.1]; exact i.2.2 @@ -319,8 +318,7 @@ theorem insert_readyForRupAdd {n : Nat} (f : DefaultFormula n) (c : DefaultClaus . next l_eq_i => have b_eq_false : b = true := by by_cases b = true - . next b_eq_true => - exact b_eq_true + . 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.get_modify_at_idx i_in_bounds, ite_true, hasPos_of_addNeg] at hb @@ -341,9 +339,7 @@ theorem insert_readyForRatAdd {n : Nat} (f : DefaultFormula n) (c : DefaultClaus readyForRatAdd f → readyForRatAdd (insert f c) := by intro h constructor - . simp only [insert, h.1] - split - repeat { rfl } + . simp only [insert, h.1] <;> split <;> rfl . exact insert_readyForRupAdd f c h.2 theorem mem_of_insertRupUnits {n : Nat} (f : DefaultFormula n) (units : List (Literal (PosFin n))) @@ -388,9 +384,8 @@ theorem mem_of_insertRatUnits {n : Nat} (f : DefaultFormula n) (units : List (Li simp only [toList, insertRatUnits, Prod.mk.eta, Array.toList_eq, List.append_assoc, List.mem_append, 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.ratUnits, f.assignments, false).1.data → (l ∈ f.ratUnits.data ∨ l ∈ units) := by - intro l hl - exact Or.inl hl + have hb : ∀ l : Literal (PosFin n), l ∈ (f.ratUnits, f.assignments, false).1.data → (l ∈ f.ratUnits.data ∨ l ∈ units) := + fun _ => Or.inl have hl (acc : Array (Literal (PosFin n)) × Array Assignment × Bool) (ih : ∀ l : Literal (PosFin n), l ∈ acc.1.data → l ∈ f.ratUnits.data ∨ l ∈ units) (unit : Literal (PosFin n)) (unit_in_units : unit ∈ units) : @@ -482,7 +477,7 @@ theorem deleteOne_preserves_strong_assignments_invariant {n : Nat} (f : DefaultF . next id_eq_idx => exfalso have idx_in_bounds2 : idx.1 < f.clauses.size := by - have f_clauses_rw : f.clauses = { data := f.clauses.data } := by rfl + have f_clauses_rw : f.clauses = { data := f.clauses.data } := rfl conv => rhs; rw [f_clauses_rw, Array.size_mk] exact idx.2 simp only [getElem!, id_eq_idx, idx_in_bounds2, dite_true, Array.getElem_eq_data_get] at heq @@ -519,7 +514,7 @@ theorem deleteOne_preserves_strong_assignments_invariant {n : Nat} (f : DefaultF . next id_eq_idx => exfalso have idx_in_bounds2 : idx.1 < f.clauses.size := by - have f_clauses_rw : f.clauses = { data := f.clauses.data } := by rfl + have f_clauses_rw : f.clauses = { data := f.clauses.data } := rfl conv => rhs; rw [f_clauses_rw, Array.size_mk] exact idx.2 simp only [getElem!, id_eq_idx, idx_in_bounds2, dite_true, Array.getElem_eq_data_get] at heq @@ -580,7 +575,7 @@ theorem deleteOne_preserves_strong_assignments_invariant {n : Nat} (f : DefaultF . next id_eq_idx => exfalso have idx_in_bounds2 : idx.1 < f.clauses.size := by - have f_clauses_rw : f.clauses = { data := f.clauses.data } := by rfl + have f_clauses_rw : f.clauses = { data := f.clauses.data } := rfl conv => rhs; rw [f_clauses_rw, Array.size_mk] exact idx.2 simp only [getElem!, id_eq_idx, idx_in_bounds2, dite_true, Array.getElem_eq_data_get] at heq @@ -631,27 +626,9 @@ 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 - . 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 [Array.toList_eq, List.mem_filterMap, id_eq, exists_eq_right] at h1 - simp only [Array.toList_eq, List.mem_filterMap, id_eq, exists_eq_right] - rw [Array.set!, Array.setD] at h1 - split at h1 - . simp only [Array.data_set] at h1 - rcases List.get_of_mem h1 with ⟨i, h4⟩ - rw [List.get_set] at h4 - split at h4 - . exact False.elim h4 - . rw [← h4] - apply List.get_mem - . exact h1 - . exact (Or.inr ∘ Or.inl) h1 - . exact (Or.inr ∘ Or.inr) h1 - . rw [toList, List.mem_append, List.mem_append, or_assoc] at 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 diff --git a/LeanSAT/LRAT/Formula/Implementation.lean b/LeanSAT/LRAT/Formula/Implementation.lean index 5d649a39..805bf284 100644 --- a/LeanSAT/LRAT/Formula/Implementation.lean +++ b/LeanSAT/LRAT/Formula/Implementation.lean @@ -61,7 +61,7 @@ instance {n : Nat} : Inhabited (DefaultFormula n) where def toList {n : Nat} (f : DefaultFormula n) : List (DefaultClause n) := (f.clauses.toList.filterMap id) ++ (f.rupUnits.toList.map unit) ++ (f.ratUnits.toList.map unit) -def ofArray_fold_fn : Array Assignment → Option (DefaultClause n) → Array Assignment := fun assignments cOpt => +def ofArray_fold_fn (assignments : Array Assignment) (cOpt : Option (DefaultClause n)) : Array Assignment := match cOpt with | none => assignments | some c => @@ -77,17 +77,14 @@ def ofArray {n : Nat} (clauses : Array (Option (DefaultClause n))) : DefaultForm ⟨clauses, #[], #[], assignments⟩ def insert {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) : DefaultFormula n := - match f with - | ⟨clauses, rupUnits, ratUnits, assignments⟩ => - match isUnit c with + let ⟨clauses, rupUnits, ratUnits, assignments⟩ := f + match isUnit c with | none => ⟨clauses.push c, rupUnits, ratUnits, assignments⟩ | some (l, true) => ⟨clauses.push c, rupUnits, ratUnits, assignments.modify l addPosAssignment⟩ | some (l, false) => ⟨clauses.push c, rupUnits, ratUnits, assignments.modify l addNegAssignment⟩ - def deleteOne {n : Nat} (f : DefaultFormula n) (id : Nat) : DefaultFormula n := - match f with - | ⟨clauses, rupUnits, ratUnits, assignments⟩ => - match clauses[id]! with + let ⟨clauses, rupUnits, ratUnits, assignments⟩ := f + match clauses[id]! with | none => ⟨clauses, rupUnits, ratUnits, assignments⟩ | some ⟨[l], _, _⟩ => ⟨clauses.set! id none, rupUnits, ratUnits, assignments.modify l.1 (removeAssignment l.2)⟩ | some _ => ⟨clauses.set! id none, rupUnits, ratUnits, assignments⟩ @@ -112,32 +109,28 @@ def insertUnit : Array (Literal (PosFin n)) × Array Assignment × Bool → /-- Returns an updated formula f and a bool which indicates whether a contradiction was found in the process of updating f -/ def insertRupUnits {n : Nat} (f : DefaultFormula n) (ls : List (Literal (PosFin n))) : DefaultFormula n × Bool := - match f with - | ⟨clauses, rupUnits, ratUnits, assignments⟩ => - let (rupUnits, assignments, foundContradiction) := ls.foldl insertUnit (rupUnits, assignments, false) - (⟨clauses, rupUnits, ratUnits, assignments⟩, foundContradiction) + let ⟨clauses, rupUnits, ratUnits, assignments⟩ := f + let (rupUnits, assignments, foundContradiction) := ls.foldl insertUnit (rupUnits, assignments, false) + (⟨clauses, rupUnits, ratUnits, assignments⟩, foundContradiction) /-- Returns an updated formula f and a bool which indicates whether a contradiction was found in the process of updating f -/ def insertRatUnits {n : Nat} (f : DefaultFormula n) (ls : List (Literal (PosFin n))) : DefaultFormula n × Bool := - match f with - | ⟨clauses, rupUnits, ratUnits, assignments⟩ => - let (ratUnits, assignments, foundContradiction) := ls.foldl insertUnit (ratUnits, assignments, false) - (⟨clauses, rupUnits, ratUnits, assignments⟩, foundContradiction) + let ⟨clauses, rupUnits, ratUnits, assignments⟩ := f + let (ratUnits, assignments, foundContradiction) := ls.foldl insertUnit (ratUnits, assignments, false) + (⟨clauses, rupUnits, ratUnits, assignments⟩, foundContradiction) def clearUnit : Array Assignment → Literal (PosFin n) → Array Assignment | assignments, (l, b) => assignments.modify l (removeAssignment b) def clearRupUnits {n : Nat} (f : DefaultFormula n) : DefaultFormula n := - match f with - | ⟨clauses, rupUnits, ratUnits, assignments⟩ => - let assignments := rupUnits.foldl clearUnit assignments - ⟨clauses, #[], ratUnits, assignments⟩ + let ⟨clauses, rupUnits, ratUnits, assignments⟩ := f + let assignments := rupUnits.foldl clearUnit assignments + ⟨clauses, #[], ratUnits, assignments⟩ def clearRatUnits {n : Nat} (f : DefaultFormula n) : DefaultFormula n := - match f with - | ⟨clauses, rupUnits, ratUnits, assignments⟩ => - let assignments := ratUnits.foldl clearUnit assignments - ⟨clauses, rupUnits, #[], assignments⟩ + let ⟨clauses, rupUnits, ratUnits, assignments⟩ := f + let assignments := ratUnits.foldl clearUnit assignments + ⟨clauses, rupUnits, #[], assignments⟩ /-- Reverts assignments to the array it was prior to adding derivedLits -/ def restoreAssignments {n : Nat} (assignments : Array Assignment) (derivedLits : List (PosFin n × Bool)) : @@ -174,10 +167,9 @@ def confirmRupHint {n : Nat} (clauses : Array (Option (DefaultClause n))) : Arra Note: This function assumes that any rupUnits and ratUnits corresponding to this rup check have already been added to f. -/ def performRupCheck {n : Nat} (f : DefaultFormula n) (rupHints : Array Nat) : DefaultFormula n × List (Literal (PosFin n)) × Bool × Bool := - match f with - | ⟨clauses, rupUnits, ratUnits, assignments⟩ => - let (assignments, derivedLits, derivedEmpty, encounteredError) := rupHints.foldl (confirmRupHint clauses) (assignments, [], false, false) - (⟨clauses, rupUnits, ratUnits, assignments⟩, derivedLits, derivedEmpty, encounteredError) + let ⟨clauses, rupUnits, ratUnits, assignments⟩ := f + let (assignments, derivedLits, derivedEmpty, encounteredError) := rupHints.foldl (confirmRupHint clauses) (assignments, [], false, false) + (⟨clauses, rupUnits, ratUnits, assignments⟩, derivedLits, derivedEmpty, encounteredError) /-- Attempts to verify that c can be added to f via unit propagation. If it can, it returns ((f.insert c), true). If it can't, it returns false as the second part of the tuple (and no guarantees are made about what formula is returned) -/ @@ -192,13 +184,12 @@ def performRupAdd {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) (rupHin if encounteredError then (f, false) else if not derivedEmpty then (f, false) else -- derivedEmpty is true and encounteredError is false - match f with - | ⟨clauses, rupUnits, ratUnits, assignments⟩ => - let assignments := restoreAssignments assignments derivedLits - -- assignments should now be the same as it was before the performRupCheck call - let f := clearRupUnits ⟨clauses, rupUnits, ratUnits, assignments⟩ - -- f should now be the same as it was before insertRupUnits - (f.insert c, true) + let ⟨clauses, rupUnits, ratUnits, assignments⟩ := f + let assignments := restoreAssignments assignments derivedLits + -- assignments should now be the same as it was before the performRupCheck call + let f := clearRupUnits ⟨clauses, rupUnits, ratUnits, assignments⟩ + -- f should now be the same as it was before insertRupUnits + (f.insert c, true) /-- Returns an array of indices corresponding to clauses that contain the negation of l -/ def getRatClauseIndices {n : Nat} (clauses : Array (Option (DefaultClause n))) (l : Literal (PosFin n)) : Array Nat := diff --git a/LeanSAT/LRAT/Formula/RatAddResult.lean b/LeanSAT/LRAT/Formula/RatAddResult.lean index c8564c7b..0b899f2b 100644 --- a/LeanSAT/LRAT/Formula/RatAddResult.lean +++ b/LeanSAT/LRAT/Formula/RatAddResult.lean @@ -149,7 +149,7 @@ theorem performRatCheck_preserves_formula {n : Nat} (f : DefaultFormula n) (hf : ⟨(insertRatUnits f (negate (DefaultClause.delete c p))).1.clauses, (insertRatUnits f (negate (DefaultClause.delete c p))).1.rupUnits, (insertRatUnits f (negate (DefaultClause.delete c p))).1.ratUnits, - (insertRatUnits f (negate (DefaultClause.delete c p))).1.assignments⟩ := by rfl + (insertRatUnits f (negate (DefaultClause.delete c p))).1.assignments⟩ := rfl simp only [performRupCheck_preserves_clauses, performRupCheck_preserves_rupUnits, performRupCheck_preserves_ratUnits] rw [restoreAssignments_performRupCheck fc fc_assignments_size ratHint.2, ← insertRatUnits_rw, clear_insertRat f hf (negate (DefaultClause.delete c p))] @@ -165,7 +165,7 @@ theorem performRatCheck_fold_preserves_formula {n : Nat} (f : DefaultFormula n) else (x.1, false)) (f, true) 0 ratHints.size performRatCheck_fold_res.1 = f := by let motive (_idx : Nat) (acc : DefaultFormula n × Bool) := acc.1 = f - have h_base : motive 0 (f, true) := by rfl + 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 intro ih @@ -207,7 +207,7 @@ theorem ratAdd_result {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) (p exact And.intro f_readyForRatAdd.1 hsize have insertRupUnits_rw : (insertRupUnits f (negate c)).1 = ⟨(insertRupUnits f (negate c)).1.clauses, (insertRupUnits f (negate c)).1.rupUnits, - (insertRupUnits f (negate c)).1.ratUnits, (insertRupUnits f (negate c)).1.assignments⟩ := by rfl + (insertRupUnits f (negate c)).1.ratUnits, (insertRupUnits f (negate c)).1.assignments⟩ := rfl simp only [performRatCheck_fold_preserves_formula performRupCheck_res h_performRupCheck_res (negateLiteral p) ratHints, performRupCheck_preserves_clauses, performRupCheck_preserves_rupUnits, performRupCheck_preserves_ratUnits, restoreAssignments_performRupCheck fc fc_assignments_size, ← insertRupUnits_rw, diff --git a/LeanSAT/LRAT/Formula/RatAddSound.lean b/LeanSAT/LRAT/Formula/RatAddSound.lean index 88b7411e..c9fdcd20 100644 --- a/LeanSAT/LRAT/Formula/RatAddSound.lean +++ b/LeanSAT/LRAT/Formula/RatAddSound.lean @@ -84,7 +84,7 @@ theorem insertRatUnits_preserves_assignments_invariant {n : Nat} (f : DefaultFor by_cases b = b' . next b_eq_b' => let j_unit := unit (insertRatUnits f units).1.ratUnits[j] - have j_unit_def : j_unit = unit (insertRatUnits f units).1.ratUnits[j] := by rfl + have j_unit_def : j_unit = unit (insertRatUnits f units).1.ratUnits[j] := rfl have j_unit_in_insertRatUnits_res : ∃ i : PosFin n, (i, false) ∈ (insertRatUnits f units).1.ratUnits.data ∧ unit (i, false) = j_unit ∨ @@ -132,7 +132,7 @@ theorem insertRatUnits_preserves_assignments_invariant {n : Nat} (f : DefaultFor have b'_def : b' = (decide ¬b = true) := by cases b <;> cases b' <;> simp at * rw [has_iff_has_of_add_complement, ← b'_def, hb] . let j1_unit := unit (insertRatUnits f units).1.ratUnits[j1] - have j1_unit_def : j1_unit = unit (insertRatUnits f units).1.ratUnits[j1] := by rfl + have j1_unit_def : j1_unit = unit (insertRatUnits f units).1.ratUnits[j1] := rfl have j1_unit_in_insertRatUnits_res : ∃ i : PosFin n, (i, false) ∈ (insertRatUnits f units).1.ratUnits.data ∧ unit (i, false) = j1_unit ∨ @@ -149,7 +149,7 @@ theorem insertRatUnits_preserves_assignments_invariant {n : Nat} (f : DefaultFor apply Array.getElem_mem_data . rfl let j2_unit := unit (insertRatUnits f units).1.ratUnits[j2] - have j2_unit_def : j2_unit = unit (insertRatUnits f units).1.ratUnits[j2] := by rfl + have j2_unit_def : j2_unit = unit (insertRatUnits f units).1.ratUnits[j2] := rfl have j2_unit_in_insertRatUnits_res : ∃ i : PosFin n, (i, false) ∈ (insertRatUnits f units).1.ratUnits.data ∧ unit (i, false) = j2_unit ∨ @@ -252,7 +252,7 @@ theorem insertRat_entails_hsat {n : Nat} (f : DefaultFormula n) (hf : f.ratUnits simp only [getElem_fin, ne_eq, true_and, Bool.not_eq_true, exists_and_right] apply Or.inl intro j - simp only [hf.1, Array.size_toArray, List.length_nil] at j + rw [hf.1] at j exact Fin.elim0 j have insertUnit_fold_satisfies_invariant := insertUnit_fold_preserves_invariant f.assignments hf.2.1 f.ratUnits f.assignments hf.2.1 false (negate c) h0 @@ -269,7 +269,7 @@ theorem insertRat_entails_hsat {n : Nat} (f : DefaultFormula n) (hf : f.ratUnits . simp only [HSat.eval, List.any_eq_true, Prod.exists, Bool.exists_bool, Bool.decide_coe] apply Exists.intro i have ib_in_insertUnit_fold : (i, b) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) (negate c)).1.data := by - have i_rw : i = ⟨i.1, i.2⟩ := by rfl + have i_rw : i = ⟨i.1, i.2⟩ := rfl rw [i_rw, ← h1] apply List.get_mem have ib_in_insertUnit_fold := mem_insertUnit_fold_units f.ratUnits f.assignments false (negate c) (i, b) ib_in_insertUnit_fold @@ -314,11 +314,11 @@ theorem insertRat_entails_hsat {n : Nat} (f : DefaultFormula n) (hf : f.ratUnits . simp only at h2 . exfalso have i_true_in_insertUnit_fold : (i, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) (negate c)).1.data := by - have i_rw : i = ⟨i.1, i.2⟩ := by rfl + have i_rw : i = ⟨i.1, i.2⟩ := rfl rw [i_rw, ← h1] apply List.get_mem have i_false_in_insertUnit_fold : (i, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) (negate c)).1.data := by - have i_rw : i = ⟨i.1, i.2⟩ := by rfl + have i_rw : i = ⟨i.1, i.2⟩ := rfl rw [i_rw, ← h2] apply List.get_mem simp only [hf.1, negate, negateLiteral] at i_true_in_insertUnit_fold i_false_in_insertUnit_fold @@ -411,7 +411,7 @@ theorem performRatCheck_success_entails_c_without_negPivot {n : Nat} (f : Defaul Bool.decide_coe, List.all_eq_true] at pfc have c_negPivot_in_fc : (DefaultClause.delete c negPivot) ∈ toList (insert f (DefaultClause.delete c negPivot)) := by rw [insert_iff] - exact Or.inl (by rfl) + exact Or.inl rfl exact of_decide_eq_true $ pfc (DefaultClause.delete c negPivot) c_negPivot_in_fc theorem existsRatHint_of_ratHintsExhaustive {n : Nat} (f : DefaultFormula n) (f_readyForRatAdd : readyForRatAdd f) @@ -434,7 +434,7 @@ theorem existsRatHint_of_ratHintsExhaustive {n : Nat} (f : DefaultFormula n) (f_ have h : i.1 ∈ (ratHints.map (fun x => x.1)).data := by rw [← of_decide_eq_true ratHintsExhaustive_eq_true] have i_eq_range_i : i.1 = (Array.range f.clauses.size)[i.1]'i_in_bounds := by - have f_clauses_rw : f.clauses = { data := f.clauses.data } := by rfl + have f_clauses_rw : f.clauses = { data := f.clauses.data } := rfl rw [Array.range_idx] conv => rhs; rw [f_clauses_rw, Array.size] exact i.2 @@ -470,7 +470,7 @@ theorem performRatCheck_success_of_performRatCheck_fold_success {n : Nat} (f : D let fold_fn (acc : DefaultFormula n × Bool) (ratHint : Nat × Array Nat) := if acc.2 = true then performRatCheck acc.1 p ratHint else (acc.1, false) have fold_fn_def (acc : DefaultFormula n × Bool) (ratHint : Nat × Array Nat) : - fold_fn acc ratHint = if acc.2 = true then performRatCheck acc.1 p ratHint else (acc.1, false) := by rfl + fold_fn acc ratHint = if acc.2 = true then performRatCheck acc.1 p ratHint else (acc.1, false) := rfl have h_inductive (idx : Fin ratHints.size) (acc : DefaultFormula n × Bool) (ih : motive idx.1 acc) : motive (idx.1 + 1) (fold_fn acc ratHints[idx]) := by constructor @@ -526,7 +526,7 @@ theorem performRatCheck_fold_success_entails_safe_insert {n : Nat} (f : DefaultF exact pc' $ pf c' c'_in_f . rw [← Clause.limplies_iff_mem] at pivot_in_c let p' : (PosFin n) → Bool := fun a => if a = pivot.1 then pivot.2 else p a - have p'_rw : p' = (fun a => if a = pivot.1 then pivot.2 else p a) := by rfl + have p'_rw : p' = (fun a => if a = pivot.1 then pivot.2 else p a) := rfl have p'_entails_c : p' ⊨ c := by specialize pivot_in_c p' simp only [instHSatLiteral._eq_1, HSat.eval._eq_1, ite_eq_left_iff, not_true, false_implies, forall_const] at pivot_in_c diff --git a/LeanSAT/LRAT/Formula/RupAddResult.lean b/LeanSAT/LRAT/Formula/RupAddResult.lean index 047cdfa6..03399156 100644 --- a/LeanSAT/LRAT/Formula/RupAddResult.lean +++ b/LeanSAT/LRAT/Formula/RupAddResult.lean @@ -95,8 +95,7 @@ theorem insertUnit_preserves_invariant {n : Nat} (assignments0 : Array Assignmen 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 - apply Exists.intro mostRecentUnitIdx ∘ Exists.intro l.2 - apply Exists.intro i_gt_zero + refine ⟨mostRecentUnitIdx, l.2, i_gt_zero, ?_⟩ simp only [insertUnit, h3, Prod.mk.eta, ite_false, Array.get_push_eq, i_eq_l] constructor . conv => lhs; rw [← @Prod.mk.eta (PosFin n) Bool l] @@ -139,10 +138,9 @@ theorem insertUnit_preserves_invariant {n : Nat} (assignments0 : Array Assignmen have j_lt_updatedUnits_size : j.1 < (insertUnit (units, assignments, foundContradiction) l).1.size := by simp only [insertUnit, h5, Prod.mk.eta, ite_true] exact j.2 - apply Exists.intro ⟨j.1, j_lt_updatedUnits_size⟩ - apply Exists.intro b ∘ Exists.intro i_gt_zero + refine ⟨⟨j.1, j_lt_updatedUnits_size⟩, b,i_gt_zero, ?_⟩ simp only [insertUnit, h5, Prod.mk.eta, ite_true] - apply And.intro h1 ∘ And.intro h2 ∘ And.intro h3 + refine ⟨h1,h2,h3,?_⟩ intro k k_ne_j have k_size : k.1 < units.size := by have k_property := k.2 @@ -174,8 +172,7 @@ theorem insertUnit_preserves_invariant {n : Nat} (assignments0 : Array Assignmen rw [hl, ← i_eq_l, assignments_i_rw, h2] at h5 exact h5 (has_of_add _ true) | true, false => - apply Exists.intro ⟨j.1, j_lt_updatedUnits_size⟩ - apply Exists.intro mostRecentUnitIdx ∘ Exists.intro i_gt_zero + refine ⟨⟨j.1, j_lt_updatedUnits_size⟩, mostRecentUnitIdx, i_gt_zero, ?_⟩ simp only [insertUnit, h5, Prod.mk.eta, ite_false, Array.get_push_eq, ne_eq] constructor . rw [Array.get_push_lt units l j.1 j.2, h1] @@ -208,13 +205,12 @@ theorem insertUnit_preserves_invariant {n : Nat} (assignments0 : Array Assignmen . exfalso have k_property := k.2 simp only [insertUnit, h5, Prod.mk.eta, ite_false, Array.size_push] 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 + rcases Nat.lt_or_eq_of_le <| Nat.le_of_lt_succ k_property with k_lt_units_size | k_eq_units_size . exact h k_lt_units_size . simp only [← k_eq_units_size, not_true] at k_ne_l exact k_ne_l rfl | false, true => - apply Exists.intro mostRecentUnitIdx ∘ Exists.intro ⟨j.1, j_lt_updatedUnits_size⟩ - apply Exists.intro i_gt_zero + refine ⟨mostRecentUnitIdx, ⟨j.1, j_lt_updatedUnits_size⟩, i_gt_zero, ?_⟩ simp only [insertUnit, h5, Prod.mk.eta, ite_false, Array.get_push_eq, ne_eq] constructor . simp only [i_eq_l, ← hl] @@ -261,8 +257,7 @@ theorem insertUnit_preserves_invariant {n : Nat} (assignments0 : Array Assignmen have j_lt_updatedUnits_size : j.1 < (insertUnit (units, assignments, foundContradiction) l).1.size := by simp only [insertUnit, h5, Prod.mk.eta, ite_false, Array.size_push] exact Nat.lt_trans j.2 (Nat.lt_succ_self units.size) - apply Exists.intro ⟨j.1, j_lt_updatedUnits_size⟩ - apply Exists.intro b ∘ Exists.intro i_gt_zero + refine ⟨⟨j.1, j_lt_updatedUnits_size⟩, b,i_gt_zero, ?_⟩ simp only [insertUnit, h5, Prod.mk.eta, ite_false] constructor . rw [Array.get_push_lt units l j.1 j.2, h1] @@ -293,9 +288,7 @@ theorem insertUnit_preserves_invariant {n : Nat} (assignments0 : Array Assignmen . exact j2.2 . simp only [Array.size_push] exact Nat.lt_trans j2.2 (Nat.lt_succ_self units.size) - apply Or.inr ∘ Or.inr ∘ Exists.intro ⟨j1.1, j1_lt_updatedUnits_size⟩ - apply Exists.intro ⟨j2.1, j2_lt_updatedUnits_size⟩ - apply Exists.intro i_gt_zero + refine Or.inr <| Or.inr <| ⟨⟨j1.1, j1_lt_updatedUnits_size⟩, ⟨j2.1, j2_lt_updatedUnits_size⟩, i_gt_zero, ?_⟩ simp only [insertUnit, Prod.mk.eta] constructor . split @@ -470,7 +463,7 @@ theorem clearUnit_preserves_size (assignments : Array Assignment) (l : Literal ( theorem clearUnit_foldl_preserves_size {α : Type u} (assignments : Array Assignment) (f : Array Assignment → α → Array Assignment) (f_preserves_size : ∀ arr : Array Assignment, ∀ a : α, (f arr a).size = arr.size) (l : List α) : Array.size (List.foldl f assignments l) = Array.size assignments := by - have hb : assignments.size = assignments.size := by rfl + have hb : assignments.size = assignments.size := rfl have hl (assignments' : Array Assignment) (hsize : assignments'.size = assignments.size) (a : α) (_ : a ∈ l) : (f assignments' a).size = assignments.size := by rw [f_preserves_size assignments' a, hsize] exact List.foldlRecOn l f assignments hb hl @@ -478,9 +471,7 @@ theorem clearUnit_foldl_preserves_size {α : Type u} (assignments : Array Assign def clear_insert_induction_motive {n : Nat} (f : DefaultFormula n) (assignments_size : f.assignments.size = n) (units : Array (Literal (PosFin n))) : Nat → Array Assignment → Prop := fun idx assignments => ∃ hsize : assignments.size = n, ∀ i : Fin n, - have i_lt_assignments_size : i.1 < assignments.size := by - rw [hsize] - exact i.2 + have i_lt_assignments_size : i.1 < assignments.size := hsize ▸ i.2 have i_lt_f_assignments_size : i.1 < f.assignments.size := by rw [assignments_size] exact i.2 @@ -554,11 +545,7 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme exact Nat.not_succ_le_self j.val k_ge_idx_add_one exact ih4 k k_ge_idx k_ne_j . next idx_ne_j => - apply Or.inr - apply Or.inl - apply Exists.intro j - apply Exists.intro b - apply Exists.intro i_gt_zero + 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 @@ -585,11 +572,7 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme rw [idx_eq_j1] intro j1_eq_j2 simp only [j1_eq_j2, ih2, Prod.mk.injEq, and_false] at ih1 - apply Or.inr - apply Or.inl - apply Exists.intro j2 - apply Exists.intro false - apply Exists.intro i_gt_zero + refine Or.inr <| Or.inl <| ⟨j2, false, i_gt_zero, ?_⟩ constructor . apply Nat.le_of_lt_succ rw [← Nat.succ_eq_add_one] @@ -601,7 +584,7 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme exact ih2 . constructor . simp only [clearUnit, idx_eq_j1, Array.get_eq_getElem, ih1] - have i_in_bounds : i.1 < assignments.size := by rw [hsize]; exact i.2 + have i_in_bounds : i.1 < assignments.size := hsize ▸ i.2 rw [Array.get_modify_at_idx i_in_bounds, ih3, ih4] decide . constructor @@ -617,20 +600,16 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme exact Nat.lt_irrefl idx.1 $ Nat.lt_of_succ_le k_ge_idx_add_one have h3 := units_nodup k j1 k_ne_j1 simp only [getElem_fin, ih1, ← h1, ← h2, ne_eq] at h3 - exact h3 (by rfl) + exact h3 rfl . next h2 => have h3 := units_nodup k j2 k_ne_j2 simp only [Bool.not_eq_true] at h2 simp only [getElem_fin, ih2, ← h1, ← h2, ne_eq] at h3 - exact h3 (by rfl) + exact h3 rfl . next idx_ne_j1 => by_cases idx = j2 . next idx_eq_j2 => - apply Or.inr - apply Or.inl - apply Exists.intro j1 - apply Exists.intro true - apply Exists.intro i_gt_zero + refine Or.inr <| Or.inl <| ⟨j1, true, i_gt_zero, ?_⟩ constructor . apply Nat.le_of_lt_succ rw [← Nat.succ_eq_add_one] @@ -642,7 +621,7 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme exact ih1 . constructor . simp only [clearUnit, idx_eq_j2, Array.get_eq_getElem, ih2] - have i_in_bounds : i.1 < assignments.size := by rw [hsize]; exact i.2 + have i_in_bounds : i.1 < assignments.size := hsize ▸ i.2 rw [Array.get_modify_at_idx i_in_bounds, ih3, ih4] decide . constructor @@ -654,7 +633,7 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme . next h2 => have h3 := units_nodup k j1 k_ne_j1 simp only [getElem_fin, ih1, ← h1, ← h2, ne_eq] at h3 - exact h3 (by rfl) + exact h3 rfl . next h2 => have k_ne_j2 : k ≠ j2 := by rw [← idx_eq_j2] @@ -664,10 +643,9 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme have h3 := units_nodup k j2 k_ne_j2 simp only [Bool.not_eq_true] at h2 simp only [getElem_fin, ih2, ← h1, ← h2, ne_eq] at h3 - exact h3 (by rfl) + exact h3 rfl . next idx_ne_j2 => - apply Or.inr ∘ Or.inr ∘ Exists.intro j1 ∘ Exists.intro j2 - apply Exists.intro i_gt_zero + refine Or.inr <| Or.inr <| ⟨j1, j2,i_gt_zero, ?_⟩ constructor . apply Nat.le_of_lt_succ rw [← Nat.succ_eq_add_one] @@ -694,16 +672,15 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme . next h2 => have h3 := units_nodup idx j1 idx_ne_j1 simp only [getElem_fin, ih1, ← h1, ← h2, ne_eq] at h3 - exact h3 (by rfl) + exact h3 rfl . next h2 => have h3 := units_nodup idx j2 idx_ne_j2 simp only [Bool.not_eq_true] at h2 simp only [getElem_fin, ih2, ← h1, ← h2, ne_eq] at h3 - exact h3 (by rfl) + exact h3 rfl have idx_unit_in_bounds : units[idx.1].1.1 < assignments.size := by rw [hsize]; exact units[idx.1].1.2.2 - have i_in_bounds : i.1 < assignments.size := by - rw [hsize]; exact i.2 + have i_in_bounds : i.1 < assignments.size := hsize ▸ i.2 rw [Array.get_modify_unchanged idx_unit_in_bounds i_in_bounds _ idx_res_ne_i] exact ih3 . constructor @@ -731,14 +708,9 @@ theorem clear_insertRup {n : Nat} (f : DefaultFormula n) (f_readyForRupAdd : rea . intro i hi1 hi2 have i_lt_n : i < n := by rw [← f_readyForRupAdd.2.1]; exact hi2 specialize h ⟨i, i_lt_n⟩ - rcases h with h | h | h - . exact h.1 - . exfalso - rcases h with ⟨j, b, i_gt_zero, j_size, _⟩ - exact Nat.not_lt_of_le j_size j.2 - . exfalso - rcases h with ⟨j1, j2, i_gt_zero, j1_size, _⟩ - exact Nat.not_lt_of_le j1_size j1.2 + rcases h with ⟨h,_⟩ + . exact h + . omega theorem performRupCheck_preserves_clauses {n : Nat} (f : DefaultFormula n) (rupHints : Array Nat) : (performRupCheck f rupHints).1.clauses = f.clauses := by @@ -756,24 +728,16 @@ theorem confirmRupHint_preserves_assignments_size {n : Nat} (clauses : Array (Op (assignments : Array Assignment) (derivedLits : List (Literal (PosFin n))) (b1 b2 : Bool) (id : Nat) : (confirmRupHint clauses (assignments, derivedLits, b1, b2) id).1.size = assignments.size := by simp only [confirmRupHint] - split - . rfl - . split - . split - . rfl - . rfl - . split - . rfl - . simp only [Array.modify_preserves_size] - . rfl - . rfl - . rfl + repeat first + | rfl + | simp only [Array.modify_preserves_size] + | split theorem performRupCheck_preserves_assignments_size {n : Nat} (f : DefaultFormula n) (rupHints : Array Nat) : (performRupCheck f rupHints).1.assignments.size = f.assignments.size := by simp only [performRupCheck, Prod.mk.eta] rw [Array.foldl_eq_foldl_data] - have hb : (f.assignments, ([] : List (Literal (PosFin n))), false, false).1.size = f.assignments.size := by rfl + have hb : (f.assignments, ([] : List (Literal (PosFin n))), false, false).1.size = f.assignments.size := rfl have hl (acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool) (hsize : acc.1.size = f.assignments.size) (id : Nat) (_ : id ∈ rupHints.data) : (confirmRupHint f.clauses acc id).1.size = f.assignments.size := by have h := confirmRupHint_preserves_assignments_size f.clauses acc.1 acc.2.1 acc.2.2.1 acc.2.2.2 id @@ -784,9 +748,7 @@ theorem performRupCheck_preserves_assignments_size {n : Nat} (f : DefaultFormula def derivedLits_invariant {n : Nat} (f : DefaultFormula n) (fassignments_size : f.assignments.size = n) (assignments : Array Assignment) (assignments_size : assignments.size = n) (derivedLits : List (Literal (PosFin n))) : Prop := ∀ i : Fin n, - have i_lt_assignments_size : i.1 < assignments.size := by - rw [assignments_size] - exact i.2 + have i_lt_assignments_size : i.1 < assignments.size := assignments_size ▸ i.2 have i_lt_f_assignments_size : i.1 < f.assignments.size := by rw [fassignments_size] exact i.2 @@ -921,8 +883,7 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula 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 - apply Exists.intro ⟨j.1 + 1, j_succ_in_bounds⟩ - apply Exists.intro ⟨0, zero_in_bounds⟩ + 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 @@ -1016,9 +977,8 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula have l_ne_i : l.1.1 ≠ i.1 := by intro l_eq_i simp only [hasAssignment, Bool.not_eq_true] at h - split at h - . simp (config := {decide := true}) only [getElem!, l_eq_i, i_in_bounds, h1, dite_true] at h - . simp (config := {decide := true}) only [getElem!, l_eq_i, i_in_bounds, h1, dite_true] at h + split at h <;> + simp (config := {decide := true}) only [getElem!, l_eq_i, i_in_bounds, h1, dite_true] at h constructor . rw [Array.get_modify_unchanged l_in_bounds i_in_bounds _ l_ne_i] exact h1 @@ -1075,7 +1035,7 @@ theorem confirmRupHint_preserves_invariant {n : Nat} (f : DefaultFormula n) (f_a match f.clauses[rupHints[i.val]]? with | none => exact Or.inl rfl | some none => exact Or.inr $ Or.inl rfl - | some (some c) => exact (Or.inr ∘ Or.inr ∘ Exists.intro c) (by 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 @@ -1087,7 +1047,7 @@ theorem confirmRupHint_preserves_invariant {n : Nat} (f : DefaultFormula n) (f_a match reduce c acc.fst with | ReduceResult.encounteredBoth => exact Or.inl rfl | ReduceResult.reducedToEmpty => exact (Or.inr ∘ Or.inl) rfl - | ReduceResult.reducedToUnit l => exact (Or.inr ∘ Or.inr ∘ Or.inl ∘ Exists.intro l) (by rfl) + | 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] @@ -1145,7 +1105,7 @@ theorem derivedLits_nodup {n : Nat} (f : DefaultFormula n) (f_assignments_size : exact j_property 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 (by rfl) + . exact h2 li li_in_derivedLits rfl . by_cases k.1 = i.1 . next k_eq_i => have j_ne_k : ⟨j.1, j_in_bounds⟩ ≠ k := by @@ -1236,8 +1196,7 @@ theorem restoreAssignments_performRupCheck_base_case {n : Nat} (f : DefaultFormu simp only [derivedLits_arr_def, Array.size_mk] exact j.2 have i_gt_zero : i.1 > 0 := by rw [← j_eq_i]; exact (List.get derivedLits j).1.2.1 - apply Exists.intro ⟨j.1, j_lt_derivedLits_arr_size⟩ - apply Exists.intro (List.get derivedLits j).2 ∘ Exists.intro i_gt_zero + refine ⟨⟨j.1, j_lt_derivedLits_arr_size⟩, List.get derivedLits j |>.2, i_gt_zero, ?_⟩ constructor . apply Nat.zero_le . constructor @@ -1263,9 +1222,9 @@ theorem restoreAssignments_performRupCheck_base_case {n : Nat} (f : DefaultFormu simp only [derivedLits_arr_def, Array.size_mk] exact j2.2 have i_gt_zero : i.1 > 0 := by rw [← j1_eq_i]; exact (List.get derivedLits j1).1.2.1 - apply Exists.intro ⟨j1.1, j1_lt_derivedLits_arr_size⟩ - apply Exists.intro ⟨j2.1, j2_lt_derivedLits_arr_size⟩ - apply Exists.intro i_gt_zero ∘ And.intro (Nat.zero_le j1.1) ∘ And.intro (Nat.zero_le j2.1) + refine ⟨⟨j1.1, j1_lt_derivedLits_arr_size⟩, + ⟨j2.1, j2_lt_derivedLits_arr_size⟩, + i_gt_zero, Nat.zero_le j1.1, Nat.zero_le j2.1, ?_⟩ constructor . simp only [derivedLits_arr_def, getElem_fin, Array.getElem_eq_data_get, ← j1_eq_i] rw [← j1_eq_true] @@ -1296,7 +1255,7 @@ theorem restoreAssignments_performRupCheck {n : Nat} (f : DefaultFormula n) (f_a restoreAssignments (performRupCheck f rupHints).1.assignments (performRupCheck f rupHints).2.1 = f.assignments := by rw [restoreAssignments] let f' := (performRupCheck f rupHints).1 - have f'_def : f' = (performRupCheck f rupHints).1 := by rfl + have f'_def : f' = (performRupCheck f rupHints).1 := rfl have f'_assignments_size : f'.assignments.size = n := by rw [performRupCheck_preserves_assignments_size f rupHints, f_assignments_size] have derivedLits_satisfies_invariant := derivedLits_postcondition f f_assignments_size rupHints f'_assignments_size @@ -1304,7 +1263,7 @@ theorem restoreAssignments_performRupCheck {n : Nat} (f : DefaultFormula n) (f_a generalize (performRupCheck f rupHints).2.1 = derivedLits at * rw [← f'_def, ← Array.foldl_eq_foldl_data] let derivedLits_arr : Array (Literal (PosFin n)) := {data := derivedLits} - have derivedLits_arr_def : derivedLits_arr = {data := derivedLits} := by rfl + have derivedLits_arr_def : derivedLits_arr = {data := derivedLits} := rfl have derivedLits_arr_nodup := derivedLits_nodup f f_assignments_size rupHints f'_assignments_size derivedLits derivedLits_satisfies_invariant derivedLits_arr derivedLits_arr_def let motive := clear_insert_induction_motive f f_assignments_size derivedLits_arr diff --git a/LeanSAT/LRAT/Formula/RupAddSound.lean b/LeanSAT/LRAT/Formula/RupAddSound.lean index ba18580f..fe823ff2 100644 --- a/LeanSAT/LRAT/Formula/RupAddSound.lean +++ b/LeanSAT/LRAT/Formula/RupAddSound.lean @@ -140,7 +140,7 @@ theorem insertRup_entails_hsat {n : Nat} (f : DefaultFormula n) (f_readyForRupAd . simp only [HSat.eval, List.any_eq_true, Prod.exists, Bool.exists_bool, Bool.decide_coe] apply Exists.intro i have ib_in_insertUnit_fold : (i, b) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) (negate c)).1.data := by - have i_rw : i = ⟨i.1, i.2⟩ := by rfl + have i_rw : i = ⟨i.1, i.2⟩ := rfl rw [i_rw, ← h1] apply List.get_mem have ib_in_insertUnit_fold := mem_insertUnit_fold_units f.rupUnits f.assignments false (negate c) (i, b) ib_in_insertUnit_fold @@ -187,11 +187,11 @@ theorem insertRup_entails_hsat {n : Nat} (f : DefaultFormula n) (f_readyForRupAd . simp only at h2 . exfalso have i_true_in_insertUnit_fold : (i, true) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) (negate c)).1.data := by - have i_rw : i = ⟨i.1, i.2⟩ := by rfl + have i_rw : i = ⟨i.1, i.2⟩ := rfl rw [i_rw, ← h1] apply List.get_mem have i_false_in_insertUnit_fold : (i, false) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) (negate c)).1.data := by - have i_rw : i = ⟨i.1, i.2⟩ := by rfl + have i_rw : i = ⟨i.1, i.2⟩ := rfl rw [i_rw, ← h2] apply List.get_mem simp only [f_readyForRupAdd.1, negate, negateLiteral] at i_true_in_insertUnit_fold i_false_in_insertUnit_fold @@ -249,7 +249,7 @@ theorem insertRupUnits_preserves_assignments_invariant {n : Nat} (f : DefaultFor by_cases b = b' . next b_eq_b' => let j_unit := unit (insertRupUnits f units).1.rupUnits[j] - have j_unit_def : j_unit = unit (insertRupUnits f units).1.rupUnits[j] := by rfl + have j_unit_def : j_unit = unit (insertRupUnits f units).1.rupUnits[j] := rfl have j_unit_in_insertRupUnits_res : ∃ i : PosFin n, (i, false) ∈ (insertRupUnits f units).1.rupUnits.data ∧ unit (i, false) = j_unit ∨ @@ -302,7 +302,7 @@ theorem insertRupUnits_preserves_assignments_invariant {n : Nat} (f : DefaultFor cases b <;> cases b' <;> simp at * rw [has_iff_has_of_add_complement, ← b'_def, hb] . let j1_unit := unit (insertRupUnits f units).1.rupUnits[j1] - have j1_unit_def : j1_unit = unit (insertRupUnits f units).1.rupUnits[j1] := by rfl + have j1_unit_def : j1_unit = unit (insertRupUnits f units).1.rupUnits[j1] := rfl have j1_unit_in_insertRupUnits_res : ∃ i : PosFin n, (i, false) ∈ (insertRupUnits f units).1.rupUnits.data ∧ unit (i, false) = j1_unit ∨ @@ -319,7 +319,7 @@ theorem insertRupUnits_preserves_assignments_invariant {n : Nat} (f : DefaultFor apply Array.getElem_mem_data . rfl let j2_unit := unit (insertRupUnits f units).1.rupUnits[j2] - have j2_unit_def : j2_unit = unit (insertRupUnits f units).1.rupUnits[j2] := by rfl + have j2_unit_def : j2_unit = unit (insertRupUnits f units).1.rupUnits[j2] := rfl have j2_unit_in_insertRupUnits_res : ∃ i : PosFin n, (i, false) ∈ (insertRupUnits f units).1.rupUnits.data ∧ unit (i, false) = j2_unit ∨ @@ -362,7 +362,7 @@ theorem encounteredBoth_entails_unsat {n : Nat} (c : DefaultClause n) (assignmen rw [reduce_fold_fn] at h split at h <;> [ - exact ih (by rfl); + exact ih rfl; skip; skip; simp only at h @@ -400,7 +400,7 @@ theorem reduce_fold_fn_preserves_induction_motive {c_arr : Array (Literal (PosFi . exact False.elim h . next c_arr_idx_eq_false => simp only [Bool.not_eq_true] at c_arr_idx_eq_false - rcases ih.1 (by rfl) p with ih1 | ih1 + rcases ih.1 rfl p with ih1 | ih1 . by_cases p ⊨ assignment . next p_entails_assignment => apply Or.inl @@ -419,7 +419,7 @@ theorem reduce_fold_fn_preserves_induction_motive {c_arr : Array (Literal (PosFi . exact False.elim h . next c_arr_idx_eq_false => simp only [Bool.not_eq_true', Bool.not_eq_false] at c_arr_idx_eq_false - rcases ih.1 (by rfl) p with ih1 | ih1 + rcases ih.1 rfl p with ih1 | ih1 . by_cases p ⊨ assignment . next p_entails_assignment => apply Or.inl @@ -484,7 +484,7 @@ theorem reduce_fold_fn_preserves_induction_motive {c_arr : Array (Literal (PosFi 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 . exfalso - rcases ih.1 (by rfl) p with ih1 | ih1 + 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 @@ -501,7 +501,7 @@ theorem reduce_fold_fn_preserves_induction_motive {c_arr : Array (Literal (PosFi . rw [← h] have ih2_precondition : ∃ i : Fin c_arr.size, i.val < idx.val ∧ (p ⊨ c_arr[i]) := (Exists.intro j ∘ And.intro j_lt_idx) p_entails_c_arr_j - exact ih.2 l (by rfl) p hp ih2_precondition + exact ih.2 l rfl p hp ih2_precondition . simp only [j_eq_idx, HSat.eval, Literal.instHSatLiteral, c_arr_idx_eq_false] at p_entails_c_arr_j simp only [instHSatPosFinArrayAssignment, Bool.not_eq_true] at hp specialize hp c_arr[idx.1].1 @@ -516,7 +516,7 @@ theorem reduce_fold_fn_preserves_induction_motive {c_arr : Array (Literal (PosFi . rw [← h] have ih2_precondition : ∃ i : Fin c_arr.size, i.val < idx.val ∧ (p ⊨ c_arr[i]) := (Exists.intro j ∘ And.intro j_lt_idx) p_entails_c_arr_j - exact ih.2 l (by rfl) p hp ih2_precondition + exact ih.2 l rfl p hp ih2_precondition . simp only [j_eq_idx, HSat.eval, Literal.instHSatLiteral, c_arr_idx_eq_true] at p_entails_c_arr_j simp only [instHSatPosFinArrayAssignment, Bool.not_eq_true] at hp specialize hp c_arr[idx.1].1 @@ -529,7 +529,7 @@ theorem reduce_postcondition {n : Nat} (c : DefaultClause n) (assignment : Array (reduce c assignment = reducedToEmpty → incompatible (PosFin n) c assignment) ∧ (∀ l : Literal (PosFin n), reduce c assignment = reducedToUnit l → ∀ (p : (PosFin n) → Bool), p ⊨ assignment → p ⊨ c → p ⊨ l) := by let c_arr := Array.mk c.clause - have c_clause_rw : c.clause = c_arr.data := by rfl + have c_clause_rw : c.clause = c_arr.data := rfl rw [reduce, c_clause_rw, ← Array.foldl_eq_foldl_data] let motive := reduce_postcondition_induction_motive c_arr assignment have h_base : motive 0 reducedToEmpty := by diff --git a/LeanSAT/LRAT/LRATCheckerSound.lean b/LeanSAT/LRAT/LRATCheckerSound.lean index bcafd02c..16357a78 100644 --- a/LeanSAT/LRAT/LRATCheckerSound.lean +++ b/LeanSAT/LRAT/LRATCheckerSound.lean @@ -13,17 +13,17 @@ theorem addEmptyCaseSound [DecidableEq α] [Clause α β] [Formula α β σ] (f 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 (by rfl) + 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' (by rfl) + specialize f_liff_f' rfl rw [f'_def] at f_liff_f' intro p pf 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 (by rfl) + exact Or.inl rfl specialize pf empty empty_in_f' simp only [HSat.eval, Clause.instHSat, List.any_eq_true, decide_eq_true_eq, Misc.Prod.exists, Misc.Bool.exists_bool, empty_eq, List.any_nil] at pf diff --git a/LeanSAT/Util/Misc.lean b/LeanSAT/Util/Misc.lean index a22eaf71..19097541 100644 --- a/LeanSAT/Util/Misc.lean +++ b/LeanSAT/Util/Misc.lean @@ -146,7 +146,7 @@ def List.Pairwise_iff.{u_1} {α : Type u_1} (R : α → α → Prop) (l : List . intro h apply Exists.intro hd apply Exists.intro tl - exact ⟨h.1, h.2, by rfl, by rfl⟩ + exact ⟨h.1, h.2, rfl, rfl⟩ . intro h rcases h with ⟨a, l', h1, h2, h3, h4⟩ rw [h3, h4] @@ -402,7 +402,7 @@ theorem Array.mem_filter {a : Array α} {p : α → Bool} : intro i i_in_bounds i_lt_zero exact False.elim $ Nat.not_lt_zero i i_lt_zero let f := (fun acc x => if p x = true then Array.push acc x else acc) - have f_def : f = (fun acc x => if p x = true then Array.push acc x else acc) := by rfl + have f_def : f = (fun acc x => if p x = true then Array.push acc x else acc) := rfl have h_inductive (idx : Fin a.size) (acc : Array α) (ih : motive idx.1 acc) : motive (idx.1 + 1) (f acc a[idx]) := by intro i i_in_bounds i_lt_idx_add_one rw [f_def] diff --git a/LeanSAT/Util/Nodupkeys.lean b/LeanSAT/Util/Nodupkeys.lean index af67ace3..f24e1d4d 100644 --- a/LeanSAT/Util/Nodupkeys.lean +++ b/LeanSAT/Util/Nodupkeys.lean @@ -21,8 +21,8 @@ theorem nodupkeys_eq_of_fst_eq {l : List (α × β)} (nd : l.Nodupkeys) {s s' : α × β} (h : s ∈ l) (h' : s' ∈ l) : s.1 = s'.1 → s = s' := by intro keys_eq have goal_rw : (s = s') = (s.1 = s'.1 ∧ s.2 = s'.2) := by - have s_rw : s = (s.1, s.2) := by rfl - have s'_rw : s' = (s'.1, s'.2) := by rfl + have s_rw : s = (s.1, s.2) := rfl + have s'_rw : s' = (s'.1, s'.2) := rfl rw [s_rw, s'_rw] simp only [Prod.mk.injEq] rw [goal_rw]