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

Turns a conversion tactic into one that always succeeds, where failure is interpreted as a proof by reflexivity.

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

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

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

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