lrat_proof command

Defines a macro for producing SAT proofs from CNF / LRAT files. These files are commonly used in the SAT community for writing proofs.

Most SAT solvers support export to DRAT format, but this format can be expensive to reconstruct because it requires recomputing all unit propagation steps. The LRAT format solves this issue by attaching a proof to the deduction of each new clause. (The L in LRAT stands for Linear time verification.) There are several verified checkers for the LRAT format, and the program implemented here makes it possible to use the lean kernel as an LRAT checker as well and expose the results as a standard propositional theorem.

The input to the lrat_proof command is the name of the theorem to define, and the statement (written in CNF format) and the proof (in LRAT format). For example:

lrat_proof foo
  "p cnf 2 4  1 2 0  -1 2 0  1 -2 0  -1 -2 0"
  "5 -2 0 4 3 0  5 d 3 4 0  6 1 0 5 1 0  6 d 1 0  7 0 5 2 6 0"

produces a theorem:

foo : ∀ (a a_1 : Prop), (¬a ∧ ¬a_1 ∨ a ∧ ¬a_1) ∨ ¬a ∧ a_1 ∨ a ∧ a_1

• You can see the theorem statement by hovering over the word foo.
• You can use the example keyword in place of foo to avoid generating a theorem.
• You can use the include_str macro in place of the two strings to load CNF / LRAT files from disk.

inductive Sat.Literal : Type

A literal is a positive or negative occurrence of an atomic propositional variable. Note that unlike DIMACS, 0 is a valid variable index.

• pos : ℕ → Sat.Literal
• neg : ℕ → Sat.Literal

def Sat.Literal.ofInt (i : ℤ) : Sat.Literal

Construct a literal. Positive numbers are translated to positive literals, and negative numbers become negative literals. The input is assumed to be nonzero.

Equations

• Sat.Literal.ofInt i = if i < 0 then Sat.Literal.neg (-i - 1).toNat else Sat.Literal.pos (i - 1).toNat

def Sat.Literal.negate : Sat.Literal → Sat.Literal

Swap the polarity of a literal.

Equations

• (Sat.Literal.pos i).negate = Sat.Literal.neg i
• (Sat.Literal.neg i).negate = Sat.Literal.pos i

instance Sat.instToExprLiteral : Lean.ToExpr Sat.Literal

Equations

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

def Sat.Clause : Type

A clause is a list of literals, thought of as a disjunction like a ∨ b ∨ ¬c.

Equations

• Sat.Clause = List Sat.Literal

def Sat.Clause.nil : Sat.Clause

Equations

• Sat.Clause.nil = []

def Sat.Clause.cons : Sat.Literal → Sat.Clause → Sat.Clause

Equations

• Sat.Clause.cons = List.cons

@[reducible, inline]

abbrev Sat.Fmla : Type

A formula is a list of clauses, thought of as a conjunction like (a ∨ b) ∧ c ∧ (¬c ∨ ¬d).

Equations

• Sat.Fmla = List Sat.Clause

def Sat.Fmla.one (c : Sat.Clause) : Sat.Fmla

A single clause as a formula.

Equations

• Sat.Fmla.one c = [c]

def Sat.Fmla.and (a b : Sat.Fmla) : Sat.Fmla

A conjunction of formulas.

Equations

• a.and b = a ++ b

