tactic.norm_num

# `norm_num`#

Evaluating arithmetic expressions including `*`, `+`, `-`, `^`, `≤`.

Faster version of `mk_app ``bit0 [e]`.

Faster version of `mk_app ``bit1 [e]`.

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.

theorem norm_num.subst_into_add {α : Type u_1} [has_add α] (l r tl tr t : α) (prl : l = tl) (prr : r = tr) (prt : tl + tr = t) :
l + r = t
theorem norm_num.subst_into_mul {α : Type u_1} [has_mul α] (l r tl tr t : α) (prl : l = tl) (prr : r = tr) (prt : tl * tr = t) :
l * r = t
theorem norm_num.subst_into_neg {α : Type u_1} [has_neg α] (a ta t : α) (pra : a = ta) (prt : -ta = t) :
-a = t
meta inductive 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.

theorem norm_num.zero_succ {α : Type u_1} [semiring α] :
0 + 1 = 1
theorem norm_num.one_succ {α : Type u_1} [semiring α] :
1 + 1 = 2
theorem norm_num.bit0_succ {α : Type u_1} [semiring α] (a : α) :
bit0 a + 1 = bit1 a
theorem norm_num.bit1_succ {α : Type u_1} [semiring α] (a b : α) (h : a + 1 = b) :
bit1 a + 1 = bit0 b

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.)

meta def norm_num.prove_succ' (a : expr) :

Given `a` natural numeral, returns `(b, ⊢ a + 1 = b)`.

theorem norm_num.zero_adc {α : Type u_1} [semiring α] (a b : α) (h : a + 1 = b) :
0 + a + 1 = b
theorem norm_num.adc_zero {α : Type u_1} [semiring α] (a b : α) (h : a + 1 = b) :
a + 0 + 1 = b
theorem norm_num.one_add {α : Type u_1} [semiring α] (a b : α) (h : a + 1 = b) :
1 + a = b
theorem norm_num.add_bit0_bit0 {α : Type u_1} [semiring α] (a b c : α) (h : a + b = c) :
bit0 a + bit0 b = bit0 c
theorem norm_num.add_bit0_bit1 {α : Type u_1} [semiring α] (a b c : α) (h : a + b = c) :
bit0 a + bit1 b = bit1 c
theorem norm_num.add_bit1_bit0 {α : Type u_1} [semiring α] (a b c : α) (h : a + b = c) :
bit1 a + bit0 b = bit1 c
theorem norm_num.add_bit1_bit1 {α : Type u_1} [semiring α] (a b c : α) (h : a + b + 1 = c) :
bit1 a + bit1 b = bit0 c
theorem norm_num.adc_one_one {α : Type u_1} [semiring α] :
1 + 1 + 1 = 3
theorem norm_num.adc_bit0_one {α : Type u_1} [semiring α] (a b : α) (h : a + 1 = b) :
bit0 a + 1 + 1 = bit0 b
theorem norm_num.adc_one_bit0 {α : Type u_1} [semiring α] (a b : α) (h : a + 1 = b) :
1 + bit0 a + 1 = bit0 b
theorem norm_num.adc_bit1_one {α : Type u_1} [semiring α] (a b : α) (h : a + 1 = b) :
bit1 a + 1 + 1 = bit1 b
theorem norm_num.adc_one_bit1 {α : Type u_1} [semiring α] (a b : α) (h : a + 1 = b) :
1 + bit1 a + 1 = bit1 b
theorem norm_num.adc_bit0_bit0 {α : Type u_1} [semiring α] (a b c : α) (h : a + b = c) :
bit0 a + bit0 b + 1 = bit1 c
theorem norm_num.adc_bit1_bit0 {α : Type u_1} [semiring α] (a b c : α) (h : a + b + 1 = c) :
bit1 a + bit0 b + 1 = bit0 c
theorem norm_num.adc_bit0_bit1 {α : Type u_1} [semiring α] (a b c : α) (h : a + b + 1 = c) :
bit0 a + bit1 b + 1 = bit0 c
theorem norm_num.adc_bit1_bit1 {α : Type u_1} [semiring α] (a b c : α) (h : a + b + 1 = c) :
bit1 a + bit1 b + 1 = bit1 c

Given `a`,`b`,`r` natural numerals, proves `⊢ a + b = r`.

Given `a`,`b`,`r` natural numerals, proves `⊢ a + b + 1 = r`.

meta def norm_num.prove_add_nat' (a b : expr) :

