mathlib docs: tactic.norm

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

(expr → tactic (expr × expr)) → (expr → tactic (expr × expr)) → expr → tactic (expr × expr)

Transitivity conversion: given two conversions (which take an expression e and returns (e', ⊢ e = e')), produces another conversion that combines them with transitivity, treating failures as reflexivity conversions.

source

meta def tactic.instance_cache.mk_bit0 :

tactic.instance_cache → expr → tactic (tactic.instance_cache × expr)

Faster version of mk_app ``bit0 [e].

source

meta def tactic.instance_cache.mk_bit1 :

tactic.instance_cache → expr → tactic (tactic.instance_cache × expr)

Faster version of mk_app ``bit1 [e].

source

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

l = tl → r = tr → tl + tr = t → l + r = t

source

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

l = tl → r = tr → tl * tr = t → l * r = t

source

theorem norm_num.subst_into_neg {α : Type u_1} [has_neg α] (a ta t : α) :

a = ta → -ta = t → -a = t

source

meta inductive norm_num.match_numeral_result :

Type

zero : norm_num.match_numeral_result
one : norm_num.match_numeral_result
bit0 : expr → norm_num.match_numeral_result
bit1 : expr → norm_num.match_numeral_result
other : norm_num.match_numeral_result

The result type of match_numeral, either 0, 1, or a top level decomposition of bit0 e or bit1 e. The other case means it is not a numeral.

source

meta def norm_num.match_numeral :

expr → norm_num.match_numeral_result

Unfold the top level constructor of the numeral expression.

source

theorem norm_num.zero_succ {α : Type u_1} [semiring α] :

0 + 1 = 1

source

theorem norm_num.one_succ {α : Type u_1} [semiring α] :

1 + 1 = 2

source

theorem norm_num.bit0_succ {α : Type u_1} [semiring α] (a : α) :

bit0 a + 1 = bit1 a

source

theorem norm_num.bit1_succ {α : Type u_1} [semiring α] (a b : α) :

a + 1 = b → bit1 a + 1 = bit0 b

source

meta def norm_num.prove_succ :

tactic.instance_cache → expr → expr → tactic (tactic.instance_cache × expr)

Given a, b natural numerals, proves ⊢ a + 1 = b, assuming that this is provable. (It may prove garbage instead of failing if a + 1 = b is false.)

source

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

a + 1 = b → 0 + a + 1 = b

source

theorem norm_num.adc_zero {α : Type u_1} [semiring α] (a b : α) :

a + 1 = b → a + 0 + 1 = b

source

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

a + 1 = b → 1 + a = b

source

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

a + b = c → bit0 a + bit0 b = bit0 c

source

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

a + b = c → bit0 a + bit1 b = bit1 c

source

theorem norm_num.add_bit1_bit0 {α : Type u_1} [semiring α] (a b c : α) :

a + b = c → bit1 a + bit0 b = bit1 c

source

theorem norm_num.add_bit1_bit1 {α : Type u_1} [semiring α] (a b c : α) :

a + b + 1 = c → bit1 a + bit1 b = bit0 c

source

theorem norm_num.adc_one_one {α : Type u_1} [semiring α] :

1 + 1 + 1 = 3

source

theorem norm_num.adc_bit0_one {α : Type u_1} [semiring α] (a b : α) :

a + 1 = b → bit0 a + 1 + 1 = bit0 b

source

theorem norm_num.adc_one_bit0 {α : Type u_1} [semiring α] (a b : α) :

a + 1 = b → 1 + bit0 a + 1 = bit0 b

source

theorem norm_num.adc_bit1_one {α : Type u_1} [semiring α] (a b : α) :

a + 1 = b → bit1 a + 1 + 1 = bit1 b

source

theorem norm_num.adc_one_bit1 {α : Type u_1} [semiring α] (a b : α) :

a + 1 = b → 1 + bit1 a + 1 = bit1 b

source