structure Sat.Fmla.subsumes (f f' : Sat.Fmla) : Prop

Formula f subsumes f' if all the clauses in f' are in f. We use this to prove that all clauses in the formula are subsumed by it.

• prop (x : Sat.Clause) : x ∈ f' → x ∈ f

theorem Sat.Fmla.subsumes_self (f : Sat.Fmla) : f.subsumes f

theorem Sat.Fmla.subsumes_left (f f₁ f₂ : Sat.Fmla) (H : f.subsumes (f₁.and f₂)) : f.subsumes f₁

theorem Sat.Fmla.subsumes_right (f f₁ f₂ : Sat.Fmla) (H : f.subsumes (f₁.and f₂)) : f.subsumes f₂

def Sat.Valuation : Type

A valuation is an assignment of values to all the propositional variables.

Equations

• Sat.Valuation = (ℕ → Prop)

def Sat.Valuation.neg (v : Sat.Valuation) : Sat.Literal → Prop

v.neg lit asserts that literal lit is falsified in the valuation.

Equations

• v.neg (Sat.Literal.pos i) = ¬v i
• v.neg (Sat.Literal.neg i) = v i

def Sat.Valuation.satisfies (v : Sat.Valuation) : Sat.Clause → Prop

v.satisfies c asserts that clause c satisfied by the valuation. It is written in a negative way: A clause like a ∨ ¬b ∨ c is rewritten as ¬a → b → ¬c → False, so we are asserting that it is not the case that all literals in the clause are falsified.

Equations

• v.satisfies [] = False
• v.satisfies (l :: c) = (v.neg l → v.satisfies c)

structure Sat.Valuation.satisfies_fmla (v : Sat.Valuation) (f : Sat.Fmla) : Prop

v.satisfies_fmla f asserts that formula f is satisfied by the valuation. A formula is satisfied if all clauses in it are satisfied.

• prop (c : Sat.Clause) : c ∈ f → v.satisfies c

def Sat.Fmla.proof (f : Sat.Fmla) (c : Sat.Clause) : Prop

f.proof c asserts that c is derivable from f.

Equations

• f.proof c = ∀ (v : Sat.Valuation), v.satisfies_fmla f → v.satisfies c

theorem Sat.Fmla.proof_of_subsumes {f : Sat.Fmla} {c : Sat.Clause} (H : f.subsumes (Sat.Fmla.one c)) : f.proof c

If f subsumes c (i.e. c ∈ f), then f.proof c.

theorem Sat.Valuation.by_cases {v : Sat.Valuation} {l : Sat.Literal} (h₁ : v.neg l.negate → False) (h₂ : v.neg l → False) : False

The core unit-propagation step.

We have a local context of assumptions ¬l' (sometimes called an assignment) and we wish to add ¬l to the context, that is, we want to prove l is also falsified. This is because there is a clause a ∨ b ∨ ¬l in the global context such that all literals in the clause are falsified except for ¬l; so in the context h₁ where we suppose that ¬l is falsified, the clause itself is falsified so we can prove False. We continue the proof in h₂, with the assumption that l is falsified.

def Sat.Valuation.implies (v : Sat.Valuation) (p : Prop) : List Prop → ℕ → Prop

v.implies p [a, b, c] 0 definitionally unfolds to (v 0 ↔ a) → (v 1 ↔ b) → (v 2 ↔ c) → p. This is used to introduce assumptions about the first n values of v during reification.

Equations

• v.implies p [] x✝ = p
• v.implies p (a :: as) x✝ = ((v x✝ ↔ a) → v.implies p as (x✝ + 1))

def Sat.Valuation.mk : List Prop → Sat.Valuation

Valuation.mk [a, b, c] is a valuation which is a at 0, b at 1 and c at 2, and false everywhere else.

Equations

• Sat.Valuation.mk [] x✝ = False
• Sat.Valuation.mk (a :: tail) 0 = a
• Sat.Valuation.mk (head :: as) n.succ = Sat.Valuation.mk as n

theorem Sat.Valuation.mk_implies {p : Prop} {as ps : List Prop} (as₁ : List Prop) : as = as₁.reverseAux ps → (Sat.Valuation.mk as).implies p ps as₁.length → p

The fundamental relationship between mk and implies: (mk ps).implies p ps 0 is equivalent to p.

structure Sat.Fmla.reify (v : Sat.Valuation) (f : Sat.Fmla) (p : Prop) : Prop

Asserts that ¬⟦f⟧_v implies p.

• prop : ¬v.satisfies_fmla f → p

theorem Sat.Fmla.refute {p : Prop} {ps : List Prop} (f : Sat.Fmla) (hf : f.proof []) (hv : ∀ (v : Sat.Valuation), v.implies (Sat.Fmla.reify v f p) ps 0) : p

If f is unsatisfiable, and every v which agrees with ps implies ¬⟦f⟧_v → p, then p. Equivalently, there exists a valuation v which agrees with ps, and every such valuation yields ¬⟦f⟧_v because f is unsatisfiable.

theorem Sat.Fmla.reify_or {v : Sat.Valuation} {f₁ : Sat.Fmla} {a : Prop} {f₂ : Sat.Fmla} {b : Prop} (h₁ : Sat.Fmla.reify v f₁ a) (h₂ : Sat.Fmla.reify v f₂ b) : Sat.Fmla.reify v (f₁.and f₂) (a ∨ b)

Negation turns AND into OR, so ¬⟦f₁ ∧ f₂⟧_v ≡ ¬⟦f₁⟧_v ∨ ¬⟦f₂⟧_v.

structure Sat.Clause.reify (v : Sat.Valuation) (c : Sat.Clause) (p : Prop) : Prop

Asserts that ¬⟦c⟧_v implies p.

• prop : ¬v.satisfies c → p

theorem Sat.Fmla.reify_one {v : Sat.Valuation} {c : Sat.Clause} {a : Prop} (h : Sat.Clause.reify v c a) : Sat.Fmla.reify v (Sat.Fmla.one c) a

Reification of a single clause formula.

structure Sat.Literal.reify (v : Sat.Valuation) (l : Sat.Literal) (p : Prop) : Prop

Asserts that ¬⟦l⟧_v implies p.

• prop : v.neg l → p

theorem Sat.Clause.reify_and {v : Sat.Valuation} {l : Sat.Literal} {a : Prop} {c : Sat.Clause} {b : Prop} (h₁ : Sat.Literal.reify v l a) (h₂ : Sat.Clause.reify v c b) : Sat.Clause.reify v (Sat.Clause.cons l c) (a ∧ b)

Negation turns OR into AND, so ¬⟦l ∨ c⟧_v ≡ ¬⟦l⟧_v ∧ ¬⟦c⟧_v.

theorem Sat.Clause.reify_zero {v : Sat.Valuation} : Sat.Clause.reify v Sat.Clause.nil True

The reification of the empty clause is True: ¬⟦⊥⟧_v ≡ True.

theorem Sat.Clause.reify_one {v : Sat.Valuation} {l : Sat.Literal} {a : Prop} (h₁ : Sat.Literal.reify v l a) : Sat.Clause.reify v (Sat.Clause.cons l Sat.Clause.nil) a

The reification of a singleton clause ¬⟦l⟧_v ≡ ¬⟦l⟧_v.

theorem Sat.Literal.reify_pos {v : Sat.Valuation} {a : Prop} {n : ℕ} (h : v n ↔ a) : Sat.Literal.reify v (Sat.Literal.pos n) ¬a

The reification of a positive literal ¬⟦a⟧_v ≡ ¬a.

theorem Sat.Literal.reify_neg {v : Sat.Valuation} {a : Prop} {n : ℕ} (h : v n ↔ a) : Sat.Literal.reify v (Sat.Literal.neg n) a

The reification of a negative literal ¬⟦¬a⟧_v ≡ a.

structure Mathlib.Tactic.Sat.Clause : Type

The representation of a global clause.

• lits : Array ℤ

  The list of literals as read from the input file

• expr : Lean.Expr

  The clause expression of type Clause

• proof : Lean.Expr

  A proof of ⊢ ctx.proof c. Note that we do not use have statements to cache these proofs: this is literally the proof expression itself. As a result, the proof terms rely heavily on dag-like sharing of the expression, and printing these proof terms directly is likely to crash lean for larger examples.

def Mathlib.Tactic.Sat.buildClause (arr : Array ℤ) : Lean.Expr

Construct the clause expression from the input list. For example [1, -2] is translated to Clause.cons (Literal.pos 1) (Clause.cons (Literal.neg 2) Clause.nil).

Equations

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

partial def Mathlib.Tactic.Sat.buildConj (arr : Array (Array ℤ)) (start stop : ℕ) : Lean.Expr

Constructs the formula expression from the input CNF, as a balanced tree of Fmla.and nodes.

partial def Mathlib.Tactic.Sat.buildClauses (arr : Array (Array ℤ)) (ctx : Lean.Expr) (start stop : ℕ) (f p : Lean.Expr) (accum : ℕ × Std.HashMap ℕ Mathlib.Tactic.Sat.Clause) : ℕ × Std.HashMap ℕ Mathlib.Tactic.Sat.Clause

Constructs the proofs of ⊢ ctx.proof c for each clause c in ctx. The proofs are stashed in a HashMap keyed on the clause ID.

structure Mathlib.Tactic.Sat.LClause : Type

A localized clause reference. It is the same as Clause except that the proof is now a local variable.

• lits : Array ℤ

  The list of literals as read from the input file

• expr : Lean.Expr

  The clause expression of type Clause

• depth : ℕ

  The bound variable index of the hypothesis asserting ⊢ ctx.proof c, counting from the outside and 1-based. (We use this numbering because we will need to reference the variable from multiple binder depths.)

def Mathlib.Tactic.Sat.buildProofStep (db : Std.HashMap ℕ Mathlib.Tactic.Sat.Clause) (ns pf : Array ℤ) (ctx clause : Lean.Expr) : Except String Lean.Expr

Construct an individual proof step ⊢ ctx.proof c.

• db: the current global context
• ns, clause: the new clause
• pf: the LRAT proof trace
• ctx: the main formula

The proof has three steps:

1. Introduce local assumptions have h1 : ctx.proof c1 := p1 for each clause c1 referenced in the proof. We actually do all the introductions at once, as in (fun h1 h2 h3 ↦ ...) p1 p2 p3, because we want p_i to not be under any binders to avoid the cost of instantiate during typechecking and get the benefits of dag-like sharing in the pi (which are themselves previous proof steps which may be large terms). The hypotheses are in gctx, keyed on the clause ID.

2. Unfold ⊢ ctx.proof [a, b, c] to ∀ v, v.satisfies_fmla ctx → v.neg a → v.neg b → v.neg c → False and intro v hv ha hb hc, storing each ha : v.neg a in lctx, keyed on the literal a.

3. For each LRAT step hc : ctx.proof [x, y], hc v hv : v.neg x → v.neg y → False. We look for a literal that is not falsified in the clause. Since it is a unit propagation step, there can be at most one such literal.

   • If x is the non-falsified clause, let x' denote the negated literal of x. Then x'.negate reduces to x, so hnx : v.neg x'.negate |- hc v hv hnx hy : False, so we construct the term by_cases (fun hnx : v.neg x'.negate ↦ hc v hv hnx hy) (fun hx : v.neg x ↦ ...) and hx is added to the local context.
   • If all clauses are falsified, then we are done: hc v hv hx hy : False.

