mathlib documentation

tactic.norm_num

norm_num

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

source
meta def tactic.refl_conv (e : expr) :
tactic (expr × expr)

Reflexivity conversion: given e returns (e, ⊢ e = e)

source
meta def tactic.trans_conv (t₁ t₂ : expr → tactic (expr × expr)) (e : expr) :
tactic (expr × expr)

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.

source
meta def tactic.instance_cache.mk_bit0 (c : tactic.instance_cache) (e : expr) :
tactic (tactic.instance_cache × expr)

Faster version of mk_app ``bit0 [e].

source
meta def tactic.instance_cache.mk_bit1 (c : tactic.instance_cache) (e : expr) :
tactic (tactic.instance_cache × expr)

Faster version of mk_app ``bit1 [e].

source
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

source
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

source
theorem norm_num.subst_into_neg {α : Type u_1} [has_neg α] (a ta t : α) (pra : a = ta) (prt : -ta = t) :
-a = t

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

source
meta def norm_num.match_numeral (a : expr) :
norm_num.match_numeral_result

Unfold the top level constructor of the numeral expression.

source
theorem norm_num.zero_succ {α : Type u_1} [semiring α] :
0 + 1 = 1

source
theorem norm_num.one_succ {α : Type u_1} [semiring α] :
1 + 1 = 2

source
theorem norm_num.bit0_succ {α : Type u_1} [semiring α] (a : α) :
bit0 a + 1 = bit1 a

source
theorem norm_num.bit1_succ {α : Type u_1} [semiring α] (a b : α) (h : a + 1 = b) :
bit1 a + 1 = bit0 b

source
meta def norm_num.prove_succ (a : tactic.instance_cache) (a_1 a_2 : expr) :
tactic (tactic.instance_cache × expr)

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

source
theorem norm_num.zero_adc {α : Type u_1} [semiring α] (a b : α) (h : a + 1 = b) :
0 + a + 1 = b

source
theorem norm_num.adc_zero {α : Type u_1} [semiring α] (a b : α) (h : a + 1 = b) :
a + 0 + 1 = b

source
theorem norm_num.one_add {α : Type u_1} [semiring α] (a b : α) (h : a + 1 = b) :
1 + a = b

source
theorem norm_num.add_bit0_bit0 {α : Type u_1} [semiring α] (a b c : α) (h : a + b = c) :
bit0 a + bit0 b = bit0 c

source
theorem norm_num.add_bit0_bit1 {α : Type u_1} [semiring α] (a b c : α) (h : a + b = c) :
bit0 a + bit1 b = bit1 c

source
theorem norm_num.add_bit1_bit0 {α : Type u_1} [semiring α] (a b c : α) (h : a + b = c) :
bit1 a + bit0 b = bit1 c

source
theorem norm_num.add_bit1_bit1 {α : Type u_1} [semiring α] (a b c : α) (h : a + b + 1 = c) :
bit1 a + bit1 b = bit0 c

source
theorem norm_num.adc_one_one {α : Type u_1} [semiring α] :
1 + 1 + 1 = 3

source
theorem norm_num.adc_bit0_one {α : Type u_1} [semiring α] (a b : α) (h : a + 1 = b) :
bit0 a + 1 + 1 = bit0 b

source
theorem norm_num.adc_one_bit0 {α : Type u_1} [semiring α] (a b : α) (h : a + 1 = b) :
1 + bit0 a + 1 = bit0 b

source
theorem norm_num.adc_bit1_one {α : Type u_1} [semiring α] (a b : α) (h : a + 1 = b) :
bit1 a + 1 + 1 = bit1 b

source
theorem norm_num.adc_one_bit1 {α : Type u_1} [semiring α] (a b : α) (h : a + 1 = b) :
1 + bit1 a + 1 = bit1 b

source
theorem norm_num.adc_bit0_bit0 {α : Type u_1} [semiring α] (a b c : α) (h : a + b = c) :
bit0 a + bit0 b + 1 = bit1 c

