mathlib documentation

tactic.omega.nat.preterm

meta inductive omega.nat.exprterm :

Type

cst : ℕ → omega.nat.exprterm
exp : ℕ → expr → omega.nat.exprterm
add : omega.nat.exprterm → omega.nat.exprterm → omega.nat.exprterm
sub : omega.nat.exprterm → omega.nat.exprterm → omega.nat.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 * (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.

@[protected, instance]

meta def omega.nat.preterm.has_reflect :

has_reflect omega.nat.preterm

@[protected, instance]

def omega.nat.preterm.inhabited :

inhabited omega.nat.preterm

@[protected, instance]

def omega.nat.preterm.decidable_eq :

decidable_eq omega.nat.preterm

inductive omega.nat.preterm :

Type

cst : ℕ → omega.nat.preterm
var : ℕ → ℕ → omega.nat.preterm
add : omega.nat.preterm → omega.nat.preterm → omega.nat.preterm
sub : omega.nat.preterm → omega.nat.preterm → omega.nat.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.nat.preterm

meta def omega.nat.preterm.induce (tac : tactic unit := tactic.skip) :

Helper tactic for proof by induction over preterms

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

omega.nat.preterm → ℕ

Preterm evaluation

Equations

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

@[simp]

theorem omega.nat.preterm.val_const {v : ℕ → ℕ} {m : ℕ} :

omega.nat.preterm.val v (omega.nat.preterm.cst m) = m

@[simp]

theorem omega.nat.preterm.val_var {v : ℕ → ℕ} {m n : ℕ} :

omega.nat.preterm.val v (omega.nat.preterm.var m n) = m * v n

@[simp]

theorem omega.nat.preterm.val_add {v : ℕ → ℕ} {t s : omega.nat.preterm} :

omega.nat.preterm.val v (t.add s) = omega.nat.preterm.val v t + omega.nat.preterm.val v s

@[simp]

theorem omega.nat.preterm.val_sub {v : ℕ → ℕ} {t s : omega.nat.preterm} :

omega.nat.preterm.val v (t.sub s) = omega.nat.preterm.val v t - omega.nat.preterm.val v s

def omega.nat.preterm.fresh_index :

omega.nat.preterm → ℕ

Fresh de Brujin index not used by any variable in argument

Equations

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

theorem omega.nat.preterm.val_constant (v w : ℕ → ℕ) (t : omega.nat.preterm) :

(∀ (x : ℕ), x < t.fresh_index → v x = w x) → omega.nat.preterm.val v t = omega.nat.preterm.val w t

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.

def omega.nat.preterm.repr :

omega.nat.preterm → string

Equations

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

@[simp]

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

omega.nat.preterm

Equations

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

def omega.nat.preterm.sub_free :

omega.nat.preterm → Prop

Preterm is free of subtractions

Equations

(_x.sub _x_1).sub_free = false
(t.add s).sub_free = (t.sub_free ∧ s.sub_free)
(omega.nat.preterm.var m n).sub_free = true
(omega.nat.preterm.cst m).sub_free = true

@[simp]

def omega.nat.canonize :

omega.nat.preterm → omega.term

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

Equations

omega.nat.canonize (_x.sub _x_1) = (0, list.nil ℤ)
omega.nat.canonize (t.add s) = (omega.nat.canonize t).add (omega.nat.canonize s)
omega.nat.canonize (omega.nat.preterm.var m n) = (0, list.func.set ↑m list.nil n)
omega.nat.canonize (omega.nat.preterm.cst m) = (↑m, list.nil ℤ)

@[simp]

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

t.sub_free → omega.term.val (λ (x : ℕ), ↑(v x)) (omega.nat.canonize t) = ↑(omega.nat.preterm.val v t)