norm_num
Evaluating arithmetic expressions including *
, +
, -
, ^
, ≤
.
Transitivity conversion: given two conversions (which take an
expression e
and returns (e', ⊢ e = e')
), produces another
conversion that combines them with transitivity, treating failures
as reflexivity conversions.
Faster version of mk_app ``bit0 [e]
.
Faster version of mk_app ``bit1 [e]
.
- zero : norm_num.match_numeral_result
- one : norm_num.match_numeral_result
- bit0 : expr → norm_num.match_numeral_result
- bit1 : expr → norm_num.match_numeral_result
- other : norm_num.match_numeral_result
The result type of match_numeral
, either 0
, 1
, or a top level
decomposition of bit0 e
or bit1 e
. The other
case means it is not a numeral.
Unfold the top level constructor of the numeral expression.
Given a
, b
natural numerals, proves ⊢ a + 1 = b
, assuming that this is provable.
(It may prove garbage instead of failing if a + 1 = b
is false.)
Given a
,b
,r
natural numerals, proves ⊢ a + b = r
.
Given a
,b
,r
natural numerals, proves ⊢ a + b + 1 = r
.
Given a
,b
natural numerals, returns (r, ⊢ a + b = r)
.
Given a
,b
natural numerals, returns (r, ⊢ a * b = r)
.
Given a
a positive natural numeral, returns ⊢ 0 < a
.
Given a
a rational numeral, returns ⊢ 0 < a
.
Given a
a rational numeral, returns ⊢ a ≠ 0
.
Given a
nonnegative rational and d
a natural number, returns (b, ⊢ a * d = b)
.
(d
should be a multiple of the denominator of a
, so that b
is a natural number.)
Given a
a rational numeral, returns ⊢ 0 ≤ a
.
Given a
a rational numeral, returns ⊢ 1 ≤ a
.
Given a
,b
natural numerals, proves ⊢ a + 1 ≤ b
.
Given a
,b
natural numerals, proves ⊢ a ≤ b
.
Given a
,b
natural numerals, proves ⊢ a < b
.
Given a
,b
nonnegative rational numerals, proves ⊢ a < b
.
Given a
,b
rational numerals, proves ⊢ a < b
.
Given a
,b
nonnegative rational numerals, proves ⊢ a ≤ b
.
Given a
,b
rational numerals, proves ⊢ a ≤ b
.
Given a
,b
rational numerals, proves ⊢ a ≠ b
. This version tries to prove
⊢ a < b
or ⊢ b < a
, and so is not appropriate for types without an order relation.
Given a' : α
a natural numeral, returns (a : ℕ, ⊢ ↑a = a')
.
(Note that the returned value is on the left of the equality.)
Given a' : α
a natural numeral, returns (a : ℤ, ⊢ ↑a = a')
.
(Note that the returned value is on the left of the equality.)
Given a' : α
a natural numeral, returns (a : ℚ, ⊢ ↑a = a')
.
(Note that the returned value is on the left of the equality.)
Given a' : α
a nonnegative rational numeral, returns (a : ℚ, ⊢ ↑a = a')
.
(Note that the returned value is on the left of the equality.)
Given a' : α
an integer numeral, returns (a : ℤ, ⊢ ↑a = a')
.
(Note that the returned value is on the left of the equality.)
Given a' : α
a rational numeral, returns (a : ℚ, ⊢ ↑a = a')
.
(Note that the returned value is on the left of the equality.)
Given a
,b
rational numerals, proves ⊢ a ≠ b
. Currently it tries two methods:
- Prove
⊢ a < b
or⊢ b < a
, if the base type has an order - Embed
↑(a':ℚ) = a
and↑(b':ℚ) = b
, and then provea' ≠ b'
. This requires that the base type bechar_zero
, and also that it be adivision_ring
so that the coercion fromℚ
is well defined.
We may also add coercions to ℤ
and ℕ
as well in order to support char_zero
rings and semirings.
Given a
a rational numeral, returns ⊢ a ≠ 0
.
Given a
nonnegative rational and d
a natural number, returns (b, ⊢ a * d = b)
.
(d
should be a multiple of the denominator of a
, so that b
is a natural number.)
Given a
,b
,c
nonnegative rational numerals, returns ⊢ a + b = c
.
Given a
,b
,c
rational numerals, returns ⊢ a + b = c
.
Given a
,b
rational numerals, returns (c, ⊢ a + b = c)
.
Given a
a nonnegative rational numeral, returns (b, c, ⊢ a * b = c)
where b
and c
are natural numerals. (b
will be the denominator of a
.)
Given a
,b
nonnegative rational numerals, returns (c, ⊢ a * b = c)
.
Given a
,b
rational numerals, returns (c, ⊢ a * b = c)
.
Given a
a rational numeral, returns (b, ⊢ a⁻¹ = b)
.
Given a
,b
rational numerals, returns (c, ⊢ a / b = c)
.
Given a
a rational numeral, returns (b, ⊢ -a = b)
.
Given a
,b
rational numerals, returns (c, ⊢ a - b = c)
.
Evaluates the basic field operations +
,neg
,-
,*
,inv
,/
on numerals.
Also handles nat subtraction. Does not do recursive simplification; that is,
1 + 1 + 1
will not simplify but 2 + 1
will. This is handled by the top level
simp
call in norm_num.derive
.
Given a
a rational numeral and b : nat
, returns (c, ⊢ a ^ b = c)
.
Evaluates expressions of the form a ^ b
, monoid.pow a b
or nat.pow a b
.
Evaluates the expression nat.succ ... (nat.succ n)
where n
is a natural numeral.
(We could also just handle nat.succ n
here and rely on simp
to work bottom up, but we figure
that towers of successors coming from e.g. induction
are a common case.)
Given a
,b
numerals in nat
or int
,
prove_div_mod ic a b ff
returns(c, ⊢ a / b = c)
prove_div_mod ic a b tt
returns(c, ⊢ a % b = c)
An attribute for adding additional extensions to norm_num
. To use this attribute, put
@[norm_num]
on a tactic of type expr → tactic (expr × expr)
; the tactic will be called on
subterms by norm_num
, and it is responsible for identifying that the expression is a numerical
function applied to numerals, for example nat.fib 17
, and should return the reduced numerical
expression (which must be in norm_num
-normal form: a natural or rational numeral, i.e. 37
,
12 / 7
or -(2 / 3)
, although this can be an expression in any type), and the proof that the
original expression is equal to the rewritten expression.
Failure is used to indicate that this tactic does not apply to the term. For performance reasons, it is best to detect non-applicability as soon as possible so that the next tactic can have a go, so generally it will start with a pattern match and then checking that the arguments to the term are numerals or of the appropriate form, followed by proof construction, which should not fail.
Propositions are treated like any other term. The normal form for propositions is true
or
false
, so it should produce a proof of the form p = true
or p = false
. eq_true_intro
can be
used to help here.
Basic version of norm_num
that does not call simp
. It uses the provided step
tactic
to simplify the expression; use get_step
to get the default norm_num
set and derive.step
for
the basic builtin set of simplifications.
Normalize numerical expressions. It uses the provided step
tactic to simplify the expression;
use get_step
to get the default norm_num
set and derive.step
for the basic builtin set of
simplifications.
Basic version of norm_num
that does not call simp
.
Normalize numerical expressions. Supports the operations
+
-
*
/
^
and %
over numerical types such as
ℕ
, ℤ
, ℚ
, ℝ
, ℂ
and some general algebraic types,
and can prove goals of the form A = B
, A ≠ B
, A < B
and A ≤ B
,
where A
and B
are numerical expressions.
It also has a relatively simple primality prover.
Normalizes a numerical expression and tries to close the goal with the result.
Basic version of norm_num
that does not call simp
.
Normalize numerical expressions. Supports the operations
+
-
*
/
^
and %
over numerical types such as
ℕ
, ℤ
, ℚ
, ℝ
, ℂ
and some general algebraic types,
and can prove goals of the form A = B
, A ≠ B
, A < B
and A ≤ B
,
where A
and B
are numerical expressions.
It also has a relatively simple primality prover.