mathlib3 documentation

data.num.lemmas

Properties of the binary representation of integers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

@[simp, norm_cast]
theorem pos_num.cast_one {α : Type u_1} [has_one α] [has_add α] :
1 = 1
@[simp]
theorem pos_num.cast_one' {α : Type u_1} [has_one α] [has_add α] :
@[simp, norm_cast]
theorem pos_num.cast_bit0 {α : Type u_1} [has_one α] [has_add α] (n : pos_num) :
@[simp, norm_cast]
theorem pos_num.cast_bit1 {α : Type u_1} [has_one α] [has_add α] (n : pos_num) :
@[simp, norm_cast]
theorem pos_num.cast_to_nat {α : Type u_1} [add_monoid_with_one α] (n : pos_num) :
@[simp, norm_cast]
@[simp, norm_cast]
theorem pos_num.cast_to_int {α : Type u_1} [add_group_with_one α] (n : pos_num) :
theorem pos_num.succ_to_nat (n : pos_num) :
(n.succ) = n + 1
theorem pos_num.one_add (n : pos_num) :
1 + n = n.succ
theorem pos_num.add_one (n : pos_num) :
n + 1 = n.succ
@[norm_cast]
theorem pos_num.add_to_nat (m n : pos_num) :
(m + n) = m + n
theorem pos_num.add_succ (m n : pos_num) :
m + n.succ = (m + n).succ
theorem pos_num.bit0_of_bit0 (n : pos_num) :
bit0 n = n.bit0
theorem pos_num.bit1_of_bit1 (n : pos_num) :
bit1 n = n.bit1
@[norm_cast]
theorem pos_num.mul_to_nat (m n : pos_num) :
(m * n) = m * n
theorem pos_num.to_nat_pos (n : pos_num) :
0 < n
theorem pos_num.cmp_swap (m n : pos_num) :
(m.cmp n).swap = n.cmp m
theorem pos_num.cmp_to_nat (m n : pos_num) :
(m.cmp n).cases_on (m < n) (m = n) (n < m)
@[norm_cast]
theorem pos_num.lt_to_nat {m n : pos_num} :
m < n m < n
@[norm_cast]
theorem pos_num.le_to_nat {m n : pos_num} :
m n m n
theorem num.add_zero (n : num) :
n + 0 = n
theorem num.zero_add (n : num) :
0 + n = n
theorem num.add_one (n : num) :
n + 1 = n.succ
theorem num.add_succ (m n : num) :
m + n.succ = (m + n).succ
theorem num.bit0_of_bit0 (n : num) :
bit0 n = n.bit0
theorem num.bit1_of_bit1 (n : num) :
bit1 n = n.bit1
@[simp]
theorem num.of_nat'_zero  :
@[simp]
theorem num.of_nat'_one  :
theorem num.bit1_succ (n : num) :
theorem num.of_nat'_succ {n : } :
@[simp]
theorem num.add_of_nat' (m n : ) :
@[simp, norm_cast]
theorem num.cast_zero {α : Type u_1} [has_zero α] [has_one α] [has_add α] :
0 = 0
@[simp]
theorem num.cast_zero' {α : Type u_1} [has_zero α] [has_one α] [has_add α] :
@[simp, norm_cast]
theorem num.cast_one {α : Type u_1} [has_zero α] [has_one α] [has_add α] :
1 = 1
@[simp]
theorem num.cast_pos {α : Type u_1} [has_zero α] [has_one α] [has_add α] (n : pos_num) :
theorem num.succ'_to_nat (n : num) :
(n.succ') = n + 1
theorem num.succ_to_nat (n : num) :
(n.succ) = n + 1
@[simp, norm_cast]
theorem num.cast_to_nat {α : Type u_1} [add_monoid_with_one α] (n : num) :
@[norm_cast]
theorem num.add_to_nat (m n : num) :
(m + n) = m + n
@[norm_cast]
theorem num.mul_to_nat (m n : num) :
(m * n) = m * n
theorem num.cmp_to_nat (m n : num) :
(m.cmp n).cases_on (m < n) (m = n) (n < m)
@[norm_cast]
theorem num.lt_to_nat {m n : num} :
m < n m < n
@[norm_cast]
theorem num.le_to_nat {m n : num} :
m n m n
@[simp]
@[simp, norm_cast]
theorem num.of_to_nat' (n : num) :
@[norm_cast]
theorem num.to_nat_inj {m n : num} :
m = n m = n
meta def num.transfer_rw  :

This tactic tries to turn an (in)equality about nums to one about nats by rewriting.

example (n : num) (m : num) : n  n + m :=
begin
  num.transfer_rw,
  exact nat.le_add_right _ _
end
meta def num.transfer  :

This tactic tries to prove (in)equalities about nums by transfering them to the nat world and then trying to call simp.

example (n : num) (m : num) : n  n + m := by num.transfer
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp, norm_cast]
theorem num.add_of_nat (m n : ) :
(m + n) = m + n
@[simp, norm_cast]
theorem num.to_nat_to_int (n : num) :
@[simp, norm_cast]
theorem num.cast_to_int {α : Type u_1} [add_group_with_one α] (n : num) :
theorem num.to_of_nat (n : ) :
@[simp, norm_cast]
theorem num.of_nat_cast {α : Type u_1} [add_monoid_with_one α] (n : ) :
@[simp, norm_cast]
theorem num.of_nat_inj {m n : } :
m = n m = n
@[simp, norm_cast]
theorem num.of_to_nat (n : num) :
@[norm_cast]
theorem num.dvd_to_nat (m n : num) :
m n m n
@[simp, norm_cast]
theorem pos_num.of_to_nat (n : pos_num) :
@[norm_cast]
theorem pos_num.to_nat_inj {m n : pos_num} :
m = n m = n
@[simp]
theorem pos_num.pred'_succ' (n : num) :
@[simp]
theorem pos_num.succ'_pred' (n : pos_num) :
@[protected, instance]
Equations
@[norm_cast]
theorem pos_num.dvd_to_nat {m n : pos_num} :
m n m n

