inductive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult (α : Type u) : Type u

An inductive datatype used specifically for the output of the reduce function. The intended meaning of each constructor is explained in the docstring of the reduce function.

• encounteredBoth {α : Type u} : Std.Tactic.BVDecide.LRAT.Internal.ReduceResult α
• reducedToEmpty {α : Type u} : Std.Tactic.BVDecide.LRAT.Internal.ReduceResult α
• reducedToUnit {α : Type u} (l : Std.Sat.Literal α) : Std.Tactic.BVDecide.LRAT.Internal.ReduceResult α
• reducedToNonunit {α : Type u} : Std.Tactic.BVDecide.LRAT.Internal.ReduceResult α

class Std.Tactic.BVDecide.LRAT.Internal.Clause (α : outParam (Type u)) (β : Type v) : Type (max u v)

Typeclass for clauses. An instance [Clause α β] indicates that β is the type of a clause with variables of type α.

• toList : β → Std.Sat.CNF.Clause α
• not_tautology (c : β) (l : Std.Sat.Literal α) : ¬l ∈ Std.Tactic.BVDecide.LRAT.Internal.Clause.toList c ∨ ¬l.negate ∈ Std.Tactic.BVDecide.LRAT.Internal.Clause.toList c
• ofArray : Array (Std.Sat.Literal α) → Option β

  Returns none if the given array contains complementary literals

• ofArray_eq (arr : Array (Std.Sat.Literal α)) : (∀ (i j : Fin arr.size), ↑i ≠ ↑j → arr[i] ≠ arr[j]) → ∀ (c : β), Std.Tactic.BVDecide.LRAT.Internal.Clause.ofArray arr = some c → Std.Tactic.BVDecide.LRAT.Internal.Clause.toList c = arr.toList
• empty : β
• empty_eq : Std.Tactic.BVDecide.LRAT.Internal.Clause.toList Std.Tactic.BVDecide.LRAT.Internal.Clause.empty = []
• unit : Std.Sat.Literal α → β
• unit_eq (l : Std.Sat.Literal α) : Std.Tactic.BVDecide.LRAT.Internal.Clause.toList (Std.Tactic.BVDecide.LRAT.Internal.Clause.unit l) = [l]
• isUnit : β → Option (Std.Sat.Literal α)
• isUnit_iff (c : β) (l : Std.Sat.Literal α) : Std.Tactic.BVDecide.LRAT.Internal.Clause.isUnit c = some l ↔ Std.Tactic.BVDecide.LRAT.Internal.Clause.toList c = [l]
• negate : β → Std.Sat.CNF.Clause α
• negate_eq (c : β) : Std.Tactic.BVDecide.LRAT.Internal.Clause.negate c = List.map Std.Sat.Literal.negate (Std.Tactic.BVDecide.LRAT.Internal.Clause.toList c)
• insert : β → Std.Sat.Literal α → Option β

  Returns none if the result is a tautology.

