This module contains basic statements about the invariants that are satisfied by the LRAT checker implementation in Implementation.

def Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.StrongAssignmentsInvariant {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) : Prop

This invariant states that if the assignments field of a default formula f indicates that f contains an assignment b at index i, then the unit literal (i, b) must be included in f. Default formulas are expected to satisfy this invariant at all times except during intermediate stages of unit propagation (during which, default formulas are only expected to satisfy the more lenient AssignmentsInvariant defined below).

Equations

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

def Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.AssignmentsInvariant {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) : Prop

This invariant states that if the assignments field of a default formula f indicates that f contains an assignment b at index i, then the unit literal (i, b) is entailed by f. This is distinct from the StrongAssignmentsInvariant defined above in that the entailment described here does not require explicitly containing the literal (i, b). For example, if f contains (i, b) ∨ (j, b') as well as (i, b) ∨ (j, ¬b'), then the AssignmentsInvariant would permit the assignments field of f to contain assignment b at index i, but the StrongAssignmentsInvariant would not.

Equations

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

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.assignmentsInvariant_of_strongAssignmentsInvariant {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) : f.StrongAssignmentsInvariant → f.AssignmentsInvariant

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.limplies_of_assignmentsInvariant {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (f_AssignmentsInvariant : f.AssignmentsInvariant) : Std.Tactic.BVDecide.LRAT.Internal.Limplies (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) f f.assignments

def Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ReadyForRupAdd {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) : Prop

performRupAdd adds to f.rupUnits and then clears f.rupUnits. If f begins with some units in f.rupUnits, then performRupAdd will clear more than it intended to which will break the correctness of rupAdd_result.

Equations

• f.ReadyForRupAdd = (f.rupUnits = #[] ∧ f.StrongAssignmentsInvariant)

def Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ReadyForRatAdd {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) : Prop

performRatAdd adds to f.rupUnits and f.ratUnits and then clears both. If f begins with some units in either, then performRatAdd will clear more than it intended to which will break the correctness of ratAdd_result

Equations

• f.ReadyForRatAdd = (f.ratUnits = #[] ∧ f.ReadyForRupAdd)

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.rupUnits_insert {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) : (f.insert c).rupUnits = f.rupUnits

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ratUnits_insert {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) : (f.insert c).ratUnits = f.ratUnits

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.size_ofArray_fold_fn {n : Nat} (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) (cOpt : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)) : (Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ofArray_fold_fn assignments cOpt).size = assignments.size

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n))) : (Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ofArray arr).ReadyForRupAdd

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.readyForRatAdd_ofArray {n : Nat} (arr : Array (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n))) : (Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ofArray arr).ReadyForRatAdd

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insert_iff {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (c1 c2 : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) : c2 ∈ (f.insert c1).toList ↔ c2 = c1 ∨ c2 ∈ f.toList

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.limplies_insert {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) : Std.Tactic.BVDecide.LRAT.Internal.Limplies (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) (f.insert c) f

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.size_assignments_insert {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) : (f.insert c).assignments.size = f.assignments.size

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.readyForRupAdd_insert {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) : f.ReadyForRupAdd → (f.insert c).ReadyForRupAdd

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.readyForRatAdd_insert {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) : f.ReadyForRatAdd → (f.insert c).ReadyForRatAdd

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.mem_of_insertRupUnits {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (units : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) : c ∈ (f.insertRupUnits units).fst.toList → c ∈ List.map Std.Tactic.BVDecide.LRAT.Internal.Clause.unit units ∨ c ∈ f.toList

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.mem_of_insertRatUnits {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (units : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) : c ∈ (f.insertRatUnits units).fst.toList → c ∈ List.map Std.Tactic.BVDecide.LRAT.Internal.Clause.unit units ∨ c ∈ f.toList

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.deleteOne_preserves_rupUnits {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (id : Nat) : (f.deleteOne id).rupUnits = f.rupUnits

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.deleteOne_preserves_assignments_size {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (id : Nat) : (f.deleteOne id).assignments.size = f.assignments.size

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (id : Nat) : f.StrongAssignmentsInvariant → (f.deleteOne id).StrongAssignmentsInvariant

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.readyForRupAdd_delete {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (arr : Array Nat) : f.ReadyForRupAdd → (f.delete arr).ReadyForRupAdd

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.deleteOne_preserves_ratUnits {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (id : Nat) : (f.deleteOne id).ratUnits = f.ratUnits

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.readyForRatAdd_delete {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (arr : Array Nat) : f.ReadyForRatAdd → (f.delete arr).ReadyForRatAdd

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.deleteOne_subset {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (id : Nat) (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) : c ∈ (f.deleteOne id).toList → c ∈ f.toList

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.delete_subset {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (arr : Array Nat) (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) : c ∈ (f.delete arr).toList → c ∈ f.toList