mathlib documentation

tactic.omega.eq_elim

def omega.symdiv (i j : ℤ) :

Equations

omega.symdiv i j = ite (2 * (i % j) < j) (i / j) (i / j + 1)

def omega.symmod (i j : ℤ) :

Equations

omega.symmod i j = ite (2 * (i % j) < j) (i % j) (i % j - j)

theorem omega.symmod_add_one_self {i : ℤ} :

0 < i → omega.symmod i (i + 1) = -1

theorem omega.mul_symdiv_eq {i j : ℤ} :

j * omega.symdiv i j = i - omega.symmod i j

theorem omega.symmod_eq {i j : ℤ} :

omega.symmod i j = i - j * omega.symdiv i j

def omega.sgm (v : ℕ → ℤ) (b : ℤ) (as : list ℤ) (n : ℕ) :

(sgm v b as n) is the new value assigned to the nth variable after a single step of equality elimination using valuation v, term ⟨b, as⟩, and variable index n. If v satisfies the initial constraint set, then (v ⟨n ↦ sgm v b as n⟩) satisfies the new constraint set after equality elimination.

Equations

omega.sgm v b as n = let a_n : ℤ := list.func.get n as, m : ℤ := a_n + 1 in (omega.symmod b m + omega.coeffs.val v (list.map (λ (x : ℤ), omega.symmod x m) as)) / m

def omega.rhs :

ℕ → ℤ → list ℤ → omega.term

Equations

omega.rhs n b as = let m : ℤ := list.func.get n as + 1 in (omega.symmod b m, (list.map (λ (x : ℤ), omega.symmod x m) as) {n ↦ -m})

theorem omega.rhs_correct_aux {v : ℕ → ℤ} {m : ℤ} {as : list ℤ} {k : ℕ} :

∃ (d : ℤ), m * d + omega.coeffs.val_between v (list.map (λ (x : ℤ), omega.symmod x m) as) 0 k = omega.coeffs.val_between v as 0 k

theorem omega.rhs_correct {v : ℕ → ℤ} {b : ℤ} {as : list ℤ} (n : ℕ) :

0 < list.func.get n as → 0 = omega.term.val v (b, as) → v n = omega.term.val v ⟨n ↦ omega.sgm v b as n⟩ (omega.rhs n b as)

def omega.sym_sym (m b : ℤ) :

Equations

omega.sym_sym m b = omega.symdiv b m + omega.symmod b m

def omega.coeffs_reduce :

ℕ → ℤ → list ℤ → omega.term

Equations

omega.coeffs_reduce n b as = let a : ℤ := list.func.get n as, m : ℤ := a + 1 in (omega.sym_sym m b, (list.map (omega.sym_sym m) as) {n ↦ -a})

theorem omega.coeffs_reduce_correct {v : ℕ → ℤ} {b : ℤ} {as : list ℤ} {n : ℕ} :

0 < list.func.get n as → 0 = omega.term.val v (b, as) → 0 = omega.term.val v ⟨n ↦ omega.sgm v b as n⟩ (omega.coeffs_reduce n b as)

def omega.cancel (m : ℕ) (t1 t2 : omega.term) :

Equations

omega.cancel m t1 t2 = (omega.term.mul (-list.func.get m t2.snd) t1).add t2

def omega.subst (n : ℕ) (t1 t2 : omega.term) :

Equations

omega.subst n t1 t2 = (omega.term.mul (list.func.get n t2.snd) t1).add (t2.fst, t2.snd {n ↦ 0})

theorem omega.subst_correct {v : ℕ → ℤ} {b : ℤ} {as : list ℤ} {t : omega.term} {n : ℕ} :

0 < list.func.get n as → 0 = omega.term.val v (b, as) → omega.term.val v t = omega.term.val v ⟨n ↦ omega.sgm v b as n⟩ (omega.subst n (omega.rhs n b as) t)

@[protected, instance]

def omega.ee.inhabited :

inhabited omega.ee

@[protected, instance]

meta def omega.ee.has_reflect :

has_reflect omega.ee

inductive omega.ee :

Type