Given `a`,`b` natural numerals, returns `(r, ⊢ a + b = r)`.

theorem norm_num.bit0_mul {α : Type u_1} [semiring α] (a b c : α) (h : a * b = c) :
bit0 a * b = bit0 c
theorem norm_num.mul_bit0' {α : Type u_1} [semiring α] (a b c : α) (h : a * b = c) :
a * bit0 b = bit0 c
theorem norm_num.mul_bit0_bit0 {α : Type u_1} [semiring α] (a b c : α) (h : a * b = c) :
bit0 a * bit0 b = bit0 (bit0 c)
theorem norm_num.mul_bit1_bit1 {α : Type u_1} [semiring α] (a b c d e : α) (hc : a * b = c) (hd : a + b = d) (he : bit0 c + d = e) :
bit1 a * bit1 b = bit1 e

Given `a`,`b` natural numerals, returns `(r, ⊢ a * b = r)`.

theorem norm_num.zero_lt_one {α : Type u}  :
0 < 1
meta def norm_num.prove_pos_nat  :

Given `a` a positive natural numeral, returns `⊢ 0 < a`.

meta def norm_num.prove_pos  :

Given `a` a rational numeral, returns `⊢ 0 < a`.

meta def norm_num.match_neg  :

`match_neg (- e) = some e`, otherwise `none`

meta def norm_num.match_sign  :

`match_sign (- e) = inl e`, `match_sign 0 = inr ff`, otherwise `inr tt`

theorem norm_num.ne_zero_of_pos {α : Type u_1} (a : α) :
0 < a a 0
theorem norm_num.ne_zero_neg {α : Type u_1} [add_group α] (a : α) :
a 0 -a 0

Given `a` a rational numeral, returns `⊢ a ≠ 0`.

theorem norm_num.clear_denom_div {α : Type u_1} (a b b' c d : α) (h₀ : b 0) (h₁ : b * b' = d) (h₂ : a * b' = c) :
a / b * d = c
meta def norm_num.prove_clear_denom' (prove_ne_zero : tactic.instance_cache ) (a d : expr) (na : ) (nd : ) :

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.)