• delete : β → Std.Sat.Literal α → β
• delete_iff (c : β) (l l' : Std.Sat.Literal α) : l' ∈ Std.Tactic.BVDecide.LRAT.Internal.Clause.toList (Std.Tactic.BVDecide.LRAT.Internal.Clause.delete c l) ↔ l' ≠ l ∧ l' ∈ Std.Tactic.BVDecide.LRAT.Internal.Clause.toList c
• contains : β → Std.Sat.Literal α → Bool
• contains_iff (c : β) (l : Std.Sat.Literal α) : Std.Tactic.BVDecide.LRAT.Internal.Clause.contains c l = true ↔ l ∈ Std.Tactic.BVDecide.LRAT.Internal.Clause.toList c
• reduce : β → Array Std.Tactic.BVDecide.LRAT.Internal.Assignment → Std.Tactic.BVDecide.LRAT.Internal.ReduceResult α

  Reduces the clause with respect to the given assignment

instance Std.Tactic.BVDecide.LRAT.Internal.Clause.instEntailsLiteral {α : Type u_1} : Std.Tactic.BVDecide.LRAT.Internal.Entails α (Std.Sat.Literal α)

Equations

• Std.Tactic.BVDecide.LRAT.Internal.Clause.instEntailsLiteral = { eval := fun (p : α → Bool) (l : Std.Sat.Literal α) => p l.fst = l.snd }

instance Std.Tactic.BVDecide.LRAT.Internal.Clause.instDecidableEvalLiteral {α : Type u_1} (p : α → Bool) (l : Std.Sat.Literal α) : Decidable (Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p l)

Equations

• Std.Tactic.BVDecide.LRAT.Internal.Clause.instDecidableEvalLiteral p l = inferInstanceAs (Decidable (p l.fst = l.snd))

def Std.Tactic.BVDecide.LRAT.Internal.Clause.eval {α : Type u_1} {β : Type u_2} [Std.Tactic.BVDecide.LRAT.Internal.Clause α β] (a : α → Bool) (c : β) : Bool

Equations

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

instance Std.Tactic.BVDecide.LRAT.Internal.Clause.instEntails {α : Type u_1} {β : Type u_2} [Std.Tactic.BVDecide.LRAT.Internal.Clause α β] : Std.Tactic.BVDecide.LRAT.Internal.Entails α β

Equations

• Std.Tactic.BVDecide.LRAT.Internal.Clause.instEntails = { eval := fun (a : α → Bool) (c : β) => Std.Tactic.BVDecide.LRAT.Internal.Clause.eval a c = true }

instance Std.Tactic.BVDecide.LRAT.Internal.Clause.instDecidableEval {α : Type u_1} {β : Type u_2} [Std.Tactic.BVDecide.LRAT.Internal.Clause α β] (p : α → Bool) (c : β) : Decidable (Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p c)

Equations

• Std.Tactic.BVDecide.LRAT.Internal.Clause.instDecidableEval p c = inferInstanceAs (Decidable (Std.Tactic.BVDecide.LRAT.Internal.Clause.eval p c = true))

instance Std.Tactic.BVDecide.LRAT.Internal.Clause.instInhabited {α : Type u_1} {β : Type u_2} [Std.Tactic.BVDecide.LRAT.Internal.Clause α β] : Inhabited β

Equations

• Std.Tactic.BVDecide.LRAT.Internal.Clause.instInhabited = { default := Std.Tactic.BVDecide.LRAT.Internal.Clause.empty }

structure Std.Tactic.BVDecide.LRAT.Internal.DefaultClause (numVarsSucc : Nat) : Type

The DefaultClause structure is primarily a list of literals. The additional field nodupkey is included to ensure that not_tautology is provable (which is needed to prove sat_of_insertRup and sat_of_insertRat in LRAT.Formula.Internal.RupAddSound and LRAT.Formula.Internal.RatAddSound). The additional field nodup is included to ensure that delete can be implemented by simply calling erase on the clause field. Without nodup, it would be necessary to iterate through the entire clause field and erase all instances of the literal to be deleted, since there would potentially be more than one.

In principle, one could combine nodupkey and nodup to instead have one additional field that stipulates that ∀ l1 : PosFin numVarsSucc, ∀ l2 : PosFin numVarsSucc, l1.1 ≠ l2.1. This would work just as well, and the only reason that DefaultClause is structured in this manner is that the nodup field was only included in a later stage of the verification process when it became clear that it was needed.

• clause : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin numVarsSucc)
• nodupkey (l : Std.Tactic.BVDecide.LRAT.Internal.PosFin numVarsSucc) : ¬(l, true) ∈ self.clause ∨ ¬(l, false) ∈ self.clause
• nodup : List.Nodup self.clause

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.ext {numVarsSucc : Nat} {x y : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause numVarsSucc} (clause : x.clause = y.clause) : x = y

