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  :
Type

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
meta def norm_num.prove_succ  :

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
meta def norm_num.prove_add_nat  :

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

meta def norm_num.prove_adc_nat  :

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
meta def norm_num.prove_mul_nat  :

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

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 < aa 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 < a0 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 < bbit0 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 < bbit1 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 bbit0 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 bbit1 a bit1 b
theorem norm_num.sle_one_bit0 {α : Type u_1} (a : α) :
1 a1 + 1 bit0 a
theorem norm_num.sle_one_bit1 {α : Type u_1} (a : α) :
1 a1 + 1 bit1 a
theorem norm_num.sle_bit0_bit0 {α : Type u_1} (a b : α) :
a + 1 bbit0 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).

meta def norm_num.eval_field  :

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

meta def norm_num.eval_pow  :

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
meta def norm_num.eval_ineq  :

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.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
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 some extra numeric operations on nat and int, specifically nat.succ, / and %, and (divisibility).

theorem norm_num.int_to_nat_cast (a : ) (b : ) (h : a = b) :
a = b
meta def norm_num.eval_cast  :

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 exprtactic (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 exprtactic (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.

meta def norm_num.get_step  :

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 : exprtactic ) :

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 : exprtactic ) (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.

meta def tactic.norm_num (step : exprtactic ) (hs : list tactic.simp_arg_type) (l : interactive.loc) :

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 : exprtactic ) (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.