source
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

source
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

source
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

source
meta def norm_num.prove_add_nat' (c : tactic.instance_cache) (a b : expr) :
tactic (tactic.instance_cache × expr × expr)

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

source
theorem norm_num.bit0_mul {α : Type u_1} [semiring α] (a b c : α) (h : a * b = c) :
(bit0 a) * b = bit0 c

source
theorem norm_num.mul_bit0' {α : Type u_1} [semiring α] (a b c : α) (h : a * b = c) :
a * bit0 b = bit0 c

source
theorem norm_num.mul_bit0_bit0 {α : Type u_1} [semiring α] (a b c : α) (h : a * b = c) :
(bit0 a) * bit0 b = bit0 (bit0 c)

source
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

source
meta def norm_num.prove_mul_nat (a : tactic.instance_cache) (a_1 a_2 : expr) :
tactic (tactic.instance_cache × expr × expr)

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

source
meta def norm_num.prove_pos_nat (c : tactic.instance_cache) (a : expr) :
tactic (tactic.instance_cache × expr)

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

source
meta def norm_num.prove_pos (c : tactic.instance_cache) (a : expr) :
tactic (tactic.instance_cache × expr)

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

source
meta def norm_num.match_neg (a : expr) :
option expr

match_neg (- e) = some e, otherwise none

source
meta def norm_num.match_sign (a : expr) :
expr ⊕ bool

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

source
theorem norm_num.ne_zero_of_pos {α : Type u_1} [ordered_add_comm_group α] (a : α) (a_1 : 0 < a) :
a ≠ 0

source
theorem norm_num.ne_zero_neg {α : Type u_1} [add_group α] (a : α) (a_1 : a ≠ 0) :
-a ≠ 0

source
meta def norm_num.prove_ne_zero (c : tactic.instance_cache) (a : expr) :
tactic (tactic.instance_cache × expr)

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

