mathlib documentation

tactic.norm_num

norm_num #

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

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

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.

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  :
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  :
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
meta def norm_num.prove_succ' (c : tactic.instance_cache) (a : expr) :
tactic (tactic.instance_cache × expr × expr)

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

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

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

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

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

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  :
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.zero_lt_one {α : Type u} [linear_ordered_semiring α] :
0 < 1
source
meta def norm_num.prove_pos_nat (c : 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 (c : 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' (c : 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 : α) (h₀ : b ≠ 0) (h₁ : b * b' = d) (h₂ : a * b' = c) :
a / b * d = c
source
meta def norm_num.prove_clear_denom' (prove_ne_zero : tactic.instance_cache → expr → ℚ → tactic (tactic.instance_cache × expr)) (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.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 : α) (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 < 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 < 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 ≤ 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 ≤ 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 : α) (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) :
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) :
expr → tactic (tactic.instance_cache × expr)

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

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

Given a,b natural numerals, proves ⊢ a + 1 ≤ b.

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

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

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

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

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

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

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

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

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
@[nolint]
theorem norm_num.gt_intro {α : Type u_1} [has_lt α] (a b : α) (c : Prop) (h : a < b = c) :
b > a = c
source
@[nolint]
theorem norm_num.ge_intro {α : Type u_1} [has_le α] (a b : α) (c : Prop) (h : a ≤ b = c) :
b ≥ a = c
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 : ℕ) (h₁ : a = b) (h₂ : b + 1 = c) :
a.succ = c
source
meta def norm_num.prove_nat_succ (ic : 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.int_to_nat_pos (a : ℤ) (b : ℕ) (h : ↑b = a) :
a.to_nat = b
source
theorem norm_num.int_to_nat_neg (a : ℤ) (h : 0 < a) :
(-a).to_nat = 0
source
theorem norm_num.nat_abs_pos (a : ℤ) (b : ℕ) (h : ↑b = a) :
a.nat_abs = b
source
theorem norm_num.nat_abs_neg (a : ℤ) (b : ℕ) (h : ↑b = a) :
(-a).nat_abs = b
source
theorem norm_num.neg_succ_of_nat (a b : ℕ) (c : ℤ) (h₁ : a + 1 = b) (h₂ : ↑b = c) :
-[1+ a] = -c
source
meta def norm_num.eval_nat_int  :
expr → tactic (expr × expr)

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

source
theorem norm_num.int_to_nat_cast (a : ℕ) (b : ℤ) (h : ↑a = b) :
↑a = b
source
meta def norm_num.eval_cast  :
expr → tactic (expr × expr)

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

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

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

source
@[protected]
meta def norm_num.attr  :
(user_attribute (expr → tactic (expr × expr)))

An attribute for adding additional extensions to norm_num. To use this attribute, put @[norm_num] on a tactic of type expr → tactic (expr × expr); the tactic will be called on subterms by norm_num, and it is responsible for identifying that the expression is a numerical function applied to numerals, for example nat.fib 17, and should return the reduced numerical expression (which must be in norm_num-normal form: a natural or rational numeral, i.e. 37, 12 / 7 or -(2 / 3), although this can be an expression in any type), and the proof that the original expression is equal to the rewritten expression.

Failure is used to indicate that this tactic does not apply to the term. For performance reasons, it is best to detect non-applicability as soon as possible so that the next tactic can have a go, so generally it will start with a pattern match and then checking that the arguments to the term are numerals or of the appropriate form, followed by proof construction, which should not fail.

Propositions are treated like any other term. The normal form for propositions is true or false, so it should produce a proof of the form p = true or p = false. eq_true_intro can be used to help here.

source
def tactic_doc.attribute.norm_num  :
tactic_doc_entry

An attribute for adding additional extensions to norm_num. To use this attribute, put @[norm_num] on a tactic of type expr → tactic (expr × expr); the tactic will be called on subterms by norm_num, and it is responsible for identifying that the expression is a numerical function applied to numerals, for example nat.fib 17, and should return the reduced numerical expression (which must be in norm_num-normal form: a natural or rational numeral, i.e. 37, 12 / 7 or -(2 / 3), although this can be an expression in any type), and the proof that the original expression is equal to the rewritten expression.

Failure is used to indicate that this tactic does not apply to the term. For performance reasons, it is best to detect non-applicability as soon as possible so that the next tactic can have a go, so generally it will start with a pattern match and then checking that the arguments to the term are numerals or of the appropriate form, followed by proof construction, which should not fail.

Propositions are treated like any other term. The normal form for propositions is true or false, so it should produce a proof of the form p = true or p = false. eq_true_intro can be used to help here.

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

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

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

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

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

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

source
meta def tactic.norm_num1 (step : expr → tactic (expr × expr)) (loc : interactive.loc) :
tactic unit

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.

source
meta def tactic.norm_num (step : expr → tactic (expr × expr)) (hs : list tactic.simp_arg_type) (l : interactive.loc) :
tactic unit

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.

source
meta def expr.norm_num (step : expr → tactic (expr × expr)) (no_dflt : bool := bool.ff) (hs : list tactic.simp_arg_type := list.nil) (attr_names : list name := list.nil) :
expr → tactic (expr × expr)

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.

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
def tactic_doc.tactic.norm_num  :
tactic_doc_entry

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 #

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.

#norm_num command #

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

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

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.

source
def tactic_doc.command.#norm_num  :
tactic_doc_entry

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.

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) :
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) (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  :
expr → tactic (expr × expr)

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