tactic.omega.clause - mathlib docs

Type

(([t₁,...tₘ],[s₁,...,sₙ]) : clause) encodes the constraints 0 = ⟦t₁⟧ ∧ ... ∧ 0 = ⟦tₘ⟧ ∧ 0 ≤ ⟦s₁⟧ ∧ ... ∧ 0 ≤ ⟦sₙ⟧, where ⟦t⟧ is the value of (t : term).

Equations

omega.clause = (list omega.term × list omega.term)

source

def omega.clause.holds (v : ℕ → ℤ) :

omega.clause → Prop

holds v c := clause c holds under valuation v

Equations

omega.clause.holds v (eqs, les) = ((∀ (t : omega.term), t ∈ eqs → 0 = omega.term.val v t) ∧ ∀ (t : omega.term), t ∈ les → 0 ≤ omega.term.val v t)

source

def omega.clause.sat (c : omega.clause) :

Prop

sat c := there exists a valuation v under which c holds

Equations

c.sat = ∃ (v : ℕ → ℤ), omega.clause.holds v c

source

def omega.clause.unsat (c : omega.clause) :

Prop

unsat c := there is no valuation v under which c holds

Equations

c.unsat = ¬c.sat

source

def omega.clause.append (c1 c2 : omega.clause) :

omega.clause

append two clauses by elementwise appending

Equations

c1.append c2 = (c1.fst ++ c2.fst, c1.snd ++ c2.snd)

source

theorem omega.clause.holds_append {v : ℕ → ℤ} {c1 c2 : omega.clause} :

omega.clause.holds v c1 → omega.clause.holds v c2 → omega.clause.holds v (c1.append c2)

source

def omega.clauses.sat (cs : list omega.clause) :

Prop

There exists a satisfiable clause c in argument

Equations

omega.clauses.sat cs = ∃ (c : omega.clause) (H : c ∈ cs), c.sat

source

def omega.clauses.unsat (cs : list omega.clause) :

Prop

There is no satisfiable clause c in argument

Equations

omega.clauses.unsat cs = ¬omega.clauses.sat cs

source

theorem omega.clauses.unsat_nil :

omega.clauses.unsat list.nil

source

theorem omega.clauses.unsat_cons (c : omega.clause) (cs : list omega.clause) :

c.unsat → omega.clauses.unsat cs → omega.clauses.unsat (c :: cs)