HepLean Documentation

Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas

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

source
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.
Instances For
    source
    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.
    Instances For
      source
      theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.assignmentsInvariant_of_strongAssignmentsInvariant {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) :
      f.StrongAssignmentsInvariant → f.AssignmentsInvariant
      source
      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
      source
      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)
      Instances For
        source
        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)
        Instances For
          source
          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
          source
          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
          source
          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
          source
          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
          source
          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
          source
          theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insert_iff {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (c1 : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) (c2 : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) :
          c2 ∈ (f.insert c1).toList ↔ c2 = c1 ∨ c2 ∈ f.toList
          source
          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
          source
          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
          source
          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
          source
          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
          source
          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
          source
          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
          source
          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
          source
          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
          source
          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
          source
          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
          source
          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
          source
          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
          source
          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
          source
          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