instance Std.Tactic.BVDecide.LRAT.Internal.instBEqDefaultClause {numVarsSucc✝ : Nat} : BEq (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause numVarsSucc✝)

Equations

• Std.Tactic.BVDecide.LRAT.Internal.instBEqDefaultClause = { beq := Std.Tactic.BVDecide.LRAT.Internal.beqDefaultClause✝ }

instance Std.Tactic.BVDecide.LRAT.Internal.instToStringDefaultClause {n : Nat} : ToString (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)

Equations

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

def Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.toList {n : Nat} (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)

Equations

• c.toList = c.clause

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.not_tautology {n : Nat} (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) : ¬l ∈ c.toList ∨ ¬l.negate ∈ c.toList

def Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.empty {n : Nat} : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n

Equations

• Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.empty = { clause := [], nodupkey := ⋯, nodup := ⋯ }

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.empty_eq {n : Nat} : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.empty.toList = []

def Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.unit {n : Nat} (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n

Equations

• Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.unit l = { clause := [l], nodupkey := ⋯, nodup := ⋯ }

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.unit_eq {n : Nat} (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) : (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.unit l).toList = [l]

def Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.isUnit {n : Nat} (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) : Option (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))

Equations

• c.isUnit = match c.clause with | [l] => some l | x => none

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.isUnit_iff {n : Nat} (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) : c.isUnit = some l ↔ c.toList = [l]

def Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.negate {n : Nat} (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)

Equations

• c.negate = List.map Std.Sat.Literal.negate c.clause

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.negate_eq {n : Nat} (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) : c.negate = List.map Std.Sat.Literal.negate c.toList

def Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.insert {n : Nat} (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)

Attempts to add the literal (idx, b) to clause c. Returns none if doing so would make c a tautology.

Equations

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

def Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.ofArray {n : Nat} (ls : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))) : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)

Equations

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

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.ofArray_eq {n : Nat} (arr : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))) (arrNodup : ∀ (i j : Fin arr.size), ↑i ≠ ↑j → arr[i] ≠ arr[j]) (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.ofArray arr = some c → c.toList = arr.toList

def Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.delete {n : Nat} (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n

Equations

• c.delete l = { clause := List.erase c.clause l, nodupkey := ⋯, nodup := ⋯ }

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.delete_iff {n : Nat} (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) (l l' : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) : l' ∈ (c.delete l).toList ↔ l' ≠ l ∧ l' ∈ c.toList

def Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.contains {n : Nat} (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) : Bool

Equations

• c.contains l = List.contains c.clause l

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.contains_iff {n : Nat} (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) : c.contains l = true ↔ l ∈ c.toList

def Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.reduce_fold_fn {n : Nat} (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) (acc : Std.Tactic.BVDecide.LRAT.Internal.ReduceResult (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) : Std.Tactic.BVDecide.LRAT.Internal.ReduceResult (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)

Equations

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

def Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.reduce {n : Nat} (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) : Std.Tactic.BVDecide.LRAT.Internal.ReduceResult (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)

The reduce function takes in a clause c and takes in an array of assignments and attempts to eliminate every literal in the clause that is not compatible with the assignments argument.

• If reduce returns encounteredBoth, then this means that the assignments array has a both Assignment and is therefore fundamentally unsatisfiable.
• If reduce returns reducedToEmpty, then this means that every literal in c is incompatible with assignments. In other words, this means that the conjunction of assignments and c is unsatisfiable.
• If reduce returns reducedToUnit l, then this means that every literal in c is incompatible with assignments except for l. In other words, this means that the conjunction of assignments and c entail l.
• If reduce returns reducedToNonunit, then this means that there are multiple literals in c that are compatible with assignments. This is a failure condition for confirmRupHint (in LRAT.Formula.Implementation.lean) which calls reduce.

Equations

• c.reduce assignments = List.foldl (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.reduce_fold_fn assignments) Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToEmpty c.clause

instance Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.instClausePosFin {n : Nat} : Std.Tactic.BVDecide.LRAT.Internal.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)

Equations

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