Equations

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

inductive Mathlib.Tactic.Sat.LRATStep : Type

An LRAT step is either an addition or a deletion step.

• add (id : ℕ) (lits proof : Array ℤ) : Mathlib.Tactic.Sat.LRATStep

  An addition step, with the clause ID, the clause literal list, and the proof trace

• del (ids : Array ℕ) : Mathlib.Tactic.Sat.LRATStep

  A (multiple) deletion step, which deletes all the listed clause IDs from the context

def Mathlib.Tactic.Sat.buildProof (arr : Array (Array ℤ)) (ctx ctx' : Lean.Expr) (steps : Array Mathlib.Tactic.Sat.LRATStep) : Lean.MetaM Lean.Expr

Build the main proof of ⊢ ctx.proof [] using the LRAT proof trace.

• arr: The input CNF
• ctx: The abbreviated formula, a constant like foo.ctx_1
• ctx': The definitional expansion of the formula, a tree of Fmla.and nodes
• steps: The input LRAT proof trace

Equations

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

def Mathlib.Tactic.Sat.buildReify (ctx ctx' proof : Lean.Expr) (nvars : ℕ) : Lean.Expr × Lean.Expr

Build the type and value of the reified theorem. This rewrites all the SAT definitions into standard operators on Prop, for example if the formula is [[1, 2], [-1, 2], [-2]] then this produces a proof of ⊢ ∀ a b : Prop, (a ∧ b) ∨ (¬a ∧ b) ∨ ¬b. We use the input nvars to decide how many quantifiers to use.

Most of the proof is under 2 * nvars + 1 quantifiers a1 .. an : Prop, v : Valuation, h1 : v 0 ↔ a1, ... hn : v (n-1) ↔ an ⊢ ..., and we do the index arithmetic by hand.

1. First, we call reifyFormula ctx' which returns a and pr : reify v ctx' a
2. Then we build fun (v : Valuation) (h1 : v 0 ↔ a1) ... (hn : v (n-1) ↔ an) ↦ pr
3. We have to lower expression a from step 1 out of the quantifiers by lowering all variable indices by nvars+1. This is okay because v and h1..hn do not appear in a.
4. We construct the expression ps, which is a1 .. an : Prop ⊢ [a1, ..., an] : List Prop
5. refute ctx (hf : ctx.proof []) (fun v h1 .. hn ↦ pr) : a forces some definitional unfolding since fun h1 .. hn ↦ pr should have type implies v (reify v ctx a) [a1, ..., an] a, which involves unfolding implies n times as well as ctx ↦ ctx'.
6. Finally, we intro a1 ... an so that we have a proof of ∀ a1 ... an, a.

Equations

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

partial def Mathlib.Tactic.Sat.buildReify.mkPS (cons : Lean.Expr) (depth : ℕ) (e : Lean.Expr) : ℕ → Lean.Expr

def Mathlib.Tactic.Sat.buildReify.v (nvars : ℕ) : Lean.Expr

The v variable under the a1 ... an, v, h1 ... hn context

Equations

• Mathlib.Tactic.Sat.buildReify.v nvars = Lean.mkBVar nvars

partial def Mathlib.Tactic.Sat.buildReify.reifyFmla (nvars : ℕ) (f : Lean.Expr) : Lean.Expr × Lean.Expr

Returns a and pr : reify v f a given a formula f

def Mathlib.Tactic.Sat.buildReify.reifyClause (nvars : ℕ) (c : Lean.Expr) : Lean.Expr × Lean.Expr

Returns a and pr : reify v c a given a clause c

Equations

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

partial def Mathlib.Tactic.Sat.buildReify.reifyClause1 (nvars : ℕ) (c : Lean.Expr) : Lean.Expr × Lean.Expr

Returns a and pr : reify v c a given a nonempty clause c

def Mathlib.Tactic.Sat.buildReify.reifyLiteral (nvars : ℕ) (l : Lean.Expr) : Lean.Expr × Lean.Expr

Returns a and pr : reify v l a given a literal c

Equations

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

def Mathlib.Tactic.Sat.buildReify.reifyVar (nvars : ℕ) (v : Lean.Expr) : Lean.Expr × Lean.Expr

Returns a and pr : v n ↔ a given a variable index n. These are both lookups into the context (a0 .. a(n-1) : Prop) (v) (h1 : v 0 ↔ a0) ... (hn : v (n-1) ↔ a(n-1)).

Equations

• Mathlib.Tactic.Sat.buildReify.reifyVar nvars v = (Lean.mkBVar (2 * nvars - v.rawNatLit?.get!), Lean.mkBVar (nvars - v.rawNatLit?.get! - 1))

def Mathlib.Tactic.Sat.Parser.parseNat : Std.Internal.Parsec.String.Parser ℕ

Parse a natural number

Equations

• Mathlib.Tactic.Sat.Parser.parseNat = Lean.Json.Parser.natMaybeZero

def Mathlib.Tactic.Sat.Parser.parseInt : Std.Internal.Parsec.String.Parser ℤ

Parse an integer

Equations

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

partial def Mathlib.Tactic.Sat.Parser.parseInts (arr : Array ℤ := #[]) : Std.Internal.Parsec.String.Parser (Array ℤ)

Parse a list of integers terminated by 0

partial def Mathlib.Tactic.Sat.Parser.parseNats (arr : Array ℕ := #[]) : Std.Internal.Parsec.String.Parser (Array ℕ)

Parse a list of natural numbers terminated by 0

def Mathlib.Tactic.Sat.Parser.parseDimacs : Std.Internal.Parsec.String.Parser (ℕ × Array (Array ℤ))

Parse a DIMACS format .cnf file. This is not very robust; we assume the file has had comments stripped.

Equations

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

def Mathlib.Tactic.Sat.Parser.parseLRAT : Std.Internal.Parsec.String.Parser (Array Mathlib.Tactic.Sat.LRATStep)

Parse an LRAT file into a list of steps.

Equations

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

def Mathlib.Tactic.Sat.fromLRATAux (cnf lrat : String) (name : Lean.Name) : Lean.MetaM (ℕ × Lean.Expr × Lean.Expr × Lean.Expr)

Core of fromLRAT. Constructs the context and main proof definitions, but not the reification theorem. Returns:

• nvars: the number of variables specified in the CNF file
• ctx: The abbreviated formula, a constant like foo.ctx_1
• ctx': The definitional expansion of the formula, a tree of Fmla.and nodes
• proof: A proof of ctx.proof []

Equations

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

def Mathlib.Tactic.Sat.fromLRAT (cnf lrat : String) (name : Lean.Name) : Lean.MetaM Unit

Main entry point. Given strings cnf and lrat with unparsed file data, and a name name, adds theorem name : type := proof where type is a propositional theorem like ∀ (a a_1 : Prop), (¬a ∧ ¬a_1 ∨ a ∧ ¬a_1) ∨ ¬a ∧ a_1 ∨ a ∧ a_1.

Also creates auxiliaries named name.ctx_1 (for the CNF formula) and name.proof_1 (for the LRAT proof), with name itself containing the reification proof.

Equations

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

def Mathlib.Tactic.Sat.commandLrat_proof_Example____ : Lean.ParserDescr

A macro for producing SAT proofs from CNF / LRAT files. These files are commonly used in the SAT community for writing proofs.

The input to the lrat_proof command is the name of the theorem to define, and the statement (written in CNF format) and the proof (in LRAT format). For example:

lrat_proof foo
  "p cnf 2 4  1 2 0  -1 2 0  1 -2 0  -1 -2 0"
  "5 -2 0 4 3 0  5 d 3 4 0  6 1 0 5 1 0  6 d 1 0  7 0 5 2 6 0"

produces a theorem:

foo : ∀ (a a_1 : Prop), (¬a ∧ ¬a_1 ∨ a ∧ ¬a_1) ∨ ¬a ∧ a_1 ∨ a ∧ a_1

• You can see the theorem statement by hovering over the word foo.
• You can use the example keyword in place of foo to avoid generating a theorem.
• You can use the include_str macro in place of the two strings to load CNF / LRAT files from disk.

Equations

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

def Mathlib.Tactic.Sat.termFrom_lrat___ : Lean.ParserDescr

A macro for producing SAT proofs from CNF / LRAT files. These files are commonly used in the SAT community for writing proofs.

The input to the from_lrat term syntax is two string expressions with the statement (written in CNF format) and the proof (in LRAT format). For example:

def foo := from_lrat
  "p cnf 2 4  1 2 0  -1 2 0  1 -2 0  -1 -2 0"
  "5 -2 0 4 3 0  5 d 3 4 0  6 1 0 5 1 0  6 d 1 0  7 0 5 2 6 0"

produces a theorem:

foo : ∀ (a a_1 : Prop), (¬a ∧ ¬a_1 ∨ a ∧ ¬a_1) ∨ ¬a ∧ a_1 ∨ a ∧ a_1

• You can use this term after have := or in def foo := to produce the term without constraining the type.
• You can use it when a specific type is expected, but it currently does not pay any attention to the shape of the goal and always produces the same theorem, so you can only use this to do alpha renaming.
• You can use the include_str macro in place of the two strings to load CNF / LRAT files from disk.

Equations

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