@[simp]
Equations
- omega.nat.dnf_core (p.and 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.or q) = omega.nat.dnf_core p ++ omega.nat.dnf_core q
- omega.nat.dnf_core _x.not = list.nil
- omega.nat.dnf_core (omega.nat.preform.le t s) = [(list.nil omega.term, [(omega.nat.canonize s).sub (omega.nat.canonize t)])]
- omega.nat.dnf_core (omega.nat.preform.eq 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)
Return a list of bools that encodes which variables have nonzero coefficients
Equations
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
Return a list of bools that encodes which variables have nonzero coefficients in any one of the input terms
Equations
Equations
- omega.nat.nonneg_consts_core k (bool.tt :: bs) = (0, list.func.set 1 list.nil k) :: omega.nat.nonneg_consts_core (k + 1) bs
- omega.nat.nonneg_consts_core k (bool.ff :: bs) = omega.nat.nonneg_consts_core (k + 1) bs
- omega.nat.nonneg_consts_core _x list.nil = list.nil
Equations
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)
DNF transformation
Equations
theorem
omega.nat.holds_nonneg_consts_core
{v : ℕ → ℤ}
(h1 : ∀ (x : ℕ), 0 ≤ v x)
(m : ℕ)
(bs : list bool)
(t : omega.term) :
t ∈ omega.nat.nonneg_consts_core m bs → 0 ≤ omega.term.val v t
theorem
omega.nat.holds_nonneg_consts
{v : ℕ → ℤ}
{bs : list bool}
(a : ∀ (x : ℕ), 0 ≤ v x)
(t : omega.term) :
t ∈ omega.nat.nonneg_consts bs → 0 ≤ omega.term.val v t
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)
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)
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