theorem norm_num.nonneg_pos {α : Type u_1} (a : α) :
0 < a 0 a
theorem norm_num.lt_one_bit0 {α : Type u_1} (a : α) (h : 1 a) :
1 < bit0 a
theorem norm_num.lt_one_bit1 {α : Type u_1} (a : α) (h : 0 < a) :
1 < bit1 a
theorem norm_num.lt_bit0_bit0 {α : Type u_1} (a b : α) :
a < b bit0 a < bit0 b
theorem norm_num.lt_bit0_bit1 {α : Type u_1} (a b : α) (h : a b) :
bit0 a < bit1 b
theorem norm_num.lt_bit1_bit0 {α : Type u_1} (a b : α) (h : a + 1 b) :
bit1 a < bit0 b
theorem norm_num.lt_bit1_bit1 {α : Type u_1} (a b : α) :
a < b bit1 a < bit1 b
theorem norm_num.le_one_bit0 {α : Type u_1} (a : α) (h : 1 a) :
1 bit0 a
theorem norm_num.le_one_bit1 {α : Type u_1} (a : α) (h : 0 < a) :
1 bit1 a
theorem norm_num.le_bit0_bit0 {α : Type u_1} (a b : α) :
a b bit0 a bit0 b
theorem norm_num.le_bit0_bit1 {α : Type u_1} (a b : α) (h : a b) :
theorem norm_num.le_bit1_bit0 {α : Type u_1} (a b : α) (h : a + 1 b) :
theorem norm_num.le_bit1_bit1 {α : Type u_1} (a b : α) :
a b bit1 a bit1 b
theorem norm_num.sle_one_bit0 {α : Type u_1} (a : α) :
1 a 1 + 1 bit0 a
theorem norm_num.sle_one_bit1 {α : Type u_1} (a : α) :
1 a 1 + 1 bit1 a
theorem norm_num.sle_bit0_bit0 {α : Type u_1} (a b : α) :
a + 1 b bit0 a + 1 bit0 b
theorem norm_num.sle_bit0_bit1 {α : Type u_1} (a b : α) (h : a b) :
bit0 a + 1 bit1 b
theorem norm_num.sle_bit1_bit0 {α : Type u_1} (a b : α) (h : a + 1 b) :
bit1 a + 1 bit0 b
theorem norm_num.sle_bit1_bit1 {α : Type u_1} (a b : α) (h : a + 1 b) :
bit1 a + 1 bit1 b

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`.

theorem norm_num.clear_denom_lt {α : Type u_1} (a a' b b' d : α) (h₀ : 0 < d) (ha : a * d = a') (hb : b * d = b') (h : a' < b') :
a < b
meta def norm_num.prove_lt_nonneg_rat (ic : tactic.instance_cache) (a b : expr) (na nb : ) :

Given `a`,`b` nonnegative rational numerals, proves `⊢ a < b`.

theorem norm_num.lt_neg_pos {α : Type u_1} (a b : α) (ha : 0 < a) (hb : 0 < b) :
-a < b
meta def norm_num.prove_lt_rat (ic : tactic.instance_cache) (a b : expr) (na nb : ) :

Given `a`,`b` rational numerals, proves `⊢ a < b`.

theorem norm_num.clear_denom_le {α : Type u_1} (a a' b b' d : α) (h₀ : 0 < d) (ha : a * d = a') (hb : b * d = b') (h : a' b') :
a b
meta def norm_num.prove_le_nonneg_rat (ic : tactic.instance_cache) (a b : expr) (na nb : ) :

Given `a`,`b` nonnegative rational numerals, proves `⊢ a ≤ b`.

theorem norm_num.le_neg_pos {α : Type u_1} (a b : α) (ha : 0 a) (hb : 0 b) :
-a b
meta def norm_num.prove_le_rat (ic : tactic.instance_cache) (a b : expr) (na nb : ) :

Given `a`,`b` rational numerals, proves `⊢ a ≤ b`.

meta def norm_num.prove_ne_rat (ic : tactic.instance_cache) (a b : expr) (na nb : ) :

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.

theorem norm_num.nat_cast_zero {α : Type u_1} [semiring α] :
0 = 0
theorem norm_num.nat_cast_one {α : Type u_1} [semiring α] :
1 = 1
theorem norm_num.nat_cast_bit0 {α : Type u_1} [semiring α] (a : ) (a' : α) (h : a = a') :
(bit0 a) = bit0 a'
theorem norm_num.nat_cast_bit1 {α : Type u_1} [semiring α] (a : ) (a' : α) (h : a = a') :
(bit1 a) = bit1 a'
theorem norm_num.int_cast_zero {α : Type u_1} [ring α] :
0 = 0
theorem norm_num.int_cast_one {α : Type u_1} [ring α] :
1 = 1
theorem norm_num.int_cast_bit0 {α : Type u_1} [ring α] (a : ) (a' : α) (h : a = a') :
(bit0 a) = bit0 a'
theorem norm_num.int_cast_bit1 {α : Type u_1} [ring α] (a : ) (a' : α) (h : a = a') :
(bit1 a) = bit1 a'
theorem norm_num.rat_cast_bit0 {α : Type u_1} [char_zero α] (a : ) (a' : α) (h : a = a') :
(bit0 a) = bit0 a'
theorem norm_num.rat_cast_bit1 {α : Type u_1} [char_zero α] (a : ) (a' : α) (h : a = a') :
(bit1 a) = bit1 a'

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.)

meta def norm_num.prove_rat_uncast_nat (ic qc : tactic.instance_cache) (cz_inst a' : expr) :

Given `a' : α` a natural numeral, returns `(a : ℚ, ⊢ ↑a = a')`. (Note that the returned value is on the left of the equality.)

theorem norm_num.rat_cast_div {α : Type u_1} [char_zero α] (a b : ) (a' b' : α) (ha : a = a') (hb : b = b') :
(a / b) = a' / b'
meta def norm_num.prove_rat_uncast_nonneg (ic qc : tactic.instance_cache) (cz_inst a' : expr) (na' : ) :

Given `a' : α` a nonnegative rational numeral, returns `(a : ℚ, ⊢ ↑a = a')`. (Note that the returned value is on the left of the equality.)

theorem norm_num.int_cast_neg {α : Type u_1} [ring α] (a : ) (a' : α) (h : a = a') :
-a = -a'
theorem norm_num.rat_cast_neg {α : Type u_1} (a : ) (a' : α) (h : a = a') :
-a = -a'

Given `a' : α` an integer numeral, returns `(a : ℤ, ⊢ ↑a = a')`. (Note that the returned value is on the left of the equality.)

meta def norm_num.prove_rat_uncast (ic qc : tactic.instance_cache) (cz_inst a' : expr) (na' : ) :

Given `a' : α` a rational numeral, returns `(a : ℚ, ⊢ ↑a = a')`. (Note that the returned value is on the left of the equality.)

theorem norm_num.nat_cast_ne {α : Type u_1} [semiring α] [char_zero α] (a b : ) (a' b' : α) (ha : a = a') (hb : b = b') (h : a b) :
a' b'
theorem norm_num.int_cast_ne {α : Type u_1} [ring α] [char_zero α] (a b : ) (a' b' : α) (ha : a = a') (hb : b = b') (h : a b) :
a' b'
theorem norm_num.rat_cast_ne {α : Type u_1} [char_zero α] (a b : ) (a' b' : α) (ha : a = a') (hb : b = b') (h : a b) :
a' b'
meta def norm_num.prove_ne  :

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 prove `a' ≠ b'`. This requires that the base type be `char_zero`, and also that it be a `division_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.)