drop : omega.ee
nondiv : ℤ → omega.ee
factor : ℤ → omega.ee
neg : omega.ee
reduce : ℕ → omega.ee
cancel : ℕ → omega.ee

The type of equality elimination rules.

def omega.ee.repr :

omega.ee → string

Equations

(omega.ee.cancel n).repr = "+" ++ n.repr
(omega.ee.reduce n).repr = "≻" ++ n.repr
omega.ee.neg.repr = "-"
(omega.ee.factor i).repr = "/" ++ i.repr
(omega.ee.nondiv i).repr = i.repr ++ "∤"
omega.ee.drop.repr = "↓"

@[protected, instance]

def omega.ee.has_repr :

has_repr omega.ee

Equations

omega.ee.has_repr = {repr := omega.ee.repr}

@[protected, instance]

meta def omega.ee.has_to_format :

has_to_format omega.ee

def omega.eq_elim :

list omega.ee → omega.clause → omega.clause

Apply a given sequence of equality elimination steps to a clause.

Equations

omega.eq_elim (omega.ee.cancel m :: es) (eq :: eqs, les) = omega.eq_elim es (list.map (omega.cancel m eq) eqs, list.map (omega.cancel m eq) les)
omega.eq_elim (omega.ee.cancel ᾰ :: _x) (list.nil omega.term, les) = (list.nil omega.term, list.nil omega.term)
omega.eq_elim (omega.ee.reduce n :: es) ((b, as) :: eqs, les) = ite (0 < list.func.get n as) (let eq' : omega.term := omega.coeffs_reduce n b as, r : omega.term := omega.rhs n b as, eqs' : list omega.term := list.map (omega.subst n r) eqs, les' : list omega.term := list.map (omega.subst n r) les in omega.eq_elim es (eq' :: eqs', les')) (list.nil omega.term, list.nil omega.term)
omega.eq_elim (omega.ee.reduce ᾰ :: _x) (list.nil omega.term, les) = (list.nil omega.term, list.nil omega.term)
omega.eq_elim (omega.ee.neg :: es) (eq :: eqs, les) = omega.eq_elim es (eq.neg :: eqs, les)
omega.eq_elim (omega.ee.neg :: _x) (list.nil omega.term, les) = (list.nil omega.term, list.nil omega.term)
omega.eq_elim (omega.ee.factor i :: es) ((b, as) :: eqs, les) = ite (i ∣ b ∧ ∀ (x : ℤ), x ∈ as → i ∣ x) (omega.eq_elim es (omega.term.div i (b, as) :: eqs, les)) (list.nil omega.term, list.nil omega.term)
omega.eq_elim (omega.ee.factor ᾰ :: _x) (list.nil omega.term, les) = (list.nil omega.term, list.nil omega.term)
omega.eq_elim (omega.ee.nondiv i :: es) ((b, as) :: eqs, les) = ite (¬i ∣ b ∧ ∀ (x : ℤ), x ∈ as → i ∣ x) (list.nil omega.term, [(-1, list.nil ℤ)]) (list.nil omega.term, list.nil omega.term)
omega.eq_elim (omega.ee.nondiv ᾰ :: _x) (list.nil omega.term, les) = (list.nil omega.term, list.nil omega.term)
omega.eq_elim (omega.ee.drop :: es) (eq :: eqs, les) = omega.eq_elim es (eqs, les)
omega.eq_elim (omega.ee.drop :: _x) (list.nil omega.term, les) = (list.nil omega.term, list.nil omega.term)
omega.eq_elim list.nil (_x :: _x_1, les) = (list.nil omega.term, list.nil omega.term)
omega.eq_elim list.nil (list.nil omega.term, les) = (list.nil omega.term, les)

theorem omega.sat_empty :

omega.clause.sat (list.nil omega.term, list.nil omega.term)

theorem omega.sat_eq_elim {es : list omega.ee} {c : omega.clause} :

c.sat → (omega.eq_elim es c).sat

theorem omega.unsat_of_unsat_eq_elim (ee : list omega.ee) (c : omega.clause) :

(omega.eq_elim ee c).unsat → c.unsat

If the result of equality elimination is unsatisfiable, the original clause is unsatisfiable.