This module contains the implementation of RUP-based clause adding for the default LRAT checker implementation.

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.size_insertUnit {n : Nat} (units : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))) (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) (b : Bool) (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) : (Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insertUnit (units, assignments, b) l).snd.fst.size = assignments.size

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.size_insertUnit_fold {n : Nat} {units : List (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))} (unitsAcc : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))) (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) (b : Bool) : (List.foldl Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insertUnit (unitsAcc, assignments, b) units).snd.fst.size = assignments.size

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.size_assignments_insertRupUnits {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (units : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) : (f.insertRupUnits units).fst.assignments.size = f.assignments.size

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.clauses_insertRupUnits {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (units : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) : (f.insertRupUnits units).fst.clauses = f.clauses

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ratUnits_insertRupUnits {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (units : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) : (f.insertRupUnits units).fst.ratUnits = f.ratUnits

def Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.InsertUnitInvariant {n : Nat} (original_assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) (original_assignments_size : original_assignments.size = n) (units : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))) (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) (assignments_size : assignments.size = n) : Prop

Equations

• One or more equations did not get rendered due to their size.

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) (assignments0_size : assignments0.size = n) (units : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))) (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) (assignments_size : assignments.size = n) (foundContradiction : Bool) (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.InsertUnitInvariant assignments0 assignments0_size units assignments assignments_size → let update_res := Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insertUnit (units, assignments, foundContradiction) l; let_fun update_res_size := ⋯; Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.InsertUnitInvariant assignments0 assignments0_size update_res.fst update_res.snd.fst update_res_size

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insertUnitInvariant_insertUnit_fold {n : Nat} (assignments0 : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) (assignments0_size : assignments0.size = n) (rupUnits : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))) (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) (assignments_size : assignments.size = n) (b : Bool) (units : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.InsertUnitInvariant assignments0 assignments0_size rupUnits assignments assignments_size → let update_res := List.foldl Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insertUnit (rupUnits, assignments, b) units; let_fun update_res_size := ⋯; Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.InsertUnitInvariant assignments0 assignments0_size update_res.fst update_res.snd.fst update_res_size

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insertUnitInvariant_insertRupUnits {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (f_readyForRupAdd : f.ReadyForRupAdd) (units : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) : let assignments := (f.insertRupUnits units).fst.assignments; let_fun hsize := ⋯; let rupUnits := (f.insertRupUnits units).fst.rupUnits; Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.InsertUnitInvariant f.assignments ⋯ rupUnits assignments hsize

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.nodup_insertRupUnits {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (f_readyForRupAdd : f.ReadyForRupAdd) (units : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) (i j : Fin (f.insertRupUnits units).fst.rupUnits.size) : i ≠ j → (f.insertRupUnits units).fst.rupUnits[i] ≠ (f.insertRupUnits units).fst.rupUnits[j]

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.size_clearUnit {n : Nat} (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) : (Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.clearUnit assignments l).size = assignments.size

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.size_clearUnit_foldl {α : Type u} (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) (f : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment → α → Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) (f_preserves_size : ∀ (arr : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) (a : α), (f arr a).size = arr.size) (l : List α) : (List.foldl f assignments l).size = assignments.size

def Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ClearInsertInductionMotive {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (assignments_size : f.assignments.size = n) (units : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))) : Nat → Array Std.Tactic.BVDecide.LRAT.Internal.Assignment → Prop

Equations

• One or more equations did not get rendered due to their size.

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.clear_insertRup_base_case {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (f_readyForRupAdd : f.ReadyForRupAdd) (units : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) : f.ClearInsertInductionMotive ⋯ (f.insertRupUnits units).fst.rupUnits 0 (f.insertRupUnits units).fst.assignments

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.clear_insert_inductive_case {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (f_assignments_size : f.assignments.size = n) (units : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))) (units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]) (idx : Fin units.size) (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) (ih : f.ClearInsertInductionMotive f_assignments_size units (↑idx) assignments) : f.ClearInsertInductionMotive f_assignments_size units (↑idx + 1) (Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.clearUnit assignments units[idx])

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.clear_insertRup {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (f_readyForRupAdd : f.ReadyForRupAdd) (units : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) : (f.insertRupUnits units).fst.clearRupUnits = f

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.clauses_performRupCheck {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (rupHints : Array Nat) : (f.performRupCheck rupHints).fst.clauses = f.clauses

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.rupUnits_performRupCheck {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (rupHints : Array Nat) : (f.performRupCheck rupHints).fst.rupUnits = f.rupUnits

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ratUnits_performRupCheck {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (rupHints : Array Nat) : (f.performRupCheck rupHints).fst.ratUnits = f.ratUnits

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.size_assignemnts_confirmRupHint {n : Nat} (clauses : Array (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n))) (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) (derivedLits : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) (b1 b2 : Bool) (id : Nat) : (Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.confirmRupHint clauses (assignments, derivedLits, b1, b2) id).fst.size = assignments.size

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.size_assignments_performRupCheck {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (rupHints : Array Nat) : (f.performRupCheck rupHints).fst.assignments.size = f.assignments.size

def Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.DerivedLitsInvariant {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (fassignments_size : f.assignments.size = n) (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) (assignments_size : assignments.size = n) (derivedLits : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) : Prop

Equations

• One or more equations did not get rendered due to their size.

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.confirmRupHint_preserves_invariant_helper {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (f_assignments_size : f.assignments.size = n) (acc : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment × Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) × Bool × Bool) (hsize : acc.fst.size = n) (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) (ih : f.DerivedLitsInvariant f_assignments_size acc.fst hsize acc.snd.fst) (h : ¬Std.Tactic.BVDecide.LRAT.Internal.Assignment.hasAssignment l.snd acc.fst[l.fst.val]! = true) : let_fun hsize' := ⋯; f.DerivedLitsInvariant f_assignments_size (acc.fst.modify l.fst.val (Std.Tactic.BVDecide.LRAT.Internal.Assignment.addAssignment l.snd)) hsize' (l :: acc.snd.fst)

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.derivedLitsInvariant_confirmRupHint {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (f_assignments_size : f.assignments.size = n) (rupHints : Array Nat) (i : Fin rupHints.size) (acc : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment × Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) × Bool × Bool) (ih : ∃ (hsize : acc.fst.size = n), f.DerivedLitsInvariant f_assignments_size acc.fst hsize acc.snd.fst) : let rupHint_res := Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.confirmRupHint f.clauses acc rupHints[i]; ∃ (hsize : rupHint_res.fst.size = n), f.DerivedLitsInvariant f_assignments_size rupHint_res.fst hsize rupHint_res.snd.fst

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.derivedLitsInvariant_performRupCheck {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (f_assignments_size : f.assignments.size = n) (rupHints : Array Nat) (f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n) : let rupCheckRes := f.performRupCheck rupHints; f.DerivedLitsInvariant f_assignments_size rupCheckRes.fst.assignments f'_assignments_size rupCheckRes.snd.fst

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.nodup_derivedLits {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (f_assignments_size : f.assignments.size = n) (rupHints : Array Nat) (f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n) (derivedLits : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) (derivedLits_satisfies_invariant : f.DerivedLitsInvariant f_assignments_size (f.performRupCheck rupHints).fst.assignments f'_assignments_size derivedLits) (derivedLits_arr : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))) (derivedLits_arr_def : derivedLits_arr = { toList := derivedLits }) (i j : Fin derivedLits_arr.size) (i_ne_j : i ≠ j) : derivedLits_arr[i] ≠ derivedLits_arr[j]

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.restoreAssignments_performRupCheck_base_case {rupHints : Array Nat} {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (f_assignments_size : f.assignments.size = n) (f' : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (_f'_def : f' = (f.performRupCheck rupHints).fst) (f'_assignments_size : f'.assignments.size = n) (derivedLits : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) (derivedLits_arr : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))) (derivedLits_arr_def : derivedLits_arr = { toList := derivedLits }) (derivedLits_satisfies_invariant : f.DerivedLitsInvariant f_assignments_size f'.assignments f'_assignments_size derivedLits) (_derivedLits_arr_nodup : ∀ (i j : Fin derivedLits_arr.size), i ≠ j → derivedLits_arr[i] ≠ derivedLits_arr[j]) : f.ClearInsertInductionMotive f_assignments_size derivedLits_arr 0 f'.assignments

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.restoreAssignments_performRupCheck {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (f_assignments_size : f.assignments.size = n) (rupHints : Array Nat) : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.restoreAssignments (f.performRupCheck rupHints).fst.assignments (f.performRupCheck rupHints).snd.fst = f.assignments

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.rupAdd_result {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) (rupHints : Array Nat) (f' : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (f_readyForRupAdd : f.ReadyForRupAdd) (rupAddSuccess : f.performRupAdd c rupHints = (f', true)) : f' = f.insert c