mathlib documentation

data.num.lemmas

Properties of the binary representation of integers

@[simp]
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]
theorem pos_num.cast_bit0 {α : Type u_1} [has_one α] [has_add α] (n : pos_num) :

@[simp]
theorem pos_num.cast_bit1 {α : Type u_1} [has_one α] [has_add α] (n : pos_num) :

@[simp]
theorem pos_num.cast_to_nat {α : Type u_1} [add_monoid α] [has_one α] (n : pos_num) :

@[simp]

@[simp]
theorem pos_num.cast_to_int {α : Type u_1} [add_group α] [has_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

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

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_to_nat_lemma {m n : pos_num} :
m < n(m.bit1) < (n.bit0)

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)

theorem pos_num.lt_to_nat {m n : pos_num} :
m < n m < n

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

@[simp]
theorem num.add_of_nat (m n : ) :
(m + n) = m + n

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.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]
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]
theorem num.cast_to_nat {α : Type u_1} [add_monoid α] [has_one α] (n : num) :

@[simp]
theorem num.to_nat_to_int (n : num) :

@[simp]
theorem num.cast_to_int {α : Type u_1} [add_group α] [has_one α] (n : num) :

theorem num.to_of_nat (n : ) :

@[simp]
theorem num.of_nat_cast {α : Type u_1} [add_monoid α] [has_one α] (n : ) :

theorem num.of_nat_inj {m n : } :
m = n m = n

theorem num.add_to_nat (m n : num) :
(m + n) = m + n

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)

theorem num.lt_to_nat {m n : num} :
m < n m < n

theorem num.le_to_nat {m n : num} :
m n m n

@[simp]
theorem pos_num.of_to_nat (n : pos_num) :

@[simp]
theorem num.of_to_nat (n : num) :

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
@[instance]

Equations
@[instance]

Equations
theorem num.dvd_to_nat (m n : num) :
m n m n

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) :

@[instance]

Equations
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
@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
@[simp]
theorem pos_num.cast_to_num (n : pos_num) :

@[simp]
theorem pos_num.bit_to_nat (b : bool) (n : pos_num) :

@[simp]
theorem pos_num.cast_add {α : Type u_1} [add_monoid α] [has_one α] (m n : pos_num) :
(m + n) = m + n

@[simp]
theorem pos_num.cast_succ {α : Type u_1} [add_monoid α] [has_one α] (n : pos_num) :
(n.succ) = n + 1

@[simp]
theorem pos_num.cast_inj {α : Type u_1} [add_monoid α] [has_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]
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]
theorem pos_num.cast_lt {α : Type u_1} [linear_ordered_semiring α] {m n : pos_num} :
m < n m < n

@[simp]
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 α] [has_one α] (n : num) :
(n.succ') = n + 1

theorem num.cast_succ {α : Type u_1} [add_monoid α] [has_one α] (n : num) :
(n.succ) = n + 1

@[simp]
theorem num.cast_add {α : Type u_1} [semiring α] (m n : num) :
(m + n) = m + n

@[simp]
theorem num.cast_bit0 {α : Type u_1} [semiring α] (n : num) :

@[simp]
theorem num.cast_bit1 {α : Type u_1} [semiring α] (n : num) :

@[simp]
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]
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} :
1 < n(n.pred) = n.pred

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]
theorem num.cast_lt {α : Type u_1} [linear_ordered_semiring α] {m n : num} :
m < n m < n

@[simp]
theorem num.cast_le {α : Type u_1} [linear_ordered_semiring α] {m n : num} :
m n m n

@[simp]
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 : numnumnum} {g : boolboolbool} (p : pos_numpos_numnum) (gff : g ff ff = ff) (f00 : f 0 0 = 0) (f0n : ∀ (n : pos_num), f 0 (num.pos n) = cond (g ff tt) (num.pos n) 0) (fn0 : ∀ (n : pos_num), f (num.pos n) 0 = cond (g tt 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 tt tt) 1 0) (p1b : ∀ (b : bool) (n : pos_num), p 1 (pos_num.bit b n) = num.bit (g tt b) (cond (g ff tt) (num.pos n) 0)) (pb1 : ∀ (a : bool) (m : pos_num), p (pos_num.bit a m) 1 = num.bit (g a tt) (cond (g tt 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]
theorem num.lor_to_nat (m n : num) :
(m.lor n) = m.lor n

@[simp]
theorem num.land_to_nat (m n : num) :
(m.land n) = m.land n

@[simp]
theorem num.ldiff_to_nat (m n : num) :

@[simp]
theorem num.lxor_to_nat (m n : num) :
(m.lxor n) = m.lxor n

@[simp]
theorem num.shiftl_to_nat (m : num) (n : ) :

@[simp]
theorem num.shiftr_to_nat (m : num) (n : ) :

@[simp]
theorem num.test_bit_to_nat (m : num) (n : ) :

@[simp]
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]
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]
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.neg_of_int (n : ) :

@[simp]
theorem znum.abs_to_nat (n : znum) :

@[simp]
theorem znum.abs_to_znum (n : num) :

@[simp]
theorem znum.cast_to_int {α : Type u_1} [add_group α] [has_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]
theorem znum.cast_bit0 {α : Type u_1} [add_group α] [has_one α] (n : znum) :

@[simp]
theorem znum.cast_bit1 {α : Type u_1} [add_group α] [has_one α] (n : znum) :

@[simp]
theorem znum.cast_bitm1 {α : Type u_1} [add_group α] [has_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 α] [has_one α] (m n : pos_num) :
(m.sub' n) = m - n

@[simp]
theorem num.cast_sub' {α : Type u_1} [add_group α] [has_one α] (m n : num) :
(m.sub' n) = m - n

@[simp]
theorem num.of_nat_to_znum (n : ) :

@[simp]

theorem num.mem_of_znum' {m : num} {n : znum} :

@[simp]

@[simp]
theorem num.cast_of_znum {α : Type u_1} [add_group α] [has_one α] (n : znum) :

@[simp]
theorem num.sub_to_nat (m n : num) :
(m - n) = m - n

@[simp]
theorem znum.cast_add {α : Type u_1} [add_group α] [has_one α] (m n : znum) :
(m + n) = m + n

@[simp]
theorem znum.cast_succ {α : Type u_1} [add_group α] [has_one α] (n : znum) :
(n.succ) = n + 1

@[simp]
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

@[simp]
theorem znum.of_to_int (n : znum) :

theorem znum.to_of_int (n : ) :

theorem znum.to_int_inj {m n : znum} :
m = n m = n

@[simp]
theorem znum.of_int_cast {α : Type u_1} [add_group α] [has_one α] (n : ) :

@[simp]
theorem znum.of_nat_cast {α : Type u_1} [add_group α] [has_one α] (n : ) :

@[simp]
theorem znum.of_int'_eq (n : ) :

theorem znum.cmp_to_int (m n : znum) :
(m.cmp n).cases_on (m < n) (m = n) (n < m)

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]
theorem znum.cast_lt {α : Type u_1} [linear_ordered_ring α] {m n : znum} :
m < n m < n

@[simp]
theorem znum.cast_le {α : Type u_1} [linear_ordered_ring α] {m n : znum} :
m n m n

@[simp]
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
@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
@[simp]
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} :
r + (d) * bit0 q = nr < 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

@[simp]
theorem num.div_to_nat (n d : num) :
(n / d) = n / d

@[simp]
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

@[simp]
theorem znum.div_to_int (n d : znum) :
(n / d) = n / d

@[simp]
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

def int.of_snum  :
snum

Cast a snum to the corresponding integer.

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

Equations