mathlib3 documentation

tactic.omega.find_ees

source
structure omega.ee_state  :
Type

The state of equality elimination proof search. eqs is the list of equality constraints, and each t ∈ eqs represents the constraint 0 = t. Similarly, les is the list of inequality constraints, and each t ∈ eqs represents the constraint 0 < t. ees is the sequence of equality elimination steps that have been used so far to obtain the current set of constraints. The list ees grows over time until eqs becomes empty.

Instances for omega.ee_state
source
@[protected, instance]
def omega.ee_state.inhabited  :
inhabited omega.ee_state
source
@[reducible]
meta def omega.eqelim (α : Type) :
Type
source
meta def omega.abort {α : Type} :
omega.eqelim α
source
meta def omega.get_eqs  :
omega.eqelim (list omega.term)

Get the current list of equality constraints.

source
meta def omega.get_les  :
omega.eqelim (list omega.term)

Get the current list of inequality constraints.

source
meta def omega.get_ees  :
omega.eqelim (list omega.ee)

Get the current sequence of equality elimiation steps.

source
meta def omega.set_eqs (eqs : list omega.term) :
omega.eqelim unit

Update the list of equality constraints.

source
meta def omega.set_les (les : list omega.term) :
omega.eqelim unit

Update the list of inequality constraints.

source
meta def omega.set_ees (es : list omega.ee) :
omega.eqelim unit

Update the sequence of equality elimiation steps.

source
meta def omega.add_ee (e : omega.ee) :
omega.eqelim unit

Add a new step to the sequence of equality elimination steps.

source
meta def omega.head_eq  :
omega.eqelim omega.term

Return the first equality constraint in the current list of equality constraints. The returned constraint is 'popped' and no longer available in the state.

source
meta def omega.run {α : Type} (eqs les : list omega.term) (r : omega.eqelim α) :
tactic α
source
meta def omega.ee_commit {α β : Type} (t1 : omega.eqelim α) (t2 : omega.eqelim β) (t3 : α → omega.eqelim β) :
omega.eqelim β

If t1 succeeds and returns a value, 'commit' to that choice and run t3 with the returned value as argument. Do not backtrack to try t2 even if t3 fails. If t1 fails outright, run t2.

source
def omega.gcd  :
list ℤ → ℕ

GCD of all elements of the list.

Equations
source
meta def omega.get_gcd (t : omega.term) :
omega.eqelim ℤ

GCD of all coefficients in a term.

source
meta def omega.factor (i : ℤ) (t : omega.term) :
omega.eqelim omega.term

Divide a term by an integer if the integer divides the constant component of the term. It is assumed that the integer also divides all coefficients of the term.

source
meta def omega.find_min_coeff_core  :
list ℤ → omega.eqelim (ℤ × ℕ)

If list has a nonzero element, return the minimum element (by absolute value) with its index. Otherwise, return none.

source
meta def omega.find_min_coeff (t : omega.term) :
omega.eqelim (ℤ × ℕ × omega.term)

Find and return the smallest coefficient (by absolute value) in a term, along with the coefficient's variable index and the term itself. If the coefficient is negative, negate both the coefficient and the term before returning them.

source
meta def omega.elim_eq  :
omega.eqelim unit

Find an appropriate equality elimination step for the current state and apply it.

source
meta def omega.elim_eqs  :
omega.eqelim (list omega.ee)

Find and return the sequence of steps for eliminating all equality constraints in the current state.

source
meta def omega.find_ees  :
omega.clause → tactic (list omega.ee)

Given a linear constrain clause, return a list of steps for eliminating its equality constraints.