mathlib documentation

tactic.norm_num

norm_num

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

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

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

source
meta def tactic.trans_conv  :
(expr → tactic (expr × expr)) → (expr → tactic (expr × expr)) → 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  :
tactic.instance_cache → expr → tactic (tactic.instance_cache × expr)

Faster version of mk_app ``bit0 [e].

source
meta def tactic.instance_cache.mk_bit1  :
tactic.instance_cache → 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 : α) :
l = tl → r = tr → tl + tr = t → l + r = t

source
theorem norm_num.subst_into_mul {α : Type u_1} [has_mul α] (l r tl tr t : α) :
l = tl → r = tr → tl * tr = t → l * r = t

source
theorem norm_num.subst_into_neg {α : Type u_1} [has_neg α] (a ta t : α) :
a = ta → -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  :
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 : α) :
a + 1 = b → bit1 a + 1 = bit0 b

source
meta def norm_num.prove_succ  :
tactic.instance_cache → expr → 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 : α) :
a + 1 = b → 0 + a + 1 = b

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

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

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

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

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

source
theorem norm_num.add_bit1_bit1 {α : Type u_1} [semiring α] (a b c : α) :
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 : α) :
a + 1 = b → bit0 a + 1 + 1 = bit0 b

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

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

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

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

source
theorem norm_num.adc_bit1_bit0 {α : Type u_1} [semiring α] (a b c : α) :
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 : α) :
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 : α) :
a + b + 1 = c → bit1 a + bit1 b + 1 = bit1 c

source
meta def norm_num.prove_add_nat'  :
tactic.instance_cache → expr → 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 : α) :
a * b = c → (bit0 a) * b = bit0 c

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

source
theorem norm_num.mul_bit0_bit0 {α : Type u_1} [semiring α] (a b c : α) :
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 : α) :
a * b = c → a + b = d → bit0 c + d = e → (bit1 a) * bit1 b = bit1 e

source
meta def norm_num.prove_mul_nat  :
tactic.instance_cache → expr → 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  :
tactic.instance_cache → expr → tactic (tactic.instance_cache × expr)

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

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

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

source
meta def norm_num.match_neg  :
expr → option expr

match_neg (- e) = some e, otherwise none

source
meta def norm_num.match_sign  :
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 : α) :
0 < a → a ≠ 0

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

source
meta def norm_num.prove_ne_zero'  :
tactic.instance_cache → 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 : α) :
b ≠ 0 → b * b' = d → a * b' = c → (a / b) * d = c

source
meta def norm_num.prove_clear_denom'  :
(tactic.instance_cache → expr → ℚ → tactic (tactic.instance_cache × expr)) → tactic.instance_cache → expr → expr → ℚ → ℕ → 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.nonneg_pos {α : Type u_1} [ordered_cancel_add_comm_monoid α] (a : α) :
0 < a → 0 ≤ a

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

source
meta def norm_num.prove_lt_nat  :
tactic.instance_cache → expr → 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 : α) :
0 < d → a * d = a' → b * d = b' → a' < b' → a < b

source
meta def norm_num.prove_lt_nonneg_rat  :
tactic.instance_cache → expr → expr → ℚ → ℚ → 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 : α) :
0 < a → 0 < b → -a < b

source
meta def norm_num.prove_lt_rat  :
tactic.instance_cache → expr → expr → ℚ → ℚ → 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 : α) :
0 < d → a * d = a' → b * d = b' → a' ≤ b' → a ≤ b

source
meta def norm_num.prove_le_nonneg_rat  :
tactic.instance_cache → expr → expr → ℚ → ℚ → 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 : α) :
0 ≤ a → 0 ≤ b → -a ≤ b

source
meta def norm_num.prove_le_rat  :
tactic.instance_cache → expr → expr → ℚ → ℚ → tactic (tactic.instance_cache × expr)

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

source
meta def norm_num.prove_ne_rat  :
tactic.instance_cache → expr → expr → ℚ → ℚ → 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' : α) :
↑a = a' → ↑(bit0 a) = bit0 a'

source
theorem norm_num.nat_cast_bit1 {α : Type u_1} [semiring α] (a : ℕ) (a' : α) :
↑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' : α) :
↑a = a' → ↑(bit0 a) = bit0 a'

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

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

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

source
meta def norm_num.prove_nat_uncast  :
tactic.instance_cache → tactic.instance_cache → 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  :
tactic.instance_cache → tactic.instance_cache → 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  :
tactic.instance_cache → tactic.instance_cache → expr → 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' : α) :
↑a = a' → ↑b = b' → ↑(a / b) = a' / b'

source
meta def norm_num.prove_rat_uncast_nonneg  :
tactic.instance_cache → tactic.instance_cache → expr → expr → ℚ → 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' : α) :
↑a = a' → ↑-a = -a'

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

source
meta def norm_num.prove_int_uncast  :
tactic.instance_cache → tactic.instance_cache → 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  :
tactic.instance_cache → tactic.instance_cache → expr → expr → ℚ → 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' : α) :
↑a = a' → ↑b = b' → a ≠ b → a' ≠ b'

source
theorem norm_num.int_cast_ne {α : Type u_1} [ring α] [char_zero α] (a b : ℤ) (a' b' : α) :
↑a = a' → ↑b = b' → a ≠ b → a' ≠ b'

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

source
meta def norm_num.prove_ne  :
tactic.instance_cache → expr → expr → ℚ → ℚ → 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.prove_ne_zero  :
tactic.instance_cache → expr → ℚ → tactic (tactic.instance_cache × expr)

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

source
meta def norm_num.prove_clear_denom  :
tactic.instance_cache → expr → expr → ℚ → ℕ → 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 : α) :
d ≠ 0 → a * d = a' → b * d = b' → c * d = c' → a' + b' = c' → a + b = c

