mathlib3 documentation

tactic.omega.prove_unsats

source
meta def omega.prove_neg  :
ℤ → tactic expr

Return expr of proof that given int is negative

source
theorem omega.forall_mem_replicate_zero_eq_zero (m : ℕ) (x : ℤ) (H : x ∈ list.replicate m 0) :
x = 0
source
meta def omega.prove_forall_mem_eq_zero (is : list ℤ) :
tactic expr

Return expr of proof that elements of (replicate is.length 0) are all 0

source
meta def omega.prove_unsat_lin_comb (ks : list ℕ) (ts : list omega.term) :
tactic expr

Return expr of proof that the combination of linear constraints represented by ks and ts is unsatisfiable

source
meta def omega.prove_unsat_ef  :
omega.clause → tactic expr

Given a (([],les) : clause), return the expr of a term (t : clause.unsat ([],les)).

source
meta def omega.prove_unsat (c : omega.clause) :
tactic expr

Given a (c : clause), return the expr of a term (t : clause.unsat c)

source
meta def omega.prove_unsats  :
list omega.clause → tactic expr

Given a (cs : list clause), return the expr of a term (t : clauses.unsat cs)