tactic.omega.nat.dnf - mathlib docs

@[simp]

Equations

omega.nat.dnf_core (p ∧* q) = list.map (λ (pq : omega.clause × omega.clause), pq.fst.append pq.snd) ((omega.nat.dnf_core p).product (omega.nat.dnf_core q))
omega.nat.dnf_core (p ∨* q) = omega.nat.dnf_core p ++ omega.nat.dnf_core q
omega.nat.dnf_core (¬* _x) = list.nil
omega.nat.dnf_core (t ≤* s) = [(list.nil omega.term, [(omega.nat.canonize s).sub (omega.nat.canonize t)])]
omega.nat.dnf_core (t =* s) = [([(omega.nat.canonize s).sub (omega.nat.canonize t)], list.nil omega.term)]

theorem omega.nat.exists_clause_holds_core {v : ℕ → ℕ} {p : omega.nat.preform} :

p.neg_free → p.sub_free → omega.nat.preform.holds v p → (∃ (c : omega.clause) (H : c ∈ omega.nat.dnf_core p), omega.clause.holds (λ (x : ℕ), ↑(v x)) c)

source

def omega.nat.term.vars_core (is : list ℤ) :

list bool

Equations

omega.nat.term.vars_core is = list.map (λ (i : ℤ), ite (i = 0) ff tt) is

source

def omega.nat.term.vars (t : omega.term) :

list bool

Return a list of bools that encodes which variables have nonzero coefficients

Equations

omega.nat.term.vars t = omega.nat.term.vars_core t.snd

source

def omega.nat.bools.or :

list bool → list bool → list bool

Equations

omega.nat.bools.or (b1 :: bs1) (b2 :: bs2) = (b1 || b2) :: omega.nat.bools.or bs1 bs2
omega.nat.bools.or (hd :: tl) list.nil = hd :: tl
omega.nat.bools.or list.nil (hd :: tl) = hd :: tl
omega.nat.bools.or list.nil list.nil = list.nil

source

def omega.nat.terms.vars :

list omega.term → list bool

Return a list of bools that encodes which variables have nonzero coefficients in any one of the input terms.

Equations

omega.nat.terms.vars (t :: ts) = omega.nat.bools.or (omega.nat.term.vars t) (omega.nat.terms.vars ts)
omega.nat.terms.vars list.nil = list.nil

source

def omega.nat.nonneg_consts_core :

ℕ → list bool → list omega.term

Equations

omega.nat.nonneg_consts_core k (tt :: bs) = (0, list.nil {k ↦ 1}) :: omega.nat.nonneg_consts_core (k + 1) bs
omega.nat.nonneg_consts_core k (ff :: bs) = omega.nat.nonneg_consts_core (k + 1) bs
omega.nat.nonneg_consts_core _x list.nil = list.nil

source

def omega.nat.nonneg_consts (bs : list bool) :

list omega.term

Equations

omega.nat.nonneg_consts bs = omega.nat.nonneg_consts_core 0 bs

source

def omega.nat.nonnegate :

omega.clause → omega.clause

Equations

omega.nat.nonnegate (eqs, les) = let xs : list bool := omega.nat.terms.vars eqs, ys : list bool := omega.nat.terms.vars les, bs : list bool := omega.nat.bools.or xs ys in (eqs, omega.nat.nonneg_consts bs ++ les)

source

def omega.nat.dnf (p : omega.nat.preform) :

list omega.clause

DNF transformation

Equations

omega.nat.dnf p = list.map omega.nat.nonnegate (omega.nat.dnf_core p)

source

theorem omega.nat.holds_nonneg_consts_core {v : ℕ → ℤ} (h1 : ∀ (x : ℕ), 0 ≤ v x) (m : ℕ) (bs : list bool) (t : omega.term) (H : t ∈ omega.nat.nonneg_consts_core m bs) :

0 ≤ omega.term.val v t

source

theorem omega.nat.holds_nonneg_consts {v : ℕ → ℤ} {bs : list bool} :

(∀ (x : ℕ), 0 ≤ v x) → ∀ (t : omega.term), t ∈ omega.nat.nonneg_consts bs → 0 ≤ omega.term.val v t

source

theorem omega.nat.exists_clause_holds {v : ℕ → ℕ} {p : omega.nat.preform} :

p.neg_free → p.sub_free → omega.nat.preform.holds v p → (∃ (c : omega.clause) (H : c ∈ omega.nat.dnf p), omega.clause.holds (λ (x : ℕ), ↑(v x)) c)

source

theorem omega.nat.exists_clause_sat {p : omega.nat.preform} :

p.neg_free → p.sub_free → p.sat → (∃ (c : omega.clause) (H : c ∈ omega.nat.dnf p), c.sat)

source

theorem omega.nat.unsat_of_unsat_dnf (p : omega.nat.preform) :

p.neg_free → p.sub_free → omega.clauses.unsat (omega.nat.dnf p) → p.unsat

mathlib documentation

DNF transformation #