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

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.contradiction_of_insertUnit_success {n : Nat} (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) (assignments_size : assignments.size = n) (units : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))) (foundContradiction : Bool) (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) : let insertUnit_res := Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insertUnit (units, assignments, foundContradiction) l; (foundContradiction = true → ∃ (i : Std.Tactic.BVDecide.LRAT.Internal.PosFin n), assignments[i.val] = Std.Tactic.BVDecide.LRAT.Internal.Assignment.both) → insertUnit_res.snd.snd = true → ∃ (j : Std.Tactic.BVDecide.LRAT.Internal.PosFin n), insertUnit_res.snd.fst[j.val] = Std.Tactic.BVDecide.LRAT.Internal.Assignment.both

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.contradiction_of_insertUnit_fold_success {n : Nat} (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) (assignments_size : assignments.size = n) (units : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))) (foundContradiction : Bool) (l : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) : let insertUnit_fold_res := List.foldl Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insertUnit (units, assignments, foundContradiction) l; (foundContradiction = true → ∃ (i : Std.Tactic.BVDecide.LRAT.Internal.PosFin n), assignments[i.val] = Std.Tactic.BVDecide.LRAT.Internal.Assignment.both) → insertUnit_fold_res.snd.snd = true → ∃ (j : Std.Tactic.BVDecide.LRAT.Internal.PosFin n), insertUnit_fold_res.snd.fst[j.val] = Std.Tactic.BVDecide.LRAT.Internal.Assignment.both

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.mem_insertUnit_units {n : Nat} (units : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))) (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) (foundContradiction : Bool) (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) : let insertUnit_res := Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insertUnit (units, assignments, foundContradiction) l; ∀ (l' : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)), l' ∈ insertUnit_res.fst.toList → l' = l ∨ l' ∈ units.toList

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.mem_insertUnit_fold_units {n : Nat} (units : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))) (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) (foundContradiction : Bool) (l : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) : let insertUnit_fold_res := List.foldl Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insertUnit (units, assignments, foundContradiction) l; ∀ (l' : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)), l' ∈ insertUnit_fold_res.fst.toList → l' ∈ l ∨ l' ∈ units.toList

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.sat_of_insertRup {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (f_readyForRupAdd : f.ReadyForRupAdd) (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) (p : Std.Tactic.BVDecide.LRAT.Internal.PosFin n → Bool) (pf : Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p f) : (f.insertRupUnits c.negate).snd = true → Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p c

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.safe_insert_of_insertRup {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (f_readyForRupAdd : f.ReadyForRupAdd) (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) : (f.insertRupUnits c.negate).snd = true → Std.Tactic.BVDecide.LRAT.Internal.Limplies (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) f (f.insert c)

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.assignmentsInvariant_insertRupUnits_of_assignmentsInvariant {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.AssignmentsInvariant

def Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ConfirmRupHintFoldEntailsMotive {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (_idx : Nat) (acc : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment × Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) × Bool × Bool) : Prop

Equations

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

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.unsat_of_encounteredBoth {n : Nat} (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) (assignment : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) : c.reduce assignment = Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.encounteredBoth → Std.Tactic.BVDecide.LRAT.Internal.Unsatisfiable (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) assignment

def Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ReducePostconditionInductionMotive {n : Nat} (c_arr : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))) (assignment : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) (idx : Nat) (res : Std.Tactic.BVDecide.LRAT.Internal.ReduceResult (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.reduce_fold_fn_preserves_induction_motive {n : Nat} {c_arr : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))} {assignment : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment} (idx : Fin c_arr.size) (res : Std.Tactic.BVDecide.LRAT.Internal.ReduceResult (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) (ih : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ReducePostconditionInductionMotive c_arr assignment (↑idx) res) : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ReducePostconditionInductionMotive c_arr assignment (↑idx + 1) (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.reduce_fold_fn assignment res c_arr[idx])

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.reduce_postcondition {n : Nat} (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) (assignment : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) : (c.reduce assignment = Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToEmpty → Std.Tactic.BVDecide.LRAT.Internal.Incompatible (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) c assignment) ∧ ∀ (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)), c.reduce assignment = Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit l → ∀ (p : Std.Tactic.BVDecide.LRAT.Internal.PosFin n → Bool), Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p assignment → Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p c → Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p l

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.incompatible_of_reducedToEmpty {n : Nat} (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) (assignment : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) : c.reduce assignment = Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToEmpty → Std.Tactic.BVDecide.LRAT.Internal.Incompatible (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) c assignment

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.limplies_of_reducedToUnit {n : Nat} (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) (assignment : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) : c.reduce assignment = Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit l → ∀ (p : Std.Tactic.BVDecide.LRAT.Internal.PosFin n → Bool), Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p assignment → Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p c → Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p l

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.confirmRupHint_preserves_motive {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (rupHints : Array Nat) (idx : 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 : f.ConfirmRupHintFoldEntailsMotive (↑idx) acc) : f.ConfirmRupHintFoldEntailsMotive (↑idx + 1) (Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.confirmRupHint f.clauses acc rupHints[idx])

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.sat_of_confirmRupHint_insertRup_fold {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (f_readyForRupAdd : f.ReadyForRupAdd) (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) (rupHints : Array Nat) (p : Std.Tactic.BVDecide.LRAT.Internal.PosFin n → Bool) (pf : Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p f) : let fc := f.insertRupUnits c.negate; let confirmRupHint_fold_res := Array.foldl (Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.confirmRupHint fc.fst.clauses) (fc.fst.assignments, [], false, false) rupHints; confirmRupHint_fold_res.snd.snd.fst = true → Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p c

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.safe_insert_of_performRupCheck_insertRup {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (f_readyForRupAdd : f.ReadyForRupAdd) (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) (rupHints : Array Nat) : ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).snd.snd.fst = true → Std.Tactic.BVDecide.LRAT.Internal.Limplies (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) f (f.insert c)

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.rupAdd_sound {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)) : Std.Tactic.BVDecide.LRAT.Internal.Liff (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) f f'