This tactic tries to turn an (in)equality about pos_nums to one about nats by rewriting.

example (n : pos_num) (m : pos_num) : n  n + m :=
begin
  pos_num.transfer_rw,
  exact nat.le_add_right _ _
end

This tactic tries to prove (in)equalities about pos_nums by transferring them to the nat world and then trying to call simp.

example (n : pos_num) (m : pos_num) : n  n + m := by pos_num.transfer
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem pos_num.cast_to_num (n : pos_num) :
@[simp, norm_cast]
theorem pos_num.bit_to_nat (b : bool) (n : pos_num) :
@[simp, norm_cast]
theorem pos_num.cast_add {α : Type u_1} [add_monoid_with_one α] (m n : pos_num) :
(m + n) = m + n
@[simp, norm_cast]
theorem pos_num.cast_succ {α : Type u_1} [add_monoid_with_one α] (n : pos_num) :
(n.succ) = n + 1
@[simp, norm_cast]
theorem pos_num.cast_inj {α : Type u_1} [add_monoid_with_one α] [char_zero α] {m n : pos_num} :
m = n m = n
@[simp]
theorem pos_num.one_le_cast {α : Type u_1} [linear_ordered_semiring α] (n : pos_num) :
1 n
@[simp]
theorem pos_num.cast_pos {α : Type u_1} [linear_ordered_semiring α] (n : pos_num) :
0 < n
@[simp, norm_cast]
theorem pos_num.cast_mul {α : Type u_1} [semiring α] (m n : pos_num) :
(m * n) = m * n
@[simp]
theorem pos_num.cmp_eq (m n : pos_num) :
@[simp, norm_cast]
theorem pos_num.cast_lt {α : Type u_1} [linear_ordered_semiring α] {m n : pos_num} :
m < n m < n
@[simp, norm_cast]
theorem pos_num.cast_le {α : Type u_1} [linear_ordered_semiring α] {m n : pos_num} :
m n m n
theorem num.bit_to_nat (b : bool) (n : num) :
theorem num.cast_succ' {α : Type u_1} [add_monoid_with_one α] (n : num) :
(n.succ') = n + 1
theorem num.cast_succ {α : Type u_1} [add_monoid_with_one α] (n : num) :
(n.succ) = n + 1
@[simp, norm_cast]
theorem num.cast_add {α : Type u_1} [semiring α] (m n : num) :
(m + n) = m + n
@[simp, norm_cast]
theorem num.cast_bit0 {α : Type u_1} [semiring α] (n : num) :
@[simp, norm_cast]
theorem num.cast_bit1 {α : Type u_1} [semiring α] (n : num) :
@[simp, norm_cast]
theorem num.cast_mul {α : Type u_1} [semiring α] (m n : num) :
(m * n) = m * n
theorem num.size_to_nat (n : num) :
theorem num.size_eq_nat_size (n : num) :
@[simp]
theorem num.of_nat'_eq (n : ) :
theorem num.to_znum_inj {m n : num} :
@[simp, norm_cast]
theorem num.cast_to_znum {α : Type u_1} [has_zero α] [has_one α] [has_add α] [has_neg α] (n : num) :
@[simp]
theorem num.cast_to_znum_neg {α : Type u_1} [add_group α] [has_one α] (n : num) :
@[simp]
theorem num.add_to_znum (m n : num) :
theorem pos_num.pred_to_nat {n : pos_num} (h : 1 < n) :
theorem pos_num.sub'_one (a : pos_num) :
theorem pos_num.lt_iff_cmp {m n : pos_num} :
theorem pos_num.le_iff_cmp {m n : pos_num} :
theorem num.pred_to_nat (n : num) :
theorem num.ppred_to_nat (n : num) :
theorem num.cmp_swap (m n : num) :
(m.cmp n).swap = n.cmp m
theorem num.cmp_eq (m n : num) :
@[simp, norm_cast]
theorem num.cast_lt {α : Type u_1} [linear_ordered_semiring α] {m n : num} :
m < n m < n
@[simp, norm_cast]
theorem num.cast_le {α : Type u_1} [linear_ordered_semiring α] {m n : num} :
m n m n
@[simp, norm_cast]
theorem num.cast_inj {α : Type u_1} [linear_ordered_semiring α] {m n : num} :
m = n m = n
theorem num.lt_iff_cmp {m n : num} :
theorem num.le_iff_cmp {m n : num} :
theorem num.bitwise_to_nat {f : num num num} {g : bool bool bool} (p : pos_num pos_num num) (gff : g bool.ff bool.ff = bool.ff) (f00 : f 0 0 = 0) (f0n : (n : pos_num), f 0 (num.pos n) = cond (g bool.ff bool.tt) (num.pos n) 0) (fn0 : (n : pos_num), f (num.pos n) 0 = cond (g bool.tt bool.ff) (num.pos n) 0) (fnn : (m n : pos_num), f (num.pos m) (num.pos n) = p m n) (p11 : p 1 1 = cond (g bool.tt bool.tt) 1 0) (p1b : (b : bool) (n : pos_num), p 1 (pos_num.bit b n) = num.bit (g bool.tt b) (cond (g bool.ff bool.tt) (num.pos n) 0)) (pb1 : (a : bool) (m : pos_num), p (pos_num.bit a m) 1 = num.bit (g a bool.tt) (cond (g bool.tt bool.ff) (num.pos m) 0)) (pbb : (a b : bool) (m n : pos_num), p (pos_num.bit a m) (pos_num.bit b n) = num.bit (g a b) (p m n)) (m n : num) :
(f m n) = nat.bitwise g m n
@[simp, norm_cast]
theorem num.lor_to_nat (m n : num) :
(m.lor n) = m.lor n
@[simp, norm_cast]
theorem num.land_to_nat (m n : num) :
(m.land n) = m.land n
@[simp, norm_cast]
theorem num.ldiff_to_nat (m n : num) :
@[simp, norm_cast]
theorem num.lxor_to_nat (m n : num) :
(m.lxor n) = m.lxor n
@[simp, norm_cast]
theorem num.shiftl_to_nat (m : num) (n : ) :
@[simp, norm_cast]
theorem num.shiftr_to_nat (m : num) (n : ) :
@[simp]
theorem num.test_bit_to_nat (m : num) (n : ) :
@[simp, norm_cast]
theorem znum.cast_zero {α : Type u_1} [has_zero α] [has_one α] [has_add α] [has_neg α] :
0 = 0
@[simp]
theorem znum.cast_zero' {α : Type u_1} [has_zero α] [has_one α] [has_add α] [has_neg α] :
@[simp, norm_cast]
theorem znum.cast_one {α : Type u_1} [has_zero α] [has_one α] [has_add α] [has_neg α] :
1 = 1
@[simp]
theorem znum.cast_pos {α : Type u_1} [has_zero α] [has_one α] [has_add α] [has_neg α] (n : pos_num) :
@[simp]
theorem znum.cast_neg {α : Type u_1} [has_zero α] [has_one α] [has_add α] [has_neg α] (n : pos_num) :
@[simp, norm_cast]
theorem znum.cast_zneg {α : Type u_1} [add_group α] [has_one α] (n : znum) :
theorem znum.neg_zero  :
-0 = 0
theorem znum.zneg_zneg (n : znum) :
--n = n
theorem znum.zneg_bit1 (n : znum) :
-n.bit1 = (-n).bitm1
theorem znum.zneg_bitm1 (n : znum) :
-n.bitm1 = (-n).bit1
theorem znum.zneg_succ (n : znum) :
-n.succ = (-n).pred
theorem znum.zneg_pred (n : znum) :
-n.pred = (-n).succ
@[simp]
theorem znum.abs_to_nat (n : znum) :
@[simp]
theorem znum.abs_to_znum (n : num) :
@[simp, norm_cast]
theorem znum.cast_to_int {α : Type u_1} [add_group_with_one α] (n : znum) :
theorem znum.bit0_of_bit0 (n : znum) :
bit0 n = n.bit0
theorem znum.bit1_of_bit1 (n : znum) :
bit1 n = n.bit1
@[simp, norm_cast]
theorem znum.cast_bit0 {α : Type u_1} [add_group_with_one α] (n : znum) :
@[simp, norm_cast]
theorem znum.cast_bit1 {α : Type u_1} [add_group_with_one α] (n : znum) :
@[simp]
theorem znum.cast_bitm1 {α : Type u_1} [add_group_with_one α] (n : znum) :
theorem znum.add_zero (n : znum) :
n + 0 = n
theorem znum.zero_add (n : znum) :
0 + n = n
theorem znum.add_one (n : znum) :
n + 1 = n.succ
theorem pos_num.cast_sub' {α : Type u_1} [add_group_with_one α] (m n : pos_num) :
(m.sub' n) = m - n
@[simp]
theorem num.cast_sub' {α : Type u_1} [add_group_with_one α] (m n : num) :
(m.sub' n) = m - n
@[simp]
theorem num.pred_succ (n : znum) :
n.pred.succ = n
theorem num.succ_of_int' (n : ) :
theorem num.mem_of_znum' {m : num} {n : znum} :
@[simp]
@[simp]
theorem num.cast_of_znum {α : Type u_1} [add_group_with_one α] (n : znum) :
@[simp, norm_cast]
theorem num.sub_to_nat (m n : num) :
(m - n) = m - n
@[simp, norm_cast]
theorem znum.cast_add {α : Type u_1} [add_group_with_one α] (m n : znum) :
(m + n) = m + n
@[simp]
theorem znum.cast_succ {α : Type u_1} [add_group_with_one α] (n : znum) :
(n.succ) = n + 1
@[simp, norm_cast]
theorem znum.mul_to_int (m n : znum) :
(m * n) = m * n
theorem znum.cast_mul {α : Type u_1} [ring α] (m n : znum) :
(m * n) = m * n
theorem znum.to_int_inj {m n : znum} :
m = n m = n
theorem znum.cmp_to_int (m n : znum) :
(m.cmp n).cases_on (m < n) (m = n) (n < m)
@[norm_cast]
theorem znum.lt_to_int {m n : znum} :
m < n m < n
theorem znum.le_to_int {m n : znum} :
m n m n
@[simp, norm_cast]
theorem znum.cast_lt {α : Type u_1} [linear_ordered_ring α] {m n : znum} :
m < n m < n
@[simp, norm_cast]
theorem znum.cast_le {α : Type u_1} [linear_ordered_ring α] {m n : znum} :
m n m n
@[simp, norm_cast]
theorem znum.cast_inj {α : Type u_1} [linear_ordered_ring α] {m n : znum} :
m = n m = n

This tactic tries to turn an (in)equality about znums to one about ints by rewriting.

example (n : znum) (m : znum) : n  n + m * m :=
begin
  znum.transfer_rw,
  exact le_add_of_nonneg_right (mul_self_nonneg _)
end
meta def znum.transfer  :

This tactic tries to prove (in)equalities about znums by transfering them to the int world and then trying to call simp.

example (n : znum) (m : znum) : n  n + m * m :=
begin
  znum.transfer,
  exact mul_self_nonneg _
end
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp, norm_cast]
theorem znum.cast_sub {α : Type u_1} [ring α] (m n : znum) :
(m - n) = m - n
@[simp, norm_cast]
theorem znum.neg_of_int (n : ) :
@[simp]
theorem znum.of_int'_eq (n : ) :
@[simp]
theorem znum.of_nat_to_znum (n : ) :
@[simp, norm_cast]
theorem znum.of_to_int (n : znum) :
theorem znum.to_of_int (n : ) :
@[simp]
@[simp, norm_cast]
theorem znum.of_int_cast {α : Type u_1} [add_group_with_one α] (n : ) :
@[simp, norm_cast]
theorem znum.of_nat_cast {α : Type u_1} [add_group_with_one α] (n : ) :
@[simp, norm_cast]
theorem znum.dvd_to_int (m n : znum) :
m n m n
theorem pos_num.divmod_to_nat_aux {n d : pos_num} {q r : num} (h₁ : r + d * bit0 q = n) (h₂ : r < 2 * d) :
((d.divmod_aux q r).snd) + d * ((d.divmod_aux q r).fst) = n ((d.divmod_aux q r).snd) < d
theorem pos_num.divmod_to_nat (d n : pos_num) :
n / d = ((d.divmod n).fst) n % d = ((d.divmod n).snd)
@[simp]
theorem pos_num.div'_to_nat (n d : pos_num) :
(n.div' d) = n / d
@[simp]
theorem pos_num.mod'_to_nat (n d : pos_num) :
(n.mod' d) = n % d
@[protected, simp]
theorem num.div_zero (n : num) :
n / 0 = 0
@[simp, norm_cast]
theorem num.div_to_nat (n d : num) :
(n / d) = n / d
@[protected, simp]
theorem num.mod_zero (n : num) :
n % 0 = n
@[simp, norm_cast]
theorem num.mod_to_nat (n d : num) :
(n % d) = n % d
theorem num.gcd_to_nat_aux {n : } {a b : num} :
a b (a * b).nat_size n (num.gcd_aux n a b) = a.gcd b
@[simp]
theorem num.gcd_to_nat (a b : num) :
(a.gcd b) = a.gcd b
theorem num.dvd_iff_mod_eq_zero {m n : num} :
m n n % m = 0
@[protected, simp]
theorem znum.div_zero (n : znum) :
n / 0 = 0
@[simp, norm_cast]
theorem znum.div_to_int (n d : znum) :
(n / d) = n / d
@[simp, norm_cast]
theorem znum.mod_to_int (n d : znum) :
(n % d) = n % d
@[simp]
theorem znum.gcd_to_nat (a b : znum) :
(a.gcd b) = a.gcd b
theorem znum.dvd_iff_mod_eq_zero {m n : znum} :
m n n % m = 0

Cast a snum to the corresponding integer.

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations