mathlib3 documentation

tactic.omega.nat.neg_elim

@[simp]

def omega.nat.push_neg :

omega.nat.preform → omega.nat.preform

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.nat.push_neg (p.and q) = (omega.nat.push_neg p).or (omega.nat.push_neg q)
omega.nat.push_neg (p.or q) = (omega.nat.push_neg p).and (omega.nat.push_neg q)
omega.nat.push_neg p.not = p
omega.nat.push_neg (omega.nat.preform.le ᾰ ᾰ_1) = (omega.nat.preform.le ᾰ ᾰ_1).not
omega.nat.push_neg (omega.nat.preform.eq ᾰ ᾰ_1) = (omega.nat.preform.eq ᾰ ᾰ_1).not

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

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

def omega.nat.nnf :

omega.nat.preform → omega.nat.preform

NNF transformation

Equations

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

def omega.nat.is_nnf :

omega.nat.preform → Prop

Asserts that the given preform is in NNF

Equations

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

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

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

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

omega.nat.is_nnf (omega.nat.nnf p)

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

(omega.nat.nnf p).equiv p

@[simp]

def omega.nat.neg_elim_core :

omega.nat.preform → omega.nat.preform

Equations

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

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

omega.nat.is_nnf p → (omega.nat.neg_elim_core p).neg_free

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

a ≤ b ∧ b ≤ a ↔ a = b

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

p.implies (omega.nat.neg_elim_core p)

def omega.nat.neg_elim :

omega.nat.preform → omega.nat.preform

Eliminate all negations in a preform

Equations

omega.nat.neg_elim = omega.nat.neg_elim_core ∘ omega.nat.nnf

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

(omega.nat.neg_elim p).neg_free

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

p.implies (omega.nat.neg_elim p)