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

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.mem_of_necessary_assignment {n : Nat} {p : Std.Tactic.BVDecide.LRAT.Internal.PosFin n → Bool} {c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n} {l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)} (p_entails_c : Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p c) (p'_not_entails_c : ¬Std.Tactic.BVDecide.LRAT.Internal.Entails.eval (fun (v : Std.Tactic.BVDecide.LRAT.Internal.PosFin n) => if v = l.fst then l.snd else p v) c) : l.negate ∈ Std.Tactic.BVDecide.LRAT.Internal.Clause.toList c

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.entails_of_irrelevant_assignment {n : Nat} {p : Std.Tactic.BVDecide.LRAT.Internal.PosFin n → Bool} {c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n} {l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)} (p_entails_cl : Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p (c.delete l.negate)) : Std.Tactic.BVDecide.LRAT.Internal.Entails.eval (fun (v : Std.Tactic.BVDecide.LRAT.Internal.PosFin n) => if v = l.fst then l.snd else p v) (c.delete l.negate)

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.assignmentsInvariant_insertRatUnits {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (hf : f.ratUnits = #[] ∧ f.AssignmentsInvariant) (units : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) : (f.insertRatUnits units).fst.AssignmentsInvariant

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.sat_of_confirmRupHint_of_insertRat_fold {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (hf : f.ratUnits = #[] ∧ f.AssignmentsInvariant) (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.insertRatUnits 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.sat_of_insertRat {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (hf : f.ratUnits = #[] ∧ f.AssignmentsInvariant) (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.insertRatUnits c.negate).snd = true → Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p c

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.safe_insert_of_performRupCheck_insertRat {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (hf : f.ratUnits = #[] ∧ f.AssignmentsInvariant) (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) (rupHints : Array Nat) : ((f.insertRatUnits 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.assignmentsInvariant_performRupCheck_of_assignmentsInvariant {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (f_AssignmentsInvariant : f.AssignmentsInvariant) (rupHints : Array Nat) : (f.performRupCheck rupHints).fst.AssignmentsInvariant

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.c_without_negPivot_of_performRatCheck_success {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (hf : f.ratUnits = #[] ∧ f.AssignmentsInvariant) (negPivot : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) (ratHint : Nat × Array Nat) (performRatCheck_success : (f.performRatCheck negPivot ratHint).snd = true) (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) : f.clauses[ratHint.fst]! = some c → Std.Tactic.BVDecide.LRAT.Internal.Limplies (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) f (c.delete negPivot)

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.existsRatHint_of_ratHintsExhaustive {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (f_readyForRatAdd : f.ReadyForRatAdd) (pivot : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) (ratHints : Array (Nat × Array Nat)) (ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true) (c' : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) (c'_in_f : c' ∈ f.toList) (negPivot_in_c' : pivot.negate ∈ Std.Tactic.BVDecide.LRAT.Internal.Clause.toList c') : ∃ (i : Fin ratHints.size), f.clauses[ratHints[i].fst]! = some c'

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.performRatCheck_success_of_performRatCheck_fold_success {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (hf : f.ratUnits = #[] ∧ f.assignments.size = n) (p : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) (ratHints : Array (Nat × Array Nat)) (i : Fin ratHints.size) (performRatCheck_fold_success : (Array.foldl (fun (acc : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n × Bool) (ratHint : Nat × Array Nat) => if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false)) (f, true) ratHints).snd = true) : (f.performRatCheck p ratHints[i]).snd = true

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.safe_insert_of_performRatCheck_fold_success {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (f_readyForRatAdd : f.ReadyForRatAdd) (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) (pivot : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) (rupHints : Array Nat) (ratHints : Array (Nat × Array Nat)) (pivot_in_c : pivot ∈ Std.Tactic.BVDecide.LRAT.Internal.Clause.toList c) (ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true) (performRatCheck_fold_success : (Array.foldl (fun (x : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n × Bool) (ratHint : Nat × Array Nat) => if x.snd = true then x.fst.performRatCheck pivot.negate ratHint else (x.fst, false)) (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints).snd = true) : Std.Tactic.BVDecide.LRAT.Internal.Equisat (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) f (f.insert c)

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ratAdd_sound {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) (pivot : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) (rupHints : Array Nat) (ratHints : Array (Nat × Array Nat)) (f' : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (f_readyForRatAdd : f.ReadyForRatAdd) (pivot_in_c : pivot ∈ Std.Tactic.BVDecide.LRAT.Internal.Clause.toList c) (ratAddSuccess : f.performRatAdd c pivot rupHints ratHints = (f', true)) : Std.Tactic.BVDecide.LRAT.Internal.Equisat (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) f f'