source
theorem norm_num.clear_denom_div {α : Type u_1} [division_ring α] (a b b' c d : α) (h₀ : b ≠ 0) (h₁ : b * b' = d) (h₂ : a * b' = c) :
(a / b) * d = c

source
meta def norm_num.prove_clear_denom (c : tactic.instance_cache) (a d : expr) (na : ℚ) (nd : ℕ) :
tactic (tactic.instance_cache × expr × expr)

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

source
theorem norm_num.clear_denom_add {α : Type u_1} [division_ring α] (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

source
meta def norm_num.prove_add_nonneg_rat (ic : tactic.instance_cache) (a b c : expr) (na nb nc : ℚ) :
tactic (tactic.instance_cache × expr)

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

source
theorem norm_num.add_pos_neg_pos {α : Type u_1} [add_group α] (a b c : α) (h : c + b = a) :
a + -b = c

source
theorem norm_num.add_pos_neg_neg {α : Type u_1} [add_group α] (a b c : α) (h : c + a = b) :
a + -b = -c

source
theorem norm_num.add_neg_pos_pos {α : Type u_1} [add_group α] (a b c : α) (h : a + c = b) :
-a + b = c

source
theorem norm_num.add_neg_pos_neg {α : Type u_1} [add_group α] (a b c : α) (h : b + c = a) :
-a + b = -c

source
theorem norm_num.add_neg_neg {α : Type u_1} [add_group α] (a b c : α) (h : b + a = c) :
-a + -b = -c

source
meta def norm_num.prove_add_rat (ic : tactic.instance_cache) (ea eb ec : expr) (a b c : ℚ) :
tactic (tactic.instance_cache × expr)

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

source
meta def norm_num.prove_add_rat' (ic : tactic.instance_cache) (a b : expr) :
tactic (tactic.instance_cache × expr × expr)

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

source
theorem norm_num.clear_denom_simple_nat {α : Type u_1} [division_ring α] (a : α) :
1 ≠ 0 ∧ a * 1 = a

source
theorem norm_num.clear_denom_simple_div {α : Type u_1} [division_ring α] (a b : α) (h : b ≠ 0) :
b ≠ 0 ∧ (a / b) * b = a

source
meta def norm_num.prove_clear_denom_simple (c : tactic.instance_cache) (a : expr) (na : ℚ) :
tactic (tactic.instance_cache × expr × expr × expr)

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

source
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

source
meta def norm_num.prove_mul_nonneg_rat (ic : tactic.instance_cache) (a b : expr) (na nb : ℚ) :
tactic (tactic.instance_cache × expr × expr)

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

source
theorem norm_num.mul_neg_pos {α : Type u_1} [ring α] (a b c : α) (h : a * b = c) :
(-a) * b = -c

source
theorem norm_num.mul_pos_neg {α : Type u_1} [ring α] (a b c : α) (h : a * b = c) :
a * -b = -c

source
theorem norm_num.mul_neg_neg {α : Type u_1} [ring α] (a b c : α) (h : a * b = c) :
(-a) * -b = c

source
meta def norm_num.prove_mul_rat (ic : tactic.instance_cache) (a b : expr) (na nb : ℚ) :
tactic (tactic.instance_cache × expr × expr)

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

source
theorem norm_num.inv_neg {α : Type u_1} [division_ring α] (a b : α) (h : a⁻¹ = b) :
(-a)⁻¹ = -b

source
theorem norm_num.inv_one {α : Type u_1} [division_ring α] :
1⁻¹ = 1

source
theorem norm_num.inv_one_div {α : Type u_1} [division_ring α] (a : α) :
(1 / a)⁻¹ = a

source
theorem norm_num.inv_div_one {α : Type u_1} [division_ring α] (a : α) :
a⁻¹ = 1 / a

source
theorem norm_num.inv_div {α : Type u_1} [division_ring α] (a b : α) :
(a / b)⁻¹ = b / a

source
meta def norm_num.prove_inv (a : tactic.instance_cache) (a_1 : expr) (a_2 : ℚ) :
tactic (tactic.instance_cache × expr × expr)

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

source
theorem norm_num.div_eq {α : Type u_1} [division_ring α] (a b b' c : α) (hb : b⁻¹ = b') (h : a * b' = c) :
a / b = c

source
meta def norm_num.prove_div (ic : tactic.instance_cache) (a b : expr) (na nb : ℚ) :
tactic (tactic.instance_cache × expr × expr)

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

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

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

source
theorem norm_num.sub_pos {α : Type u_1} [add_group α] (a b b' c : α) (hb : -b = b') (h : a + b' = c) :
a - b = c

source
theorem norm_num.sub_neg {α : Type u_1} [add_group α] (a b c : α) (h : a + b = c) :
a - -b = c

source
meta def norm_num.prove_sub (ic : tactic.instance_cache) (a b : expr) :
tactic (tactic.instance_cache × expr × expr)

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

source
theorem norm_num.sub_nat_pos (a b c : ℕ) (h : b + c = a) :
a - b = c

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

source
meta def norm_num.prove_sub_nat (ic : tactic.instance_cache) (a b : expr) :
tactic (expr × expr)

Given a : nat,b : nat natural numerals, returns (c, ⊢ a - b = c).

source
theorem norm_num.int_sub_hack (a b c : ℤ) (h : a - b = c) :
a - b = c

This is needed because when a and b are numerals lean is more likely to unfold them than unfold the instances in order to prove that add_group_has_sub = int.has_sub.

source
meta def norm_num.prove_sub_int (ic : tactic.instance_cache) (a b : expr) :
tactic (expr × expr)

Given a : ℤ, b : ℤ integral numerals, returns (c, ⊢ a - b = c).

source
meta def norm_num.eval_field (a : expr) :
tactic (expr × expr)

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.

source
theorem norm_num.pow_bit0 {α : Type u} [monoid α] (a c' c : α) (b : ℕ) (h : a ^ b = c') (h₂ : c' * c' = c) :
a ^ bit0 b = c

source
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

source
meta def norm_num.prove_pow (a : expr) (na : ℚ) (a_1 : tactic.instance_cache) (a_2 : expr) :
tactic (tactic.instance_cache × expr × expr)

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

source
meta def norm_num.eval_pow (a : expr) :
tactic (expr × expr)

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

source
theorem norm_num.nonneg_pos {α : Type u_1} [ordered_cancel_add_comm_monoid α] (a : α) (a_1 : 0 < a) :
0 ≤ a

source
theorem norm_num.lt_one_bit0 {α : Type u_1} [linear_ordered_semiring α] (a : α) (h : 1 ≤ a) :
1 < bit0 a

source
theorem norm_num.lt_one_bit1 {α : Type u_1} [linear_ordered_semiring α] (a : α) (h : 0 < a) :
1 < bit1 a

source
theorem norm_num.lt_bit0_bit0 {α : Type u_1} [linear_ordered_semiring α] (a b : α) (a_1 : a < b) :
bit0 a < bit0 b

source
theorem norm_num.lt_bit0_bit1 {α : Type u_1} [linear_ordered_semiring α] (a b : α) (h : a ≤ b) :
bit0 a < bit1 b

source
theorem norm_num.lt_bit1_bit0 {α : Type u_1} [linear_ordered_semiring α] (a b : α) (h : a + 1 ≤ b) :
bit1 a < bit0 b

source
theorem norm_num.lt_bit1_bit1 {α : Type u_1} [linear_ordered_semiring α] (a b : α) (a_1 : a < b) :
bit1 a < bit1 b

source
theorem norm_num.le_one_bit0 {α : Type u_1} [linear_ordered_semiring α] (a : α) (h : 1 ≤ a) :
1 ≤ bit0 a

source
theorem norm_num.le_one_bit1 {α : Type u_1} [linear_ordered_semiring α] (a : α) (h : 0 < a) :
1 ≤ bit1 a

source
theorem norm_num.le_bit0_bit0 {α : Type u_1} [linear_ordered_semiring α] (a b : α) (a_1 : a ≤ b) :
bit0 a ≤ bit0 b

source
theorem norm_num.le_bit0_bit1 {α : Type u_1} [linear_ordered_semiring α] (a b : α) (h : a ≤ b) :
bit0 a ≤ bit1 b

source
theorem norm_num.le_bit1_bit0 {α : Type u_1} [linear_ordered_semiring α] (a b : α) (h : a + 1 ≤ b) :
bit1 a ≤ bit0 b

source
theorem norm_num.le_bit1_bit1 {α : Type u_1} [linear_ordered_semiring α] (a b : α) (a_1 : a ≤ b) :
bit1 a ≤ bit1 b

source
theorem norm_num.sle_one_bit0 {α : Type u_1} [linear_ordered_semiring α] (a : α) (a_1 : 1 ≤ a) :
1 + 1 ≤ bit0 a

source
theorem norm_num.sle_one_bit1 {α : Type u_1} [linear_ordered_semiring α] (a : α) (a_1 : 1 ≤ a) :
1 + 1 ≤ bit1 a

source
theorem norm_num.sle_bit0_bit0 {α : Type u_1} [linear_ordered_semiring α] (a b : α) (a_1 : a + 1 ≤ b) :
bit0 a + 1 ≤ bit0 b

source
theorem norm_num.sle_bit0_bit1 {α : Type u_1} [linear_ordered_semiring α] (a b : α) (h : a ≤ b) :
bit0 a + 1 ≤ bit1 b

source
theorem norm_num.sle_bit1_bit0 {α : Type u_1} [linear_ordered_semiring α] (a b : α) (h : a + 1 ≤ b) :
bit1 a + 1 ≤ bit0 b

source
theorem norm_num.sle_bit1_bit1 {α : Type u_1} [linear_ordered_semiring α] (a b : α) (h : a + 1 ≤ b) :
bit1 a + 1 ≤ bit1 b

source
meta def norm_num.prove_nonneg (ic : tactic.instance_cache) (a : expr) :
tactic (tactic.instance_cache × expr)

Given a a rational numeral, returns ⊢ 0 ≤ a.

source
meta def norm_num.prove_one_le_nat (ic : tactic.instance_cache) (a : expr) :
tactic (tactic.instance_cache × expr)

Given a a rational numeral, returns ⊢ 1 ≤ a.

source
meta def norm_num.prove_lt_nat (ic : tactic.instance_cache) (a a_1 : expr) :
tactic (tactic.instance_cache × expr)

Given a,b natural numerals, proves ⊢ a < b.

source
theorem norm_num.clear_denom_lt {α : Type u_1} [linear_ordered_semiring α] (a a' b b' d : α) (h₀ : 0 < d) (ha : a * d = a') (hb : b * d = b') (h : a' < b') :
a < b

source
meta def norm_num.prove_lt_nonneg_rat (ic : tactic.instance_cache) (a b : expr) (na nb : ℚ) :
tactic (tactic.instance_cache × expr)

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

source
theorem norm_num.lt_neg_pos {α : Type u_1} [ordered_add_comm_group α] (a b : α) (ha : 0 < a) (hb : 0 < b) :
-a < b

source
meta def norm_num.prove_lt_rat (ic : tactic.instance_cache) (a b : expr) (na nb : ℚ) :
tactic (tactic.instance_cache × expr)

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

source
theorem norm_num.clear_denom_le {α : Type u_1} [linear_ordered_semiring α] (a a' b b' d : α) (h₀ : 0 < d) (ha : a * d = a') (hb : b * d = b') (h : a' ≤ b') :
a ≤ b

source
meta def norm_num.prove_le_nonneg_rat (ic : tactic.instance_cache) (a b : expr) (na nb : ℚ) :
tactic (tactic.instance_cache × expr)

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

source
theorem norm_num.le_neg_pos {α : Type u_1} [ordered_add_comm_group α] (a b : α) (ha : 0 ≤ a) (hb : 0 ≤ b) :
-a ≤ b

source
meta def norm_num.prove_le_rat (ic : tactic.instance_cache) (a b : expr) (na nb : ℚ) :
tactic (tactic.instance_cache × expr)

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

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

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.

source
theorem norm_num.nat_cast_zero {α : Type u_1} [semiring α] :
↑0 = 0

source
theorem norm_num.nat_cast_one {α : Type u_1} [semiring α] :
↑1 = 1

source
theorem norm_num.nat_cast_bit0 {α : Type u_1} [semiring α] (a : ℕ) (a' : α) (h : ↑a = a') :
↑(bit0 a) = bit0 a'

source
theorem norm_num.nat_cast_bit1 {α : Type u_1} [semiring α] (a : ℕ) (a' : α) (h : ↑a = a') :
↑(bit1 a) = bit1 a'

source
theorem norm_num.int_cast_zero {α : Type u_1} [ring α] :
↑0 = 0

source
theorem norm_num.int_cast_one {α : Type u_1} [ring α] :
↑1 = 1

source
theorem norm_num.int_cast_bit0 {α : Type u_1} [ring α] (a : ℤ) (a' : α) (h : ↑a = a') :
↑(bit0 a) = bit0 a'

source
theorem norm_num.int_cast_bit1 {α : Type u_1} [ring α] (a : ℤ) (a' : α) (h : ↑a = a') :
↑(bit1 a) = bit1 a'

source
theorem norm_num.rat_cast_bit0 {α : Type u_1} [division_ring α] [char_zero α] (a : ℚ) (a' : α) (h : ↑a = a') :
↑(bit0 a) = bit0 a'

source
theorem norm_num.rat_cast_bit1 {α : Type u_1} [division_ring α] [char_zero α] (a : ℚ) (a' : α) (h : ↑a = a') :
↑(bit1 a) = bit1 a'

source
meta def norm_num.prove_nat_uncast (ic nc : tactic.instance_cache) (a' : expr) :
tactic (tactic.instance_cache × tactic.instance_cache × expr × expr)

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

source
meta def norm_num.prove_int_uncast_nat (ic zc : tactic.instance_cache) (a' : expr) :
tactic (tactic.instance_cache × tactic.instance_cache × expr × expr)

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

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

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

source
theorem norm_num.rat_cast_div {α : Type u_1} [division_ring α] [char_zero α] (a b : ℚ) (a' b' : α) (ha : ↑a = a') (hb : ↑b = b') :
↑(a / b) = a' / b'

source
meta def norm_num.prove_rat_uncast_nonneg (ic qc : tactic.instance_cache) (cz_inst a' : expr) (na' : ℚ) :
tactic (tactic.instance_cache × tactic.instance_cache × expr × expr)

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

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

source
theorem norm_num.rat_cast_neg {α : Type u_1} [division_ring α] (a : ℚ) (a' : α) (h : ↑a = a') :
↑-a = -a'

source
meta def norm_num.prove_int_uncast (ic zc : tactic.instance_cache) (a' : expr) :
tactic (tactic.instance_cache × tactic.instance_cache × expr × expr)

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

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

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

source
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'

source
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'

source
theorem norm_num.rat_cast_ne {α : Type u_1} [division_ring α] [char_zero α] (a b : ℚ) (a' b' : α) (ha : ↑a = a') (hb : ↑b = b') (h : a ≠ b) :
a' ≠ b'

source
meta def norm_num.prove_ne (a : tactic.instance_cache) (a_1 a_2 : expr) (a_3 a_4 : ℚ) :
tactic (tactic.instance_cache × expr)

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.

source
meta def norm_num.true_intro (p : expr) :
tactic (expr × expr)

Given ∣- p, returns (true, ⊢ p = true).

source
meta def norm_num.false_intro (p : expr) :
tactic (expr × expr)

Given ∣- ¬ p, returns (false, ⊢ p = false).

source
theorem norm_num.not_refl_false_intro {α : Sort u_1} (a : α) :
a ≠ a = false

source
meta def norm_num.eval_ineq (a : expr) :
tactic (expr × expr)

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

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

source
meta def norm_num.prove_nat_succ (ic : tactic.instance_cache) (a : expr) :
tactic (tactic.instance_cache × ℕ × expr × expr)

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

source
theorem norm_num.nat_div (a b q r m : ℕ) (hm : q * b = m) (h : r + m = a) (h₂ : r < b) :
a / b = q

source
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

source
theorem norm_num.nat_mod (a b q r m : ℕ) (hm : q * b = m) (h : r + m = a) (h₂ : r < b) :
a % b = r

source
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

source
theorem norm_num.int_div_neg (a b c' c : ℤ) (h : a / b = c') (h₂ : -c' = c) :
a / -b = c

source
theorem norm_num.int_mod_neg (a b c : ℤ) (h : a % b = c) :
a % -b = c

source
meta def norm_num.prove_div_mod (ic : tactic.instance_cache) (a a_1 : expr) (a_2 : bool) :
tactic (tactic.instance_cache × expr × expr)

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

source
theorem norm_num.dvd_eq_int (a b c : ℤ) (p : Prop) (h₁ : b % a = c) (h₂ : c = 0 = p) :
a ∣ b = p

source
meta def norm_num.eval_nat_int_ext (a : expr) :
tactic (expr × expr)

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

source
theorem norm_num.not_prime_helper (a b n : ℕ) (h : a * b = n) (h₁ : 1 < a) (h₂ : 1 < b) :
¬nat.prime n

source
theorem norm_num.is_prime_helper (n : ℕ) (h₁ : 1 < n) (h₂ : n.min_fac = n) :
nat.prime n

source
theorem norm_num.min_fac_bit0 (n : ℕ) :
(bit0 n).min_fac = 2

source
def norm_num.min_fac_helper (n k : ℕ) :
Prop

A predicate representing partial progress in a proof of min_fac.

Equations
source
theorem norm_num.min_fac_helper.n_pos {n k : ℕ} (h : norm_num.min_fac_helper n k) :
0 < n

source
theorem norm_num.min_fac_ne_bit0 {n k : ℕ} :
(bit1 n).min_fac ≠ bit0 k

source
theorem norm_num.min_fac_helper_0 (n : ℕ) (h : 0 < n) :
norm_num.min_fac_helper n 1

source
theorem norm_num.min_fac_helper_1 {n k k' : ℕ} (e : k + 1 = k') (np : (bit1 n).min_fac ≠ bit1 k) (h : norm_num.min_fac_helper n k) :
norm_num.min_fac_helper n k'

source
theorem norm_num.min_fac_helper_2 (n k k' : ℕ) (e : k + 1 = k') (np : ¬nat.prime (bit1 k)) (h : norm_num.min_fac_helper n k) :
norm_num.min_fac_helper n k'

source
theorem norm_num.min_fac_helper_3 (n k k' c : ℕ) (e : k + 1 = k') (nc : bit1 n % bit1 k = c) (c0 : 0 < c) (h : norm_num.min_fac_helper n k) :
norm_num.min_fac_helper n k'

source
theorem norm_num.min_fac_helper_4 (n k : ℕ) (hd : bit1 n % bit1 k = 0) (h : norm_num.min_fac_helper n k) :
(bit1 n).min_fac = bit1 k

source
theorem norm_num.min_fac_helper_5 (n k k' : ℕ) (e : (bit1 k) * bit1 k = k') (hd : bit1 n < k') (h : norm_num.min_fac_helper n k) :
(bit1 n).min_fac = bit1 n

source
meta def norm_num.prove_non_prime (e : expr) (n d₁ : ℕ) :
tactic expr

Given e a natural numeral and d : nat a factor of it, return ⊢ ¬ prime e.

source
meta def norm_num.prove_min_fac_aux (a a1 : expr) (n1 : ℕ) (a_1 : tactic.instance_cache) (a_2 a_3 : expr) :
tactic (tactic.instance_cache × expr × expr)

Given a,a1 := bit1 a, n1 the value of a1, b and p : min_fac_helper a b, returns (c, ⊢ min_fac a1 = c).

source
meta def norm_num.prove_min_fac (ic : tactic.instance_cache) (e : expr) :
tactic (tactic.instance_cache × expr × expr)

Given a a natural numeral, returns (b, ⊢ min_fac a = b).

source
meta def norm_num.eval_prime (a : expr) :
tactic (expr × expr)

Evaluates the prime and min_fac functions.

source
meta def norm_num.derive' (e : expr) :
tactic (expr × expr)

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

source
meta def norm_num.derive (a : expr) :
tactic (expr × expr)

source
meta def tactic.interactive.norm_num1 (loc : interactive.parse interactive.types.location) :
tactic unit

Basic version of norm_num that does not call simp.

source
meta def tactic.interactive.norm_num (hs : interactive.parse tactic.simp_arg_list) (l : interactive.parse interactive.types.location) :
tactic unit

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.

source
meta def tactic.interactive.apply_normed (x : interactive.parse interactive.types.texpr) :
tactic unit

Normalizes a numerical expression and tries to close the goal with the result.

source
meta def conv.interactive.norm_num1  :
conv unit

Basic version of norm_num that does not call simp.

source
meta def conv.interactive.norm_num (hs : interactive.parse tactic.simp_arg_list) :
conv unit

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.