Evaluating arithmetic expressions including
Each lemma in this file is written the way it is to exactly match (with no defeq reduction allowed) the conclusion of some lemma generated by the proof procedure that uses it. That proof procedure should describe the shape of the generated lemma in its docstring.
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
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.
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
false, so it should produce a proof of the form
p = true or
p = false.
eq_true_intro can be
used to help here.
Normalises numerical expressions. It supports the operations
numerical types such as
ℂ, and can prove goals of the form
A = B,
A ≠ B,
A < B and
A ≤ B, where
B are numerical expressions.
Add-on tactics marked as
@[norm_num] can extend the behavior of
norm_num to include other
functions. This is used to support several other functions on
import data.real.basic example : (2 : ℝ) + 2 = 4 := by norm_num example : (12345.2 : ℝ) ≠ 12345.3 := by norm_num example : (73 : ℝ) < 789/2 := by norm_num example : 123456789 + 987654321 = 1111111110 := by norm_num example (R : Type*) [ring R] : (2 : R) + 2 = 4 := by norm_num example (F : Type*) [linear_ordered_field F] : (2 : F) + 2 < 5 := by norm_num example : nat.prime (2^13 - 1) := by norm_num example : ¬ nat.prime (2^11 - 1) := by norm_num example (x : ℝ) (h : x = 123 + 456) : x = 579 := by norm_num at h; assumption
norm_num1 does not call
norm_num1 can be called inside the
apply_normed normalises a numerical expression and tries to close the goal with
the result. Compare:
def a : ℕ := 2^100 #print a -- 2 ^ 100 def normed_a : ℕ := by apply_normed 2^100 #print normed_a -- 1267650600228229401496703205376 ```
#norm_num command #
A user command to run
norm_num. Mostly copied from the
The basic usage is
#norm_num e, where
e is an expression,
which will print the
norm_num form of
[ simp lemma list
with simp sets)?
This accepts the same options as the
You can specify additional simp lemmas as usual, for example using
#norm_num [f, g] : e, or
#norm_num with attr : e.
(The colon is optional but helpful for the parser.)
norm_num to using only the provided lemmas, and so
#norm_num only : e behaves similarly to
norm_num, this command does not fail when no simplifications are made.
#norm_num understands local variables, so you can use them to