tactic.omega.int.dnf - mathlib 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 ∧* q) = (omega.int.push_neg p ∨* omega.int.push_neg q)
omega.int.push_neg (p ∨* q) = (omega.int.push_neg p ∧* omega.int.push_neg q)
omega.int.push_neg (¬* p) = p
omega.int.push_neg (ᾰ ≤* ᾰ_1) = ¬* (ᾰ ≤* ᾰ_1)
omega.int.push_neg (ᾰ =* ᾰ_1) = ¬* (ᾰ =* ᾰ_1)

source

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

(omega.int.push_neg p).equiv (¬* p)

source

def omega.int.nnf :

omega.int.preform → omega.int.preform

NNF transformation

Equations

omega.int.nnf (p ∧* q) = (omega.int.nnf p ∧* omega.int.nnf q)
omega.int.nnf (p ∨* q) = (omega.int.nnf p ∨* omega.int.nnf q)
omega.int.nnf (¬* p) = omega.int.push_neg (omega.int.nnf p)
omega.int.nnf (ᾰ ≤* ᾰ_1) = (ᾰ ≤* ᾰ_1)
omega.int.nnf (ᾰ =* ᾰ_1) = (ᾰ =* ᾰ_1)

source

def omega.int.is_nnf :

omega.int.preform → Prop

Equations

omega.int.is_nnf (p ∧* q) = (omega.int.is_nnf p ∧ omega.int.is_nnf q)
omega.int.is_nnf (p ∨* q) = (omega.int.is_nnf p ∧ omega.int.is_nnf q)
omega.int.is_nnf (¬* (ᾰ ∧* ᾰ_1)) = false
omega.int.is_nnf (¬* (ᾰ ∨* ᾰ_1)) = false
omega.int.is_nnf (¬* ¬* ᾰ) = false
omega.int.is_nnf (¬* (t ≤* s)) = true
omega.int.is_nnf (¬* (t =* s)) = true
omega.int.is_nnf (t ≤* s) = true
omega.int.is_nnf (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 ∧* q) = (omega.int.neg_free p ∧ omega.int.neg_free q)
omega.int.neg_free (p ∨* q) = (omega.int.neg_free p ∧ omega.int.neg_free q)
omega.int.neg_free (¬* ᾰ) = false
omega.int.neg_free (t ≤* s) = true
omega.int.neg_free (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 ∧* q) = (omega.int.neg_elim p ∧* omega.int.neg_elim q)
omega.int.neg_elim (p ∨* q) = (omega.int.neg_elim p ∨* omega.int.neg_elim q)
omega.int.neg_elim (¬* (ᾰ ∧* ᾰ_1)) = ¬* (ᾰ ∧* ᾰ_1)
omega.int.neg_elim (¬* (ᾰ ∨* ᾰ_1)) = ¬* (ᾰ ∨* ᾰ_1)
omega.int.neg_elim (¬* ¬* ᾰ) = ¬* ¬* ᾰ
omega.int.neg_elim (¬* (t ≤* s)) = (s.add_one ≤* t)
omega.int.neg_elim (¬* (t =* s)) = (t.add_one ≤* s ∨* (s.add_one ≤* t))
omega.int.neg_elim (ᾰ ≤* ᾰ_1) = (ᾰ ≤* ᾰ_1)
omega.int.neg_elim (ᾰ =* ᾰ_1) = (ᾰ =* ᾰ_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 ∧* q) = list.map (λ (pq : omega.clause × omega.clause), pq.fst.append pq.snd) ((omega.int.dnf_core p).product (omega.int.dnf_core q))
omega.int.dnf_core (p ∨* q) = omega.int.dnf_core p ++ omega.int.dnf_core q
omega.int.dnf_core (¬* _x) = list.nil
omega.int.dnf_core (t ≤* s) = [(list.nil omega.term, [(omega.int.canonize s).sub (omega.int.canonize t)])]
omega.int.dnf_core (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

mathlib documentation

DNF transformation #