tactic.omega.int.dnf - mathlib3 docs

@[simp]

push_neg p returns the result of normalizing ¬ p by pushing the outermost negation all the way down, until it reaches either a negation or an atom

Equations

omega.int.push_neg (p.and q) = (omega.int.push_neg p).or (omega.int.push_neg q)
omega.int.push_neg (p.or q) = (omega.int.push_neg p).and (omega.int.push_neg q)
omega.int.push_neg p.not = p
omega.int.push_neg (omega.int.preform.le ᾰ ᾰ_1) = (omega.int.preform.le ᾰ ᾰ_1).not
omega.int.push_neg (omega.int.preform.eq ᾰ ᾰ_1) = (omega.int.preform.eq ᾰ ᾰ_1).not

source

theorem omega.int.push_neg_equiv {p : omega.int.preform} :

(omega.int.push_neg p).equiv p.not

source

def omega.int.nnf :

omega.int.preform → omega.int.preform

NNF transformation

Equations

omega.int.nnf (p.and q) = (omega.int.nnf p).and (omega.int.nnf q)
omega.int.nnf (p.or q) = (omega.int.nnf p).or (omega.int.nnf q)
omega.int.nnf p.not = omega.int.push_neg (omega.int.nnf p)
omega.int.nnf (omega.int.preform.le ᾰ ᾰ_1) = omega.int.preform.le ᾰ ᾰ_1
omega.int.nnf (omega.int.preform.eq ᾰ ᾰ_1) = omega.int.preform.eq ᾰ ᾰ_1

source

def omega.int.is_nnf :

omega.int.preform → Prop

Equations

omega.int.is_nnf (p.and q) = (omega.int.is_nnf p ∧ omega.int.is_nnf q)
omega.int.is_nnf (p.or q) = (omega.int.is_nnf p ∧ omega.int.is_nnf q)
omega.int.is_nnf (ᾰ.and ᾰ_1).not = false
omega.int.is_nnf (ᾰ.or ᾰ_1).not = false
omega.int.is_nnf ᾰ.not.not = false
omega.int.is_nnf (omega.int.preform.le t s).not = true
omega.int.is_nnf (omega.int.preform.eq t s).not = true
omega.int.is_nnf (omega.int.preform.le t s) = true
omega.int.is_nnf (omega.int.preform.eq t s) = true

source

theorem omega.int.is_nnf_push_neg (p : omega.int.preform) :

omega.int.is_nnf p → omega.int.is_nnf (omega.int.push_neg p)

source

def omega.int.neg_free :

omega.int.preform → Prop

Argument is free of negations

Equations

omega.int.neg_free (p.and q) = (omega.int.neg_free p ∧ omega.int.neg_free q)
omega.int.neg_free (p.or q) = (omega.int.neg_free p ∧ omega.int.neg_free q)
omega.int.neg_free ᾰ.not = false
omega.int.neg_free (omega.int.preform.le t s) = true
omega.int.neg_free (omega.int.preform.eq t s) = true

source

theorem omega.int.is_nnf_nnf (p : omega.int.preform) :

omega.int.is_nnf (omega.int.nnf p)

source

theorem omega.int.nnf_equiv {p : omega.int.preform} :

(omega.int.nnf p).equiv p

source

@[simp]

def omega.int.neg_elim :

omega.int.preform → omega.int.preform

Eliminate all negations from preform

Equations

omega.int.neg_elim (p.and q) = (omega.int.neg_elim p).and (omega.int.neg_elim q)
omega.int.neg_elim (p.or q) = (omega.int.neg_elim p).or (omega.int.neg_elim q)
omega.int.neg_elim (ᾰ.and ᾰ_1).not = (ᾰ.and ᾰ_1).not
omega.int.neg_elim (ᾰ.or ᾰ_1).not = (ᾰ.or ᾰ_1).not
omega.int.neg_elim ᾰ.not.not = ᾰ.not.not
omega.int.neg_elim (omega.int.preform.le t s).not = omega.int.preform.le s.add_one t
omega.int.neg_elim (omega.int.preform.eq t s).not = (omega.int.preform.le t.add_one s).or (omega.int.preform.le s.add_one t)
omega.int.neg_elim (omega.int.preform.le ᾰ ᾰ_1) = omega.int.preform.le ᾰ ᾰ_1
omega.int.neg_elim (omega.int.preform.eq ᾰ ᾰ_1) = omega.int.preform.eq ᾰ ᾰ_1

source

theorem omega.int.neg_free_neg_elim (p : omega.int.preform) :

omega.int.is_nnf p → omega.int.neg_free (omega.int.neg_elim p)

source

theorem omega.int.le_and_le_iff_eq {α : Type} [partial_order α] {a b : α} :

a ≤ b ∧ b ≤ a ↔ a = b

source

theorem omega.int.implies_neg_elim {p : omega.int.preform} :

p.implies (omega.int.neg_elim p)

source

@[simp]

def omega.int.dnf_core :

omega.int.preform → list omega.clause

Equations

omega.int.dnf_core (p.and q) = list.map (λ (pq : omega.clause × omega.clause), pq.fst.append pq.snd) (omega.int.dnf_core p ×ˢ omega.int.dnf_core q)
omega.int.dnf_core (p.or q) = omega.int.dnf_core p ++ omega.int.dnf_core q
omega.int.dnf_core _x.not = list.nil
omega.int.dnf_core (omega.int.preform.le t s) = [(list.nil omega.term, [(omega.int.canonize s).sub (omega.int.canonize t)])]
omega.int.dnf_core (omega.int.preform.eq t s) = [([(omega.int.canonize s).sub (omega.int.canonize t)], list.nil omega.term)]

source

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

list omega.clause

DNF transformation

Equations

omega.int.dnf p = omega.int.dnf_core (omega.int.neg_elim (omega.int.nnf p))

source

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

omega.int.neg_free p → omega.int.preform.holds v p → (∃ (c : omega.clause) (H : c ∈ omega.int.dnf_core p), omega.clause.holds v c)

source

theorem omega.int.clauses_sat_dnf_core {p : omega.int.preform} :

omega.int.neg_free p → p.sat → omega.clauses.sat (omega.int.dnf_core p)

source

theorem omega.int.unsat_of_clauses_unsat {p : omega.int.preform} :

omega.clauses.unsat (omega.int.dnf p) → p.unsat

mathlib3 documentation

DNF transformation #