# mathlibdocumentation

tactic.omega.nat.preterm

meta inductive omega.nat.exprterm  :
Type
• cst :
• exp :
• sub :

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 * (list.length l) is reified to exp 5 \(list.length l)).expaccepts a coefficient of typenat as its first argument because multiplication by constant is allowed by the omega test.

@[instance]
@[instance]
@[instance]
inductive omega.nat.preterm  :
Type
• cst :
• var :
• sub :

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.

Helper tactic for proof by induction over preterms

def omega.nat.preterm.val (v : ) :

Preterm evaluation

Equations
@[simp]
theorem omega.nat.preterm.val_const {v : } {m : } :
= m
@[simp]
theorem omega.nat.preterm.val_var {v : } {m n : } :
(m ** n) = m * v n
@[simp]
theorem omega.nat.preterm.val_add {v : } {t s : omega.nat.preterm} :
(t +* s) =
@[simp]
theorem omega.nat.preterm.val_sub {v : } {t s : omega.nat.preterm} :
(t -* s) =

Fresh de Brujin index not used by any variable in argument

Equations
theorem omega.nat.preterm.val_constant (v w : ) (t : omega.nat.preterm) :
(∀ (x : ), x < t.fresh_indexv x = w x)

If variable assignments v and w agree on all variables that occur in term t, the value of t under v and w` are identical.

Equations
@[simp]
Equations

Preterm is free of subtractions

Equations
@[simp]

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

Equations
@[simp]
theorem omega.nat.val_canonize {v : } {t : omega.nat.preterm} :
t.sub_freeomega.term.val (λ (x : ), (v x)) =