- 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.
- 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.
Helper tactic for proof by induction over preterms
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
Fresh de Brujin index not used by any variable in argument
Equations
- (t1.sub t2).fresh_index = max t1.fresh_index t2.fresh_index
- (t1.add t2).fresh_index = 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
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
- t.add_one = t.add (omega.nat.preterm.cst 1)
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 ℤ)