theorem norm_num.clear_denom_add {α : Type u_1} (a a' b b' c c' d : α) (h₀ : d 0) (ha : a * d = a') (hb : b * d = b') (hc : c * d = c') (h : a' + b' = c') :
a + b = c
meta def norm_num.prove_add_nonneg_rat (ic : tactic.instance_cache) (a b c : expr) (na nb nc : ) :

Given `a`,`b`,`c` nonnegative rational numerals, returns `⊢ a + b = c`.

theorem norm_num.add_pos_neg_pos {α : Type u_1} [add_group α] (a b c : α) (h : c + b = a) :
a + -b = c
theorem norm_num.add_pos_neg_neg {α : Type u_1} [add_group α] (a b c : α) (h : c + a = b) :
a + -b = -c
theorem norm_num.add_neg_pos_pos {α : Type u_1} [add_group α] (a b c : α) (h : a + c = b) :
-a + b = c
theorem norm_num.add_neg_pos_neg {α : Type u_1} [add_group α] (a b c : α) (h : b + c = a) :
-a + b = -c
theorem norm_num.add_neg_neg {α : Type u_1} [add_group α] (a b c : α) (h : b + a = c) :
-a + -b = -c
meta def norm_num.prove_add_rat (ic : tactic.instance_cache) (ea eb ec : expr) (a b c : ) :

Given `a`,`b`,`c` rational numerals, returns `⊢ a + b = c`.

Given `a`,`b` rational numerals, returns `(c, ⊢ a + b = c)`.

theorem norm_num.clear_denom_simple_nat {α : Type u_1} (a : α) :
1 0 a * 1 = a
theorem norm_num.clear_denom_simple_div {α : Type u_1} (a b : α) (h : b 0) :
b 0 a / b * b = a
meta def norm_num.prove_clear_denom_simple (a : expr) (na : ) :

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`.)

theorem norm_num.clear_denom_mul {α : Type u_1} [field α] (a a' b b' c c' d₁ d₂ d : α) (ha : d₁ 0 a * d₁ = a') (hb : d₂ 0 b * d₂ = b') (hc : c * d = c') (hd : d₁ * d₂ = d) (h : a' * b' = c') :
a * b = c
meta def norm_num.prove_mul_nonneg_rat (ic : tactic.instance_cache) (a b : expr) (na nb : ) :

Given `a`,`b` nonnegative rational numerals, returns `(c, ⊢ a * b = c)`.

theorem norm_num.mul_neg_pos {α : Type u_1} [ring α] (a b c : α) (h : a * b = c) :
-a * b = -c
theorem norm_num.mul_pos_neg {α : Type u_1} [ring α] (a b c : α) (h : a * b = c) :
a * -b = -c
theorem norm_num.mul_neg_neg {α : Type u_1} [ring α] (a b c : α) (h : a * b = c) :
-a * -b = c
meta def norm_num.prove_mul_rat (ic : tactic.instance_cache) (a b : expr) (na nb : ) :

Given `a`,`b` rational numerals, returns `(c, ⊢ a * b = c)`.

theorem norm_num.inv_neg {α : Type u_1} (a b : α) (h : a⁻¹ = b) :
(-a)⁻¹ = -b
theorem norm_num.inv_one {α : Type u_1}  :
1⁻¹ = 1
theorem norm_num.inv_one_div {α : Type u_1} (a : α) :
(1 / a)⁻¹ = a
theorem norm_num.inv_div_one {α : Type u_1} (a : α) :
a⁻¹ = 1 / a
theorem norm_num.inv_div {α : Type u_1} (a b : α) :
(a / b)⁻¹ = b / a
meta def norm_num.prove_inv  :

Given `a` a rational numeral, returns `(b, ⊢ a⁻¹ = b)`.

theorem norm_num.div_eq {α : Type u_1} (a b b' c : α) (hb : b⁻¹ = b') (h : a * b' = c) :
a / b = c
meta def norm_num.prove_div (ic : tactic.instance_cache) (a b : expr) (na nb : ) :

Given `a`,`b` rational numerals, returns `(c, ⊢ a / b = c)`.

meta def norm_num.prove_neg (ic : tactic.instance_cache) (a : expr) :

Given `a` a rational numeral, returns `(b, ⊢ -a = b)`.

theorem norm_num.sub_pos {α : Type u_1} [add_group α] (a b b' c : α) (hb : -b = b') (h : a + b' = c) :
a - b = c
theorem norm_num.sub_neg {α : Type u_1} [add_group α] (a b c : α) (h : a + b = c) :
a - -b = c
meta def norm_num.prove_sub (ic : tactic.instance_cache) (a b : expr) :

Given `a`,`b` rational numerals, returns `(c, ⊢ a - b = c)`.

theorem norm_num.sub_nat_pos (a b c : ) (h : b + c = a) :
a - b = c
theorem norm_num.sub_nat_neg (a b c : ) (h : a + c = b) :
a - b = 0

Given `a : nat`,`b : nat` natural 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`.

theorem norm_num.pow_bit0 {α : Type u} [monoid α] (a c' c : α) (b : ) (h : a ^ b = c') (h₂ : c' * c' = c) :
a ^ bit0 b = c
theorem norm_num.pow_bit1 {α : Type u} [monoid α] (a c₁ c₂ c : α) (b : ) (h : a ^ b = c₁) (h₂ : c₁ * c₁ = c₂) (h₃ : c₂ * a = c) :
a ^ bit1 b = c
meta def norm_num.prove_pow (a : expr) (na : ) :

Given `a` a rational numeral and `b : nat`, returns `(c, ⊢ a ^ b = c)`.

theorem norm_num.zpow_pos {α : Type u_1} (a : α) (b : ) (b' : ) (c : α) (hb : b = b') (h : a ^ b' = c) :
a ^ b = c
theorem norm_num.zpow_neg {α : Type u_1} (a : α) (b : ) (b' : ) (c c' : α) (b0 : 0 < b') (hb : b = b') (h : a ^ b' = c) (hc : c⁻¹ = c') :
a ^ -b = c'
meta def norm_num.prove_zpow (ic zc nc : tactic.instance_cache) (a : expr) (na : ) (b : expr) :

Given `a` a rational numeral and `b : ℤ`, returns `(c, ⊢ a ^ b = c)`.

Evaluates expressions of the form `a ^ b`, `monoid.npow a b` or `nat.pow a b`.

meta def norm_num.true_intro (p : expr) :

Given `⊢ p`, returns `(true, ⊢ p = true)`.

meta def norm_num.false_intro (p : expr) :

Given `⊢ ¬ p`, returns `(false, ⊢ p = false)`.

theorem norm_num.not_refl_false_intro {α : Sort u_1} (a : α) :
a a = false
@[nolint]
theorem norm_num.gt_intro {α : Type u_1} [has_lt α] (a b : α) (c : Prop) (h : a < b = c) :
b > a = c
@[nolint]
theorem norm_num.ge_intro {α : Type u_1} [has_le α] (a b : α) (c : Prop) (h : a b = c) :
b a = c

Evaluates the inequality operations `=`,`<`,`>`,`≤`,`≥`,`≠` on numerals.

theorem norm_num.nat_succ_eq (a b c : ) (h₁ : a = b) (h₂ : b + 1 = c) :
a.succ = c

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.)

theorem norm_num.int_to_nat_pos (a : ) (b : ) (h : b = a) :
a.to_nat = b
theorem norm_num.int_to_nat_neg (a : ) (h : 0 < a) :
(-a).to_nat = 0
theorem norm_num.nat_abs_pos (a : ) (b : ) (h : b = a) :
theorem norm_num.nat_abs_neg (a : ) (b : ) (h : b = a) :
(-a).nat_abs = b
theorem norm_num.neg_succ_of_nat (a b : ) (c : ) (h₁ : a + 1 = b) (h₂ : b = c) :
= -c

Evaluates `nat.succ`, `int.to_nat`, `int.nat_abs`, `int.neg_succ_of_nat`.

theorem norm_num.int_to_nat_cast (a : ) (b : ) (h : a = b) :
a = b

Evaluates the `↑n` cast operation from `ℕ`, `ℤ`, `ℚ` to an arbitrary type `α`.

meta def norm_num.derive.step (e : expr) :

This version of `derive` does not fail when the input is already a numeral

@[protected]

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.

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.

Look up the `norm_num` extensions in the cache and return a tactic extending `derive.step` with additional reduction procedures.

meta def norm_num.derive' (step : expr tactic ) :

Simplify an expression bottom-up using `step` to simplify the subexpressions.

meta def norm_num.derive (e : expr) :

Simplify an expression bottom-up using the default `norm_num` set to simplify the subexpressions.

meta def tactic.norm_num1 (step : expr tactic ) (loc : interactive.loc) :

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.

meta def expr.norm_num (step : expr tactic ) (no_dflt : bool := bool.ff) (attr_names : := list.nil) :

Carry out similar operations as `tactic.norm_num` but on an `expr` rather than a location. Given an expression `e`, returns `(e', ⊢ e = e')`. The `no_dflt`, `hs`, and `attr_names` are passed on to `simp`. Unlike `norm_num`, this tactic does not fail.

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.

Normalises numerical expressions. It supports the operations `+` `-` `*` `/` `^` and `%` over numerical types such as `ℕ`, `ℤ`, `ℚ`, `ℝ`, `ℂ`, and can prove goals of the form `A = B`, `A ≠ B`, `A < B` and `A ≤ B`, where `A` and `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 `nat` like `prime`, `min_fac` and `factors`.

``````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
``````

The variant `norm_num1` does not call `simp`.

Both `norm_num` and `norm_num1` can be called inside the `conv` tactic.

The tactic `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
```
``````

## `conv` tactic #

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.

## `#norm_num` command #

A user command to run `norm_num`. Mostly copied from the `#simp` command.

meta def tactic.norm_num_cmd (_x : interactive.parse (lean.parser.tk "#norm_num")) :

The basic usage is `#norm_num e`, where `e` is an expression, which will print the `norm_num` form of `e`.

Syntax: `#norm_num` (`only`)? (`[` simp lemma list `]`)? (`with` simp sets)? `:`? expression

This accepts the same options as the `#simp` command. 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.) The `only` restricts `norm_num` to using only the provided lemmas, and so `#norm_num only : e` behaves similarly to `norm_num1`.

