mathlib docs: tactic.omega.nat.dnf

@[simp]

def omega.nat.dnf_core (a : omega.nat.preform) :

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} (a : p.neg_free) (a_1 : p.sub_free) (a_2 : 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 (a a_1 : 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 (a : 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 (a : ℕ) (a_1 : 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 (a : 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} (a : ∀ (x : ℕ), 0 ≤ v x) (t : omega.term) (H : t ∈ omega.nat.nonneg_consts bs) :

0 ≤ omega.term.val v t

source

theorem omega.nat.exists_clause_holds {v : ℕ → ℕ} {p : omega.nat.preform} (a : p.neg_free) (a_1 : p.sub_free) (a_2 : 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} (a : p.neg_free) (a_1 : p.sub_free) (a_2 : 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) (a : p.neg_free) (a_1 : p.sub_free) (a_2 : omega.clauses.unsat (omega.nat.dnf p)) :

p.unsat