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 Assignment) (assignments_size : assignments.size = n) (units : Array (Sat.Literal (PosFin n))) (foundContradiction : Bool) (l : Sat.Literal (PosFin n)) : let insertUnit_res := insertUnit (units, assignments, foundContradiction) l; (foundContradiction = true → ∃ (i : PosFin n), assignments[i.val] = Assignment.both) → insertUnit_res.snd.snd = true → ∃ (j : PosFin n), insertUnit_res.snd.fst[j.val] = Assignment.both

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

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.mem_insertUnit_units {n : Nat} (units : Array (Sat.Literal (PosFin n))) (assignments : Array Assignment) (foundContradiction : Bool) (l : Sat.Literal (PosFin n)) : let insertUnit_res := insertUnit (units, assignments, foundContradiction) l; ∀ (l' : Sat.Literal (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 (Sat.Literal (PosFin n))) (assignments : Array Assignment) (foundContradiction : Bool) (l : Sat.CNF.Clause (PosFin n)) : let insertUnit_fold_res := List.foldl insertUnit (units, assignments, foundContradiction) l; ∀ (l' : Sat.Literal (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 : DefaultFormula n) (f_readyForRupAdd : f.ReadyForRupAdd) (c : DefaultClause n) (p : PosFin n → Bool) (pf : Entails.eval p f) : (f.insertRupUnits c.negate).snd = true → Entails.eval p c

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

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

def Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ConfirmRupHintFoldEntailsMotive {n : Nat} (f : DefaultFormula n) (_idx : Nat) (acc : Array Assignment × Sat.CNF.Clause (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 : DefaultClause n) (assignment : Array Assignment) : c.reduce assignment = ReduceResult.encounteredBoth → Unsatisfiable (PosFin n) assignment

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

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

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

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

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.confirmRupHint_preserves_motive {n : Nat} (f : DefaultFormula n) (rupHints : Array Nat) (idx : Fin rupHints.size) (acc : Array Assignment × Sat.CNF.Clause (PosFin n) × Bool × Bool) (ih : f.ConfirmRupHintFoldEntailsMotive (↑idx) acc) : f.ConfirmRupHintFoldEntailsMotive (↑idx + 1) (confirmRupHint f.clauses acc rupHints[idx])

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

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

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