source
meta def norm_num.prove_add_nonneg_rat  :
tactic.instance_cache → expr → expr → expr → ℚ → ℚ → ℚ → 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 : α) :
c + b = a → a + -b = c

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

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

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

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

source
meta def norm_num.prove_add_rat  :
tactic.instance_cache → expr → expr → expr → ℚ → ℚ → ℚ → tactic (tactic.instance_cache × expr)

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

source
meta def norm_num.prove_add_rat'  :
tactic.instance_cache → expr → 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 : α) :
b ≠ 0 → b ≠ 0 ∧ (a / b) * b = a

source
meta def norm_num.prove_clear_denom_simple  :
tactic.instance_cache → expr → ℚ → 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 : α) :
d₁ ≠ 0 ∧ a * d₁ = a' → d₂ ≠ 0 ∧ b * d₂ = b' → c * d = c' → d₁ * d₂ = d → a' * b' = c' → a * b = c

source
meta def norm_num.prove_mul_nonneg_rat  :
tactic.instance_cache → expr → expr → ℚ → ℚ → 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 : α) :
a * b = c → (-a) * b = -c

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

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

source
meta def norm_num.prove_mul_rat  :
tactic.instance_cache → expr → expr → ℚ → ℚ → 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 : α) :
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  :
tactic.instance_cache → expr → ℚ → 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 : α) :
b⁻¹ = b' → a * b' = c → a / b = c

source
meta def norm_num.prove_div  :
tactic.instance_cache → expr → expr → ℚ → ℚ → tactic (tactic.instance_cache × expr × expr)

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

source
meta def norm_num.prove_neg  :
tactic.instance_cache → 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 : α) :
-b = b' → a + b' = c → a - b = c

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

source
meta def norm_num.prove_sub  :
tactic.instance_cache → expr → 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 : ℕ) :
b + c = a → a - b = c

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

source
meta def norm_num.prove_sub_nat  :
tactic.instance_cache → expr → 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 : ℤ) :
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  :
tactic.instance_cache → expr → expr → tactic (expr × expr)

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

source
meta def norm_num.eval_field  :
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 : ℕ) :
a ^ b = c' → c' * c' = c → a ^ bit0 b = c

source
theorem norm_num.pow_bit1 {α : Type u} [monoid α] (a c₁ c₂ c : α) (b : ℕ) :
a ^ b = c₁ → c₁ * c₁ = c₂ → c₂ * a = c → a ^ bit1 b = c

source
meta def norm_num.prove_pow  :
expr → ℚ → tactic.instance_cache → 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  :
expr → tactic (expr × expr)

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

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

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

source
meta def norm_num.false_intro  :
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  :
expr → tactic (expr × expr)

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

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

source
meta def norm_num.prove_nat_succ  :
tactic.instance_cache → 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 : ℕ) :
q * b = m → r + m = a → r < b → a / b = q

source
theorem norm_num.int_div (a b q r m : ℤ) :
q * b = m → r + m = a → 0 ≤ r → r < b → a / b = q

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

source
theorem norm_num.int_mod (a b q r m : ℤ) :
q * b = m → r + m = a → 0 ≤ r → r < b → a % b = r

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

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

source
meta def norm_num.prove_div_mod  :
tactic.instance_cache → expr → expr → 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) :
b % a = c → c = 0 = p → a ∣ b = p

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

source
meta def norm_num.eval_nat_int_ext  :
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 : ℕ) :
a * b = n → 1 < a → 1 < b → ¬nat.prime n

source
theorem norm_num.is_prime_helper (n : ℕ) :
1 < n → 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  :
ℕ → ℕ → Prop

A predicate representing partial progress in a proof of min_fac.

Equations
source
theorem norm_num.min_fac_helper.n_pos {n k : ℕ} :
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 : ℕ) :
0 < n → norm_num.min_fac_helper n 1

source
theorem norm_num.min_fac_helper_1 {n k k' : ℕ} :
k + 1 = k' → (bit1 n).min_fac ≠ bit1 k → 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' : ℕ) :
k + 1 = k' → ¬nat.prime (bit1 k) → 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 : ℕ) :
k + 1 = k' → bit1 n % bit1 k = c → 0 < c → norm_num.min_fac_helper n k → norm_num.min_fac_helper n k'

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

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

source
meta def norm_num.prove_non_prime  :
expr → ℕ → ℕ → 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  :
expr → expr → ℕ → tactic.instance_cache → expr → 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  :
tactic.instance_cache → 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  :
expr → tactic (expr × expr)

Evaluates the prime and min_fac functions.

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

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

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

source
meta def tactic.interactive.norm_num1  :
interactive.parse interactive.types.location → tactic unit

Basic version of norm_num that does not call simp.

source
meta def tactic.interactive.norm_num  :
interactive.parse tactic.simp_arg_list → 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  :
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  :
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.