tactic.norm_num - mathlib docs

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.

mathlib documentation

`norm_num` #

norm_num #

`norm_num` #