mathlib3 documentation

tactic.omega.int.preterm

meta inductive omega.int.exprterm :

cst : ℤ → omega.int.exprterm
exp : ℤ → expr → omega.int.exprterm
add : omega.int.exprterm → omega.int.exprterm → omega.int.exprterm

The shadow syntax for arithmetic terms. All constants are reified to cst (e.g., -5 is reified to cst -5) and all other atomic terms are reified to exp (e.g., -5 * (gcd 14 -7) is reified to exp -5 \(gcd 14 -7)).expaccepts a coefficient of typeint` as its first argument because multiplication by constant is allowed by the omega test.

@[protected, instance]

meta def omega.int.preterm.has_reflect :

has_reflect omega.int.preterm

@[protected, instance]

def omega.int.preterm.inhabited :

inhabited omega.int.preterm

inductive omega.int.preterm :

cst : ℤ → omega.int.preterm
var : ℤ → ℕ → omega.int.preterm
add : omega.int.preterm → omega.int.preterm → omega.int.preterm

Similar to exprterm, except that all exprs are now replaced with de Brujin indices of type nat. This is akin to generalizing over the terms represented by the said exprs.

Instances for omega.int.preterm

@[simp]

def omega.int.preterm.val (v : ℕ → ℤ) :

omega.int.preterm → ℤ

Preterm evaluation

Equations

omega.int.preterm.val v (t1.add t2) = omega.int.preterm.val v t1 + omega.int.preterm.val v t2
omega.int.preterm.val v (omega.int.preterm.var i n) = ite (i = 1) (v n) (ite (i = -1) (-v n) (v n * i))
omega.int.preterm.val v (omega.int.preterm.cst i) = i

def omega.int.preterm.fresh_index :

omega.int.preterm → ℕ

Fresh de Brujin index not used by any variable in argument

Equations

(t1.add t2).fresh_index = linear_order.max t1.fresh_index t2.fresh_index
(omega.int.preterm.var i n).fresh_index = n + 1
(omega.int.preterm.cst _x).fresh_index = 0

@[simp]

def omega.int.preterm.add_one (t : omega.int.preterm) :

omega.int.preterm

Equations

t.add_one = t.add (omega.int.preterm.cst 1)

def omega.int.preterm.repr :

omega.int.preterm → string

Equations

(t1.add t2).repr = "(" ++ t1.repr ++ " + " ++ t2.repr ++ ")"
(omega.int.preterm.var i n).repr = i.repr ++ "*x" ++ n.repr
(omega.int.preterm.cst i).repr = i.repr

@[simp]

def omega.int.canonize :

omega.int.preterm → omega.term

Return a term (which is in canonical form by definition) that is equivalent to the input preterm

Equations

omega.int.canonize (t1.add t2) = (omega.int.canonize t1).add (omega.int.canonize t2)
omega.int.canonize (omega.int.preterm.var i n) = (0, list.func.set i list.nil n)
omega.int.canonize (omega.int.preterm.cst i) = (i, list.nil ℤ)

@[simp]

theorem omega.int.val_canonize {v : ℕ → ℤ} {t : omega.int.preterm} :

omega.term.val v (omega.int.canonize t) = omega.int.preterm.val v t