mathlib documentation

tactic.norm_num

norm_num

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

meta def tactic.refl_conv  :

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

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

Faster version of mk_app ``bit0 [e].

Faster version of mk_app ``bit1 [e].

theorem norm_num.subst_into_add {α : Type u_1} [has_add α] (l r tl tr t : α) :
l = tlr = trtl + tr = tl + r = t

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem norm_num.adc_bit1_bit0 {α : Type u_1} [semiring α] (a b c : α) :
a + b + 1 = cbit1 a + bit0 b + 1 = bit0 c

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

theorem norm_num.adc_bit1_bit1 {α : Type u_1} [semiring α] (a b c : α) :
a + b + 1 = cbit1 a + bit1 b + 1 = bit1 c

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

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

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

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

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

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

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} [ordered_add_comm_group α] (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} [division_ring α] (a b b' c d : α) :
b 0b * b' = da * b' = c(a / b) * d = c

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} [ordered_cancel_add_comm_monoid α] (a : α) :
0 < a0 a

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

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

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

theorem norm_num.lt_bit0_bit1 {α : Type u_1} [linear_ordered_semiring α] (a b : α) :
a bbit0 a < bit1 b

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

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

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

theorem norm_num.le_one_bit1 {α : Type u_1} [linear_ordered_semiring α] (a : α) :
0 < a1 bit1 a

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

theorem norm_num.le_bit0_bit1 {α : Type u_1} [linear_ordered_semiring α] (a b : α) :
a bbit0 a bit1 b

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

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

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

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

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

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

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

theorem norm_num.sle_bit1_bit1 {α : Type u_1} [linear_ordered_semiring α] (a b : α) :
a + 1 bbit1 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 < b.

theorem norm_num.clear_denom_lt {α : Type u_1} [linear_ordered_semiring α] (a a' b b' d : α) :
0 < da * d = a'b * d = b'a' < b'a < b

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

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

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

theorem norm_num.clear_denom_le {α : Type u_1} [linear_ordered_semiring α] (a a' b b' d : α) :
0 < da * d = a'b * d = b'a' b'a b

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

theorem norm_num.le_neg_pos {α : Type u_1} [ordered_add_comm_group α] (a b : α) :
0 a0 b-a b

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

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' : α) :
a = a'(bit0 a) = bit0 a'

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

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

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

theorem norm_num.rat_cast_bit1 {α : Type u_1} [division_ring α] [char_zero α] (a : ) (a' : α) :
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.)

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} [division_ring α] [char_zero α] (a b : ) (a' b' : α) :
a = a'b = b'(a / b) = a' / b'

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' : α) :
a = a'-a = -a'

theorem norm_num.rat_cast_neg {α : Type u_1} [division_ring α] (a : ) (a' : α) :
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.)

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' : α) :
a = a'b = b'a ba' b'

theorem norm_num.int_cast_ne {α : Type u_1} [ring α] [char_zero α] (a b : ) (a' b' : α) :
a = a'b = b'a ba' b'

theorem norm_num.rat_cast_ne {α : Type u_1} [division_ring α] [char_zero α] (a b : ) (a' b' : α) :
a = a'b = b'a ba' b'

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} [division_ring α] (a a' b b' c c' d : α) :
d 0a * d = a'b * d = b'c * d = c'a' + b' = c'a + b = c

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 : α) :
c + b = aa + -b = c

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

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

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

theorem norm_num.add_neg_neg {α : Type u_1} [add_group α] (a b c : α) :
b + a = c-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} [division_ring α] (a : α) :
1 0 a * 1 = a

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

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 : α) :
d₁ 0 a * d₁ = a'd₂ 0 b * d₂ = b'c * d = c'd₁ * d₂ = da' * b' = c'a * b = c

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem norm_num.sub_nat_pos (a b c : ) :
b + c = aa - b = c

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

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

theorem norm_num.int_sub_hack (a b c : ) :
a - b = ca - 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.

Given a : ℤ, b : ℤ integral 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 : ) :
a ^ b = c'c' * c' = ca ^ bit0 b = c

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

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

meta def norm_num.eval_pow  :

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

meta def norm_num.true_intro  :

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

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

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

meta def norm_num.eval_ineq  :

Evaluates the inequality operations =,<,>,,, on numerals.

theorem norm_num.nat_succ_eq (a b c : ) :
a = bb + 1 = ca.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 : ) :
q * b = mr + m = ar < ba / b = q

theorem norm_num.int_div (a b q r m : ) :
q * b = mr + m = a0 rr < ba / b = q

theorem norm_num.nat_mod (a b q r m : ) :
q * b = mr + m = ar < ba % b = r

theorem norm_num.int_mod (a b q r m : ) :
q * b = mr + m = a0 rr < ba % b = r

theorem norm_num.int_div_neg (a b c' c : ) :
a / b = c'-c' = ca / -b = c

theorem norm_num.int_mod_neg (a b c : ) :
a % b = ca % -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) :
b % a = cc = 0 = pa b = p

theorem norm_num.dvd_eq_int (a b c : ) (p : Prop) :
b % a = cc = 0 = pa b = p

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

theorem norm_num.not_prime_helper (a b n : ) :
a * b = n1 < a1 < b¬nat.prime n

theorem norm_num.is_prime_helper (n : ) :
1 < nn.min_fac = nnat.prime n

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

def norm_num.min_fac_helper  :
→ Prop

A predicate representing partial progress in a proof of min_fac.

Equations
theorem norm_num.min_fac_helper_1 {n k k' : } :

theorem norm_num.min_fac_helper_3 (n k k' c : ) :
k + 1 = k'bit1 n % bit1 k = c0 < cnorm_num.min_fac_helper n knorm_num.min_fac_helper n k'

theorem norm_num.min_fac_helper_4 (n k : ) :

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

meta def norm_num.prove_non_prime  :
exprtactic expr

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

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

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

meta def norm_num.eval_prime  :

Evaluates the prime and min_fac functions.

meta def norm_num.derive'  :

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

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.

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.