Unlike `norm_num`, this command does not fail when no simplifications are made.

`#norm_num` understands local variables, so you can use them to introduce parameters.

The basic usage is `#norm_num e`, where `e` is an expression, which will print the `norm_num` form of `e`.

Syntax: `#norm_num` (`only`)? (`[` simp lemma list `]`)? (`with` simp sets)? `:`? expression

This accepts the same options as the `#simp` command. 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.) The `only` restricts `norm_num` to using only the provided lemmas, and so `#norm_num only : e` behaves similarly to `norm_num1`.

Unlike `norm_num`, this command does not fail when no simplifications are made.

`#norm_num` understands local variables, so you can use them to introduce parameters.

theorem norm_num.nat_div (a b q r m : ) (hm : q * b = m) (h : r + m = a) (h₂ : r < b) :
a / b = q
theorem norm_num.int_div (a b q r m : ) (hm : q * b = m) (h : r + m = a) (h₁ : 0 r) (h₂ : r < b) :
a / b = q
theorem norm_num.nat_mod (a b q r m : ) (hm : q * b = m) (h : r + m = a) (h₂ : r < b) :
a % b = r
theorem norm_num.int_mod (a b q r m : ) (hm : q * b = m) (h : r + m = a) (h₁ : 0 r) (h₂ : r < b) :
a % b = r
theorem norm_num.int_div_neg (a b c' c : ) (h : a / b = c') (h₂ : -c' = c) :
a / -b = c
theorem norm_num.int_mod_neg (a b c : ) (h : a % b = c) :
a % -b = c

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)`
theorem norm_num.dvd_eq_nat (a b c : ) (p : Prop) (h₁ : b % a = c) (h₂ : c = 0 = p) :
a b = p
theorem norm_num.dvd_eq_int (a b c : ) (p : Prop) (h₁ : b % a = c) (h₂ : c = 0 = p) :
a b = p

Evaluates some extra numeric operations on `nat` and `int`, specifically `/` and `%`, and `∣` (divisibility).