# `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.

source
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 : ℕ → Literal
- neg : ℕ → Literal

Instances For

source
def Sat.Literal.ofInt (i : ℤ) :
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

Instances For

source
def Sat.Literal.negate :
Literal → 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

Instances For

source
instance Sat.instToExprLiteral :
Lean.ToExpr Literal
Equations

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

source
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

Instances For

source
def Sat.Clause.nil :
Clause

The empty clause

Equations

- Sat.Clause.nil = []

Instances For

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

Append a literal to a clause.

Equations

- Sat.Clause.cons = List.cons

Instances For

source
@[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

Instances For

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

A single clause as a formula.

Equations

- Sat.Fmla.one c = [c]

Instances For

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

A conjunction of formulas.

Equations

- a.and b = a ++ b

Instances For

source
structure Sat.Fmla.subsumes (f f' : 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 : Clause) : x ∈ f' → x ∈ f

Instances For

source
theorem Sat.Fmla.subsumes_self (f : Fmla) :
f.subsumes f
source
theorem Sat.Fmla.subsumes_left (f f₁ f₂ : Fmla) (H : f.subsumes (f₁.and f₂)) :
f.subsumes f₁
source
theorem Sat.Fmla.subsumes_right (f f₁ f₂ : Fmla) (H : f.subsumes (f₁.and f₂)) :
f.subsumes f₂
source
def Sat.Valuation :
Type

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

Equations

- Sat.Valuation = (ℕ → Prop)

Instances For

source
def Sat.Valuation.neg (v : Valuation) :
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

Instances For

source
def Sat.Valuation.satisfies (v : Valuation) :
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)

Instances For

source
structure Sat.Valuation.satisfies_fmla (v : Valuation) (f : 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 : Clause) : c ∈ f → v.satisfies c

Instances For

source
def Sat.Fmla.proof (f : Fmla) (c : 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

Instances For

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

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

source
theorem Sat.Valuation.by_cases {v : Valuation} {l : 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.

source
def Sat.Valuation.implies (v : 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))

Instances For

source
def Sat.Valuation.mk :
List Prop → 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

Instances For

source
theorem Sat.Valuation.mk_implies {p : Prop} {as ps : List Prop} (as₁ : List Prop) :
as = as₁.reverseAux ps → (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`.

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

Asserts that `¬⟦f⟧_v` implies `p`.

- prop : ¬v.satisfies_fmla f → p

Instances For

source
theorem Sat.Fmla.refute {p : Prop} {ps : List Prop} (f : Fmla) (hf : f.proof []) (hv : ∀ (v : Valuation), v.implies (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.

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

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

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

Asserts that `¬⟦c⟧_v` implies `p`.

- prop : ¬v.satisfies c → p

Instances For

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

Reification of a single clause formula.

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

Asserts that `¬⟦l⟧_v` implies `p`.

- prop : v.neg l → p

Instances For

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

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

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

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

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

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

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

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

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

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

source
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.

Instances For

source
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.

Instances For

source
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.

source
partial def Mathlib.Tactic.Sat.buildClauses (arr : Array (Array ℤ)) (ctx : Lean.Expr) (start stop : ℕ) (f p : Lean.Expr) (accum : ℕ × Std.HashMap ℕ Clause) :
ℕ × Std.HashMap ℕ 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.

source
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.)

Instances For

source
def Mathlib.Tactic.Sat.buildProofStep (db : Std.HashMap ℕ 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.

Instances For

source
inductive Mathlib.Tactic.Sat.LRATStep :
Type

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

- add (id : ℕ) (lits proof : Array ℤ) : LRATStep

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

- del (ids : Array ℕ) : LRATStep

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

Instances For

source
def Mathlib.Tactic.Sat.buildProof (arr : Array (Array ℤ)) (ctx ctx' : Lean.Expr) (steps : Array 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.

Instances For

source
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.

Instances For

source
partial def Mathlib.Tactic.Sat.buildReify.mkPS (cons : Lean.Expr) (depth : ℕ) (e : Lean.Expr) :
ℕ → Lean.Expr
source
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

Instances For

source
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`

source
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.

Instances For

source
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`

source
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.

Instances For

source
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))

Instances For

source
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

Instances For

source
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.

Instances For

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

Parse a list of integers terminated by 0

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

Parse a list of natural numbers terminated by 0

source
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.

Instances For

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

Parse an LRAT file into a list of steps.

Equations

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

Instances For

source
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.

Instances For

source
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.

Instances For

source
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.

Instances For

source
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.

Instances For