theorem norm_num.adc_bit0_bit0 {α : Type u_1} [semiring α] (a b c : α) :

a + b = c → bit0 a + bit0 b + 1 = bit1 c

source

theorem norm_num.adc_bit1_bit0 {α : Type u_1} [semiring α] (a b c : α) :

a + b + 1 = c → bit1 a + bit0 b + 1 = bit0 c

source

theorem norm_num.adc_bit0_bit1 {α : Type u_1} [semiring α] (a b c : α) :

a + b + 1 = c → bit0 a + bit1 b + 1 = bit0 c

source

theorem norm_num.adc_bit1_bit1 {α : Type u_1} [semiring α] (a b c : α) :

a + b + 1 = c → bit1 a + bit1 b + 1 = bit1 c

source

meta def norm_num.prove_add_nat' :

tactic.instance_cache → expr → expr → tactic (tactic.instance_cache × expr × expr)

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

source

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

a * b = c → bit0 a * b = bit0 c

source

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

a * b = c → a * bit0 b = bit0 c

source

theorem norm_num.mul_bit0_bit0 {α : Type u_1} [semiring α] (a b c : α) :

a * b = c → bit0 a * bit0 b = bit0 (bit0 c)

source

theorem norm_num.mul_bit1_bit1 {α : Type u_1} [semiring α] (a b c d e : α) :

a * b = c → a + b = d → bit0 c + d = e → bit1 a * bit1 b = bit1 e

source

meta def norm_num.prove_mul_nat :

tactic.instance_cache → expr → expr → tactic (tactic.instance_cache × expr × expr)

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

source

meta def norm_num.prove_pos_nat :

tactic.instance_cache → expr → tactic (tactic.instance_cache × expr)

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

source

meta def norm_num.prove_pos :

tactic.instance_cache → expr → tactic (tactic.instance_cache × expr)

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

source

meta def norm_num.match_neg :

expr → option expr

match_neg (- e) = some e, otherwise none

source

meta def norm_num.match_sign :

expr → expr ⊕ bool

match_sign (- e) = inl e, match_sign 0 = inr ff, otherwise inr tt

source

theorem norm_num.ne_zero_of_pos {α : Type u_1} [ordered_add_comm_group α] (a : α) :

0 < a → a ≠ 0

source

theorem norm_num.ne_zero_neg {α : Type u_1} [add_group α] (a : α) :

a ≠ 0 → -a ≠ 0

source

meta def norm_num.prove_ne_zero :

tactic.instance_cache → expr → tactic (tactic.instance_cache × expr)

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

source

theorem norm_num.clear_denom_div {α : Type u_1} [division_ring α] (a b b' c d : α) :

b ≠ 0 → b * b' = d → a * b' = c → a / b * d = c

source

meta def norm_num.prove_clear_denom :

tactic.instance_cache → expr → expr → ℚ → ℕ → tactic (tactic.instance_cache × expr × expr)

Given a nonnegative rational and d a natural number, returns (b, ⊢ a * d = b). (d should be a multiple of the denominator of a, so that b is a natural number.)

source

theorem norm_num.clear_denom_add {α : Type u_1} [division_ring α] (a a' b b' c c' d : α) :

d ≠ 0 → a * d = a' → b * d = b' → c * d = c' → a' + b' = c' → a + b = c

source

meta def norm_num.prove_add_nonneg_rat :

tactic.instance_cache → expr → expr → expr → ℚ → ℚ → ℚ → tactic (tactic.instance_cache × expr)

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

source

theorem norm_num.add_pos_neg_pos {α : Type u_1} [add_group α] (a b c : α) :

c + b = a → a + -b = c

source

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

c + a = b → a + -b = -c

source

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

a + c = b → -a + b = c

source

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

b + c = a → -a + b = -c

source

theorem norm_num.add_neg_neg {α : Type u_1} [add_group α] (a b c : α) :

b + a = c → -a + -b = -c

source

meta def norm_num.prove_add_rat :

tactic.instance_cache → expr → expr → expr → ℚ → ℚ → ℚ → tactic (tactic.instance_cache × expr)

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

source

meta def norm_num.prove_add_rat' :

tactic.instance_cache → expr → expr → tactic (tactic.instance_cache × expr × expr)

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

source

theorem norm_num.clear_denom_simple_nat {α : Type u_1} [division_ring α] (a : α) :

1 ≠ 0 ∧ a * 1 = a

source

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

b ≠ 0 → b ≠ 0 ∧ a / b * b = a

source

meta def norm_num.prove_clear_denom_simple :

tactic.instance_cache → expr → ℚ → tactic (tactic.instance_cache × expr × expr × expr)

Given a a nonnegative rational numeral, returns (b, c, ⊢ a * b = c) where b and c are natural numerals. (b will be the denominator of a.)

source

theorem norm_num.clear_denom_mul {α : Type u_1} [field α] (a a' b b' c c' d₁ d₂ d : α) :

d₁ ≠ 0 ∧ a * d₁ = a' → d₂ ≠ 0 ∧ b * d₂ = b' → c * d = c' → d₁ * d₂ = d → a' * b' = c' → a * b = c

source

meta def norm_num.prove_mul_nonneg_rat :

tactic.instance_cache → expr → expr → ℚ → ℚ → tactic (tactic.instance_cache × expr × expr)

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

source

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

a * b = c → -a * b = -c

source

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

a * b = c → a * -b = -c

source

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

a * b = c → -a * -b = c

source

meta def norm_num.prove_mul_rat :

tactic.instance_cache → expr → expr → ℚ → ℚ → tactic (tactic.instance_cache × expr × expr)

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

source

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

a⁻¹ = b → (-a)⁻¹ = -b

source

theorem norm_num.inv_one {α : Type u_1} [division_ring α] :

1⁻¹ = 1

source

theorem norm_num.inv_one_div {α : Type u_1} [division_ring α] (a : α) :

(1 / a)⁻¹ = a

source

theorem norm_num.inv_div_one {α : Type u_1} [division_ring α] (a : α) :

a⁻¹ = 1 / a

source

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

(a / b)⁻¹ = b / a

source

meta def norm_num.prove_inv :

tactic.instance_cache → expr → ℚ → tactic (tactic.instance_cache × expr × expr)

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

source

theorem norm_num.div_eq {α : Type u_1} [division_ring α] (a b b' c : α) :

b⁻¹ = b' → a * b' = c → a / b = c

source

meta def norm_num.prove_div :

tactic.instance_cache → expr → expr → ℚ → ℚ → tactic (tactic.instance_cache × expr × expr)

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

source

meta def norm_num.prove_neg :

tactic.instance_cache → expr → tactic (tactic.instance_cache × expr × expr)

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

source

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

-b = b' → a + b' = c → a - b = c

source

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

a + b = c → a - -b = c

source

meta def norm_num.prove_sub :

tactic.instance_cache → expr → expr → tactic (tactic.instance_cache × expr × expr)

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

source

theorem norm_num.sub_nat_pos (a b c : ℕ) :

b + c = a → a - b = c

source

theorem norm_num.sub_nat_neg (a b c : ℕ) :

a + c = b → a - b = 0

source

meta def norm_num.prove_sub_nat :

tactic.instance_cache → expr → expr → tactic (expr × expr)

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

source

theorem norm_num.int_sub_hack (a b c : ℤ) :

a - b = c → a - b = c

This is needed because when a and b are numerals lean is more likely to unfold them than unfold the instances in order to prove that add_group_has_sub = int.has_sub.

source

meta def norm_num.prove_sub_int :

tactic.instance_cache → expr → expr → tactic (expr × expr)

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

source

meta def norm_num.eval_field :

expr → tactic (expr × expr)

Evaluates the basic field operations +,neg,-,*,inv,/ on numerals. Also handles nat subtraction. Does not do recursive simplification; that is, 1 + 1 + 1 will not simplify but 2 + 1 will. This is handled by the top level simp call in norm_num.derive.

source

theorem norm_num.pow_bit0 {α : Type u} [monoid α] (a c' c : α) (b : ℕ) :

a ^ b = c' → c' * c' = c → a ^ bit0 b = c

source

theorem norm_num.pow_bit1 {α : Type u} [monoid α] (a c₁ c₂ c : α) (b : ℕ) :

a ^ b = c₁ → c₁ * c₁ = c₂ → c₂ * a = c → a ^ bit1 b = c

source

meta def norm_num.prove_pow :

expr → ℚ → tactic.instance_cache → expr → tactic (tactic.instance_cache × expr × expr)

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

source

theorem norm_num.from_nat_pow (a b c : ℕ) :

a ^ b = c → a ^ b = c

source

meta def norm_num.eval_pow :

expr → tactic (expr × expr)

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

source

theorem norm_num.nonneg_pos {α : Type u_1} [ordered_cancel_add_comm_monoid α] (a : α) :

0 < a → 0 ≤ a

source

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

1 ≤ a → 1 < bit0 a

source

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

0 < a → 1 < bit1 a

source

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

a < b → bit0 a < bit0 b

source

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

a ≤ b → bit0 a < bit1 b

source

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

a + 1 ≤ b → bit1 a < bit0 b

source

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

a < b → bit1 a < bit1 b

source

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

1 ≤ a → 1 ≤ bit0 a

source

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

0 < a → 1 ≤ bit1 a

source

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

a ≤ b → bit0 a ≤ bit0 b

source

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

a ≤ b → bit0 a ≤ bit1 b

source

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

a + 1 ≤ b → bit1 a ≤ bit0 b

source

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

a ≤ b → bit1 a ≤ bit1 b

source

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

1 ≤ a → 1 + 1 ≤ bit0 a

source

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

1 ≤ a → 1 + 1 ≤ bit1 a

source

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

a + 1 ≤ b → bit0 a + 1 ≤ bit0 b

source

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

a ≤ b → bit0 a + 1 ≤ bit1 b

source

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

a + 1 ≤ b → bit1 a + 1 ≤ bit0 b

source

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

a + 1 ≤ b → bit1 a + 1 ≤ bit1 b

source

meta def norm_num.prove_nonneg :

tactic.instance_cache → expr → tactic (tactic.instance_cache × expr)

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

source

meta def norm_num.prove_one_le_nat :

tactic.instance_cache → expr → tactic (tactic.instance_cache × expr)

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

source

meta def norm_num.prove_lt_nat :

tactic.instance_cache → expr → expr → tactic (tactic.instance_cache × expr)

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

source

theorem norm_num.clear_denom_lt {α : Type u_1} [linear_ordered_semiring α] (a a' b b' d : α) :

0 < d → a * d = a' → b * d = b' → a' < b' → a < b

source

meta def norm_num.prove_lt_nonneg_rat :

tactic.instance_cache → expr → expr → ℚ → ℚ → tactic (tactic.instance_cache × expr)

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

source

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

0 < a → 0 < b → -a < b

source

meta def norm_num.prove_lt_rat :

tactic.instance_cache → expr → expr → ℚ → ℚ → tactic (tactic.instance_cache × expr)

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

source

theorem norm_num.clear_denom_le {α : Type u_1} [linear_ordered_semiring α] (a a' b b' d : α) :

0 < d → a * d = a' → b * d = b' → a' ≤ b' → a ≤ b

source

meta def norm_num.prove_le_nonneg_rat :

tactic.instance_cache → expr → expr → ℚ → ℚ → tactic (tactic.instance_cache × expr)

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

source

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

0 ≤ a → 0 ≤ b → -a ≤ b

source

meta def norm_num.prove_le_rat :

tactic.instance_cache → expr → expr → ℚ → ℚ → tactic (tactic.instance_cache × expr)

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

source

meta def norm_num.prove_ne_rat :

tactic.instance_cache → expr → expr → ℚ → ℚ → tactic (tactic.instance_cache × expr)

Given a,b rational numerals, proves ⊢ a ≠ b. This version tries to prove ⊢ a < b or ⊢ b < a, and so is not appropriate for types without an order relation.

source

theorem norm_num.nat_cast_zero {α : Type u_1} [semiring α] :

↑0 = 0

source

theorem norm_num.nat_cast_one {α : Type u_1} [semiring α] :

↑1 = 1

source

theorem norm_num.nat_cast_bit0 {α : Type u_1} [semiring α] (a : ℕ) (a' : α) :

↑a = a' → ↑(bit0 a) = bit0 a'

source

theorem norm_num.nat_cast_bit1 {α : Type u_1} [semiring α] (a : ℕ) (a' : α) :

↑a = a' → ↑(bit1 a) = bit1 a'

source

theorem norm_num.int_cast_zero {α : Type u_1} [ring α] :

↑0 = 0

source

theorem norm_num.int_cast_one {α : Type u_1} [ring α] :

↑1 = 1

source

theorem norm_num.int_cast_bit0 {α : Type u_1} [ring α] (a : ℤ) (a' : α) :

↑a = a' → ↑(bit0 a) = bit0 a'

source

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

↑a = a' → ↑(bit1 a) = bit1 a'

source

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

↑a = a' → ↑(bit0 a) = bit0 a'

source

theorem norm_num.rat_cast_bit1 {α : Type u_1} [division_ring α] [char_zero α] (a : ℚ) (a' : α) :

↑a = a' → ↑(bit1 a) = bit1 a'

source

meta def norm_num.prove_nat_uncast :

tactic.instance_cache → tactic.instance_cache → expr → tactic (tactic.instance_cache × tactic.instance_cache × expr × expr)

Given a' : α a natural numeral, returns (a : ℕ, ⊢ ↑a = a'). (Note that the returned value is on the left of the equality.)

source

meta def norm_num.prove_int_uncast_nat :

tactic.instance_cache → tactic.instance_cache → expr → tactic (tactic.instance_cache × tactic.instance_cache × expr × expr)

Given a' : α a natural numeral, returns (a : ℤ, ⊢ ↑a = a'). (Note that the returned value is on the left of the equality.)

source

meta def norm_num.prove_rat_uncast_nat :

tactic.instance_cache → tactic.instance_cache → expr → expr → tactic (tactic.instance_cache × tactic.instance_cache × expr × expr)

Given a' : α a natural numeral, returns (a : ℚ, ⊢ ↑a = a'). (Note that the returned value is on the left of the equality.)

source

theorem norm_num.rat_cast_div {α : Type u_1} [division_ring α] [char_zero α] (a b : ℚ) (a' b' : α) :

↑a = a' → ↑b = b' → ↑(a / b) = a' / b'

source

meta def norm_num.prove_rat_uncast_nonneg :

tactic.instance_cache → tactic.instance_cache → expr → expr → ℚ → tactic (tactic.instance_cache × tactic.instance_cache × expr × expr)

Given a' : α a nonnegative rational numeral, returns (a : ℚ, ⊢ ↑a = a'). (Note that the returned value is on the left of the equality.)

source

theorem norm_num.int_cast_neg {α : Type u_1} [ring α] (a : ℤ) (a' : α) :

↑a = a' → ↑-a = -a'

source

theorem norm_num.rat_cast_neg {α : Type u_1} [division_ring α] (a : ℚ) (a' : α) :

↑a = a' → ↑-a = -a'

source

meta def norm_num.prove_int_uncast :

tactic.instance_cache → tactic.instance_cache → expr → tactic (tactic.instance_cache × tactic.instance_cache × expr × expr)

Given a' : α an integer numeral, returns (a : ℤ, ⊢ ↑a = a'). (Note that the returned value is on the left of the equality.)

source

meta def norm_num.prove_rat_uncast :

tactic.instance_cache → tactic.instance_cache → expr → expr → ℚ → tactic (tactic.instance_cache × tactic.instance_cache × expr × expr)

Given a' : α a rational numeral, returns (a : ℚ, ⊢ ↑a = a'). (Note that the returned value is on the left of the equality.)

source

theorem norm_num.nat_cast_ne {α : Type u_1} [semiring α] [char_zero α] (a b : ℕ) (a' b' : α) :

↑a = a' → ↑b = b' → a ≠ b → a' ≠ b'

source

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

↑a = a' → ↑b = b' → a ≠ b → a' ≠ b'

source

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

↑a = a' → ↑b = b' → a ≠ b → a' ≠ b'

source

meta def norm_num.prove_ne :

tactic.instance_cache → expr → expr → ℚ → ℚ → tactic (tactic.instance_cache × expr)

Given a,b rational numerals, proves ⊢ a ≠ b. Currently it tries two methods:

Prove ⊢ a < b or ⊢ b < a, if the base type has an order
Embed ↑(a':ℚ) = a and ↑(b':ℚ) = b, and then prove a' ≠ b'. This requires that the base type be char_zero, and also that it be a division_ring so that the coercion from ℚ is well defined.

We may also add coercions to ℤ and ℕ as well in order to support char_zero rings and semirings.

source

meta def norm_num.true_intro :

expr → tactic (expr × expr)

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

source

meta def norm_num.false_intro :

expr → tactic (expr × expr)

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

source

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

a ≠ a = false

source

meta def norm_num.eval_ineq :

expr → tactic (expr × expr)

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

source

theorem norm_num.nat_succ_eq (a b c : ℕ) :

a = b → b + 1 = c → a.succ = c

source

meta def norm_num.prove_nat_succ :

tactic.instance_cache → expr → tactic (tactic.instance_cache × ℕ × expr × expr)

Evaluates the expression nat.succ ... (nat.succ n) where n is a natural numeral. (We could also just handle nat.succ n here and rely on simp to work bottom up, but we figure that towers of successors coming from e.g. induction are a common case.)

source

theorem norm_num.nat_div (a b q r m : ℕ) :

q * b = m → r + m = a → r < b → a / b = q

source

theorem norm_num.int_div (a b q r m : ℤ) :

q * b = m → r + m = a → 0 ≤ r → r < b → a / b = q

source

theorem norm_num.nat_mod (a b q r m : ℕ) :

q * b = m → r + m = a → r < b → a % b = r

source

theorem norm_num.int_mod (a b q r m : ℤ) :

q * b = m → r + m = a → 0 ≤ r → r < b → a % b = r

source

theorem norm_num.int_div_neg (a b c' c : ℤ) :

a / b = c' → -c' = c → a / -b = c

source

theorem norm_num.int_mod_neg (a b c : ℤ) :

a % b = c → a % -b = c

source

meta def norm_num.prove_div_mod :

tactic.instance_cache → expr → expr → bool → tactic (tactic.instance_cache × expr × expr)

Given a,b numerals in nat or int,

prove_div_mod ic a b ff returns (c, ⊢ a / b = c)
prove_div_mod ic a b tt returns (c, ⊢ a % b = c)

source

theorem norm_num.dvd_eq_nat (a b c : ℕ) (p : Prop) :

b % a = c → c = 0 = p → a ∣ b = p

source

theorem norm_num.dvd_eq_int (a b c : ℤ) (p : Prop) :

b % a = c → c = 0 = p → a ∣ b = p

source

meta def norm_num.eval_nat_int_ext :

expr → tactic (expr × expr)

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

source

theorem norm_num.not_prime_helper (a b n : ℕ) :

a * b = n → 1 < a → 1 < b → ¬nat.prime n

source

theorem norm_num.is_prime_helper (n : ℕ) :

1 < n → n.min_fac = n → nat.prime n

source

theorem norm_num.min_fac_bit0 (n : ℕ) :

(bit0 n).min_fac = 2

source

def norm_num.min_fac_helper :

ℕ → ℕ → Prop

A predicate representing partial progress in a proof of min_fac.

Equations

norm_num.min_fac_helper n k = (0 < k ∧ bit1 k ≤ (bit1 n).min_fac)

source

theorem norm_num.min_fac_helper.n_pos {n k : ℕ} :

norm_num.min_fac_helper n k → 0 < n

source

theorem norm_num.min_fac_ne_bit0 {n k : ℕ} :

(bit1 n).min_fac ≠ bit0 k

source

theorem norm_num.min_fac_helper_0 (n : ℕ) :

0 < n → norm_num.min_fac_helper n 1

source

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

k + 1 = k' → (bit1 n).min_fac ≠ bit1 k → norm_num.min_fac_helper n k → norm_num.min_fac_helper n k'

source

theorem norm_num.min_fac_helper_2 (n k k' : ℕ) :

k + 1 = k' → ¬nat.prime (bit1 k) → norm_num.min_fac_helper n k → norm_num.min_fac_helper n k'

source

theorem norm_num.min_fac_helper_3 (n k k' c : ℕ) :

k + 1 = k' → bit1 n % bit1 k = c → 0 < c → norm_num.min_fac_helper n k → norm_num.min_fac_helper n k'

source

theorem norm_num.min_fac_helper_4 (n k : ℕ) :

bit1 n % bit1 k = 0 → norm_num.min_fac_helper n k → (bit1 n).min_fac = bit1 k

source

theorem norm_num.min_fac_helper_5 (n k k' : ℕ) :

bit1 k * bit1 k = k' → bit1 n < k' → norm_num.min_fac_helper n k → (bit1 n).min_fac = bit1 n

source

meta def norm_num.prove_non_prime :

expr → ℕ → ℕ → tactic expr

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

source

meta def norm_num.prove_min_fac_aux :

expr → expr → ℕ → tactic.instance_cache → expr → expr → tactic (tactic.instance_cache × expr × expr)

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

source

meta def norm_num.prove_min_fac :

tactic.instance_cache → expr → tactic (tactic.instance_cache × expr × expr)

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

source

meta def norm_num.eval_prime :

expr → tactic (expr × expr)

Evaluates the prime and min_fac functions.

source

meta def norm_num.derive' :

expr → tactic (expr × expr)

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

source

meta def norm_num.derive :

expr → tactic (expr × expr)

source

meta def tactic.interactive.norm_num1 :

interactive.parse interactive.types.location → tactic unit

Basic version of norm_num that does not call simp.

source

meta def tactic.interactive.norm_num :

interactive.parse tactic.simp_arg_list → interactive.parse interactive.types.location → tactic unit

Normalize numerical expressions. Supports the operations + - * / ^ and % over numerical types such as ℕ, ℤ, ℚ, ℝ, ℂ and some general algebraic types, and can prove goals of the form A = B, A ≠ B, A < B and A ≤ B, where A and B are numerical expressions. It also has a relatively simple primality prover.

source

meta def tactic.interactive.apply_normed :

interactive.parse interactive.types.texpr → tactic unit

Normalizes a numerical expression and tries to close the goal with the result.

source

meta def conv.interactive.norm_num1 :

conv unit

Basic version of norm_num that does not call simp.

source

meta def conv.interactive.norm_num :

interactive.parse tactic.simp_arg_list → conv unit

Normalize numerical expressions. Supports the operations + - * / ^ and % over numerical types such as ℕ, ℤ, ℚ, ℝ, ℂ and some general algebraic types, and can prove goals of the form A = B, A ≠ B, A < B and A ≤ B, where A and B are numerical expressions. It also has a relatively simple primality prover.

mathlib documentation

tactic.norm_num

`norm_num`

General documentation

Additional documentation

Library

mathlib documentation

tactic.​norm_num

norm_num

General documentation

Additional documentation

Library

tactic.norm_num

`norm_num`