# Properties of the binary representation of integers #

@[simp]
theorem PosNum.cast_one {α : Type u_1} [One α] [Add α] :
1 = 1
@[simp]
theorem PosNum.cast_one' {α : Type u_1} [One α] [Add α] :
@[simp]
theorem PosNum.cast_bit0 {α : Type u_1} [One α] [Add α] (n : PosNum) :
n.bit0 = n + n
@[simp]
theorem PosNum.cast_bit1 {α : Type u_1} [One α] [Add α] (n : PosNum) :
n.bit1 = n + n + 1
@[simp]
theorem PosNum.cast_to_nat {α : Type u_1} [] (n : PosNum) :
n = n
theorem PosNum.to_nat_to_int (n : PosNum) :
n = n
@[simp]
theorem PosNum.cast_to_int {α : Type u_1} [] (n : PosNum) :
n = n
theorem PosNum.succ_to_nat (n : PosNum) :
n.succ = n + 1
theorem PosNum.one_add (n : PosNum) :
1 + n = n.succ
theorem PosNum.add_one (n : PosNum) :
n + 1 = n.succ
theorem PosNum.add_to_nat (m : PosNum) (n : PosNum) :
(m + n) = m + n
theorem PosNum.add_succ (m : PosNum) (n : PosNum) :
m + n.succ = (m + n).succ
theorem PosNum.bit0_of_bit0 (n : PosNum) :
n + n = n.bit0
theorem PosNum.bit1_of_bit1 (n : PosNum) :
n + n + 1 = n.bit1
theorem PosNum.mul_to_nat (m : PosNum) (n : PosNum) :
(m * n) = m * n
theorem PosNum.to_nat_pos (n : PosNum) :
0 < n
theorem PosNum.cmp_to_nat_lemma {m : PosNum} {n : PosNum} :
m < nm.bit1 < n.bit0
theorem PosNum.cmp_swap (m : PosNum) (n : PosNum) :
(m.cmp n).swap = n.cmp m
theorem PosNum.cmp_to_nat (m : PosNum) (n : PosNum) :
Ordering.casesOn (m.cmp n) (m < n) (m = n) (n < m)
theorem PosNum.lt_to_nat {m : PosNum} {n : PosNum} :
m < n m < n
theorem PosNum.le_to_nat {m : PosNum} {n : PosNum} :
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 : Num) (n : Num) :
m + n.succ = (m + n).succ
theorem Num.bit0_of_bit0 (n : Num) :
n + n = n.bit0
theorem Num.bit1_of_bit1 (n : Num) :
n + n + 1 = n.bit1
@[simp]
theorem Num.ofNat'_zero :
= 0
theorem Num.ofNat'_bit (b : Bool) (n : ) :
Num.ofNat' (Nat.bit b n) = (bif b then Num.bit1 else Num.bit0) (Num.ofNat' n)
@[simp]
theorem Num.ofNat'_one :
= 1
theorem Num.bit1_succ (n : Num) :
n.bit1.succ = n.succ.bit0
theorem Num.ofNat'_succ {n : } :
Num.ofNat' (n + 1) = + 1
@[simp]
theorem Num.add_ofNat' (m : ) (n : ) :
Num.ofNat' (m + n) =
@[simp]
theorem Num.cast_zero {α : Type u_1} [Zero α] [One α] [Add α] :
0 = 0
@[simp]
theorem Num.cast_zero' {α : Type u_1} [Zero α] [One α] [Add α] :
@[simp]
theorem Num.cast_one {α : Type u_1} [Zero α] [One α] [Add α] :
1 = 1
@[simp]
theorem Num.cast_pos {α : Type u_1} [Zero α] [One α] [Add α] (n : PosNum) :
(Num.pos n) = n
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} [] (n : Num) :
n = n
theorem Num.add_to_nat (m : Num) (n : Num) :
(m + n) = m + n
theorem Num.mul_to_nat (m : Num) (n : Num) :
(m * n) = m * n
theorem Num.cmp_to_nat (m : Num) (n : Num) :
Ordering.casesOn (m.cmp n) (m < n) (m = n) (n < m)
theorem Num.lt_to_nat {m : Num} {n : Num} :
m < n m < n
theorem Num.le_to_nat {m : Num} {n : Num} :
m n m n
@[simp]
theorem PosNum.of_to_nat' (n : PosNum) :
=
@[simp]
theorem Num.of_to_nat' (n : Num) :
= n
theorem Num.to_nat_inj {m : Num} {n : Num} :
m = n m = n

This tactic tries to turn an (in)equality about Nums to one about Nats by rewriting.

example (n : Num) (m : Num) : n ≤ n + m := by
transfer_rw

Equations
Instances For

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

example (n : Num) (m : Num) : n ≤ n + m := by transfer

Equations
Instances For
Equations
Equations
instance Num.commSemiring :
Equations
Equations
• One or more equations did not get rendered due to their size.
theorem Num.add_of_nat (m : ) (n : ) :
(m + n) = m + n
theorem Num.to_nat_to_int (n : Num) :
n = n
@[simp]
theorem Num.cast_to_int {α : Type u_1} [] (n : Num) :
n = n
theorem Num.to_of_nat (n : ) :
n = n
@[simp]
theorem Num.of_natCast {α : Type u_1} [] (n : ) :
n = n
@[deprecated Num.of_natCast]
theorem Num.of_nat_cast {α : Type u_1} [] (n : ) :
n = n

Alias of Num.of_natCast.

theorem Num.of_nat_inj {m : } {n : } :
m = n m = n
@[simp]
theorem Num.of_to_nat (n : Num) :
n = n
theorem Num.dvd_to_nat (m : Num) (n : Num) :
m n m n
@[simp]
theorem PosNum.of_to_nat (n : PosNum) :
n =
theorem PosNum.to_nat_inj {m : PosNum} {n : PosNum} :
m = n m = n
theorem PosNum.pred'_to_nat (n : PosNum) :
n.pred' = (↑n).pred
@[simp]
theorem PosNum.pred'_succ' (n : Num) :
n.succ'.pred' = n
@[simp]
theorem PosNum.succ'_pred' (n : PosNum) :
n.pred'.succ' = n
instance PosNum.dvd :
Equations
theorem PosNum.dvd_to_nat {m : PosNum} {n : PosNum} :
m n m n
theorem PosNum.size_to_nat (n : PosNum) :
n.size = (↑n).size
theorem PosNum.size_eq_natSize (n : PosNum) :
n.size = n.natSize
theorem PosNum.natSize_to_nat (n : PosNum) :
n.natSize = (↑n).size
theorem PosNum.natSize_pos (n : PosNum) :
0 < n.natSize

This tactic tries to turn an (in)equality about PosNums to one about Nats by rewriting.

example (n : PosNum) (m : PosNum) : n ≤ n + m := by
transfer_rw

Equations
Instances For

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

example (n : PosNum) (m : PosNum) : n ≤ n + m := by transfer

Equations
Instances For
Equations
@[simp]
theorem PosNum.cast_to_num (n : PosNum) :
n =
@[simp]
theorem PosNum.bit_to_nat (b : Bool) (n : PosNum) :
(PosNum.bit b n) = Nat.bit b n
@[simp]
theorem PosNum.cast_add {α : Type u_1} [] (m : PosNum) (n : PosNum) :
(m + n) = m + n
@[simp]
theorem PosNum.cast_succ {α : Type u_1} [] (n : PosNum) :
n.succ = n + 1
@[simp]
theorem PosNum.cast_inj {α : Type u_1} [] [] {m : PosNum} {n : PosNum} :
m = n m = n
@[simp]
theorem PosNum.one_le_cast {α : Type u_1} (n : PosNum) :
1 n
@[simp]
theorem PosNum.cast_pos {α : Type u_1} (n : PosNum) :
0 < n
@[simp]
theorem PosNum.cast_mul {α : Type u_1} [] (m : PosNum) (n : PosNum) :
(m * n) = m * n
@[simp]
theorem PosNum.cmp_eq (m : PosNum) (n : PosNum) :
m.cmp n = Ordering.eq m = n
@[simp]
theorem PosNum.cast_lt {α : Type u_1} {m : PosNum} {n : PosNum} :
m < n m < n
@[simp]
theorem PosNum.cast_le {α : Type u_1} {m : PosNum} {n : PosNum} :
m n m n
theorem Num.bit_to_nat (b : Bool) (n : Num) :
(Num.bit b n) = Nat.bit b n
theorem Num.cast_succ' {α : Type u_1} [] (n : Num) :
n.succ' = n + 1
theorem Num.cast_succ {α : Type u_1} [] (n : Num) :
n.succ = n + 1
@[simp]
theorem Num.cast_add {α : Type u_1} [] (m : Num) (n : Num) :
(m + n) = m + n
@[simp]
theorem Num.cast_bit0 {α : Type u_1} [] (n : Num) :
n.bit0 = 2 * n
@[simp]
theorem Num.cast_bit1 {α : Type u_1} [] (n : Num) :
n.bit1 = 2 * n + 1
@[simp]
theorem Num.cast_mul {α : Type u_1} [] (m : Num) (n : Num) :
(m * n) = m * n
theorem Num.size_to_nat (n : Num) :
n.size = (↑n).size
theorem Num.size_eq_natSize (n : Num) :
n.size = n.natSize
theorem Num.natSize_to_nat (n : Num) :
n.natSize = (↑n).size
@[simp]
theorem Num.ofNat'_eq (n : ) :
= n
theorem Num.zneg_toZNum (n : Num) :
-n.toZNum = n.toZNumNeg
theorem Num.zneg_toZNumNeg (n : Num) :
-n.toZNumNeg = n.toZNum
theorem Num.toZNum_inj {m : Num} {n : Num} :
m.toZNum = n.toZNum m = n
@[simp]
theorem Num.cast_toZNum {α : Type u_1} [Zero α] [One α] [Add α] [Neg α] (n : Num) :
n.toZNum = n
@[simp]
theorem Num.cast_toZNumNeg {α : Type u_1} [] [One α] (n : Num) :
n.toZNumNeg = -n
@[simp]
theorem Num.add_toZNum (m : Num) (n : Num) :
(m + n).toZNum = m.toZNum + n.toZNum
theorem PosNum.pred_to_nat {n : PosNum} (h : 1 < n) :
n.pred = (↑n).pred
theorem PosNum.sub'_one (a : PosNum) :
a.sub' 1 = a.pred'.toZNum
theorem PosNum.one_sub' (a : PosNum) :
= a.pred'.toZNumNeg
theorem PosNum.lt_iff_cmp {m : PosNum} {n : PosNum} :
m < n m.cmp n = Ordering.lt
theorem PosNum.le_iff_cmp {m : PosNum} {n : PosNum} :
m n m.cmp n Ordering.gt
theorem Num.pred_to_nat (n : Num) :
n.pred = (↑n).pred
theorem Num.ppred_to_nat (n : Num) :
castNum <$> n.ppred = (↑n).ppred theorem Num.cmp_swap (m : Num) (n : Num) : (m.cmp n).swap = n.cmp m theorem Num.cmp_eq (m : Num) (n : Num) : m.cmp n = Ordering.eq m = n @[simp] theorem Num.cast_lt {α : Type u_1} {m : Num} {n : Num} : m < n m < n @[simp] theorem Num.cast_le {α : Type u_1} {m : Num} {n : Num} : m n m n @[simp] theorem Num.cast_inj {α : Type u_1} {m : Num} {n : Num} : m = n m = n theorem Num.lt_iff_cmp {m : Num} {n : Num} : m < n m.cmp n = Ordering.lt theorem Num.le_iff_cmp {m : Num} {n : Num} : m n m.cmp n Ordering.gt theorem Num.castNum_eq_bitwise {f : } {g : } (p : ) (gff : ) (f00 : f 0 0 = 0) (f0n : ∀ (n : PosNum), f 0 (Num.pos n) = bif then else 0) (fn0 : ∀ (n : PosNum), f (Num.pos n) 0 = bif then else 0) (fnn : ∀ (m n : PosNum), f (Num.pos m) (Num.pos n) = p m n) (p11 : p 1 1 = bif then 1 else 0) (p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = Num.bit (g true b) (bif then else 0)) (pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = Num.bit (g a true) (bif then else 0)) (pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = Num.bit (g a b) (p m n)) (m : Num) (n : Num) : (f m n) = Nat.bitwise g m n @[simp] theorem Num.castNum_or (m : Num) (n : Num) : (m ||| n) = m ||| n @[simp] theorem Num.castNum_and (m : Num) (n : Num) : (m &&& n) = m &&& n @[simp] theorem Num.castNum_ldiff (m : Num) (n : Num) : (m.ldiff n) = (↑m).ldiff n @[simp] theorem Num.castNum_xor (m : Num) (n : Num) : (m ^^^ n) = m ^^^ n @[simp] theorem Num.castNum_shiftLeft (m : Num) (n : ) : (m <<< n) = m <<< n @[simp] theorem Num.castNum_shiftRight (m : Num) (n : ) : (m >>> n) = m >>> n @[simp] theorem Num.castNum_testBit (m : Num) (n : ) : m.testBit n = (↑m).testBit n @[simp] theorem ZNum.cast_zero {α : Type u_1} [Zero α] [One α] [Add α] [Neg α] : 0 = 0 @[simp] theorem ZNum.cast_zero' {α : Type u_1} [Zero α] [One α] [Add α] [Neg α] : @[simp] theorem ZNum.cast_one {α : Type u_1} [Zero α] [One α] [Add α] [Neg α] : 1 = 1 @[simp] theorem ZNum.cast_pos {α : Type u_1} [Zero α] [One α] [Add α] [Neg α] (n : PosNum) : (ZNum.pos n) = n @[simp] theorem ZNum.cast_neg {α : Type u_1} [Zero α] [One α] [Add α] [Neg α] (n : PosNum) : (ZNum.neg n) = -n @[simp] theorem ZNum.cast_zneg {α : Type u_1} [] [One α] (n : ZNum) : (-n) = -n theorem ZNum.neg_zero : -0 = 0 theorem ZNum.zneg_pos (n : PosNum) : theorem ZNum.zneg_neg (n : PosNum) : 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) : n.abs = (↑n).natAbs @[simp] theorem ZNum.abs_toZNum (n : Num) : n.toZNum.abs = n @[simp] theorem ZNum.cast_to_int {α : Type u_1} [] (n : ZNum) : n = n theorem ZNum.bit0_of_bit0 (n : ZNum) : n + n = n.bit0 theorem ZNum.bit1_of_bit1 (n : ZNum) : n + n + 1 = n.bit1 @[simp] theorem ZNum.cast_bit0 {α : Type u_1} [] (n : ZNum) : n.bit0 = n + n @[simp] theorem ZNum.cast_bit1 {α : Type u_1} [] (n : ZNum) : n.bit1 = n + n + 1 @[simp] theorem ZNum.cast_bitm1 {α : Type u_1} [] (n : ZNum) : n.bitm1 = n + n - 1 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 PosNum.cast_to_znum (n : PosNum) : n = theorem PosNum.cast_sub' {α : Type u_1} [] (m : PosNum) (n : PosNum) : (m.sub' n) = m - n theorem PosNum.to_nat_eq_succ_pred (n : PosNum) : n = n.pred' + 1 theorem PosNum.to_int_eq_succ_pred (n : PosNum) : n = n.pred' + 1 @[simp] theorem Num.cast_sub' {α : Type u_1} [] (m : Num) (n : Num) : (m.sub' n) = m - n theorem Num.toZNum_succ (n : Num) : n.succ.toZNum = n.toZNum.succ theorem Num.toZNumNeg_succ (n : Num) : n.succ.toZNumNeg = n.toZNumNeg.pred @[simp] theorem Num.pred_succ (n : ZNum) : n.pred.succ = n theorem Num.succ_ofInt' (n : ) : ZNum.ofInt' (n + 1) = + 1 theorem Num.ofInt'_toZNum (n : ) : (↑n).toZNum = theorem Num.mem_ofZNum' {m : Num} {n : ZNum} : m n = m.toZNum theorem Num.ofZNum'_toNat (n : ZNum) : castNum <$> = (↑n).toNat'
@[simp]
theorem Num.ofZNum_toNat (n : ZNum) :
(Num.ofZNum n) = (↑n).toNat
@[simp]
theorem Num.cast_ofZNum {α : Type u_1} [] (n : ZNum) :
(Num.ofZNum n) = (↑n).toNat
@[simp]
theorem Num.sub_to_nat (m : Num) (n : Num) :
(m - n) = m - n
@[simp]
theorem ZNum.cast_add {α : Type u_1} [] (m : ZNum) (n : ZNum) :
(m + n) = m + n
@[simp]
theorem ZNum.cast_succ {α : Type u_1} [] (n : ZNum) :
n.succ = n + 1
@[simp]
theorem ZNum.mul_to_int (m : ZNum) (n : ZNum) :
(m * n) = m * n
theorem ZNum.cast_mul {α : Type u_1} [Ring α] (m : ZNum) (n : ZNum) :
(m * n) = m * n
theorem ZNum.ofInt'_neg (n : ) :
theorem ZNum.of_to_int' (n : ZNum) :
= n
theorem ZNum.to_int_inj {m : ZNum} {n : ZNum} :
m = n m = n
theorem ZNum.cmp_to_int (m : ZNum) (n : ZNum) :
Ordering.casesOn (m.cmp n) (m < n) (m = n) (n < m)
theorem ZNum.lt_to_int {m : ZNum} {n : ZNum} :
m < n m < n
theorem ZNum.le_to_int {m : ZNum} {n : ZNum} :
m n m n
@[simp]
theorem ZNum.cast_lt {α : Type u_1} {m : ZNum} {n : ZNum} :
m < n m < n
@[simp]
theorem ZNum.cast_le {α : Type u_1} {m : ZNum} {n : ZNum} :
m n m n
@[simp]
theorem ZNum.cast_inj {α : Type u_1} {m : ZNum} {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 := by
transfer_rw

Equations
Instances For

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

example (n : ZNum) (m : ZNum) : n ≤ n + m * m := by
transfer
exact mul_self_nonneg _

Equations
Instances For
Equations
@[simp]
theorem ZNum.cast_sub {α : Type u_1} [Ring α] (m : ZNum) (n : ZNum) :
(m - n) = m - n
theorem ZNum.neg_of_int (n : ) :
(-n) = -n
@[simp]
theorem ZNum.ofInt'_eq (n : ) :
= n
@[simp]
theorem ZNum.of_nat_toZNum (n : ) :
(↑n).toZNum = n
@[simp]
theorem ZNum.of_to_int (n : ZNum) :
n = n
theorem ZNum.to_of_int (n : ) :
n = n
@[simp]
theorem ZNum.of_nat_toZNumNeg (n : ) :
(↑n).toZNumNeg = -n
@[simp]
theorem ZNum.of_intCast {α : Type u_1} [] (n : ) :
n = n
@[deprecated ZNum.of_intCast]
theorem ZNum.of_int_cast {α : Type u_1} [] (n : ) :
n = n

Alias of ZNum.of_intCast.

@[simp]
theorem ZNum.of_natCast {α : Type u_1} [] (n : ) :
n = n
@[deprecated ZNum.of_natCast]
theorem ZNum.of_nat_cast {α : Type u_1} [] (n : ) :
n = n

Alias of ZNum.of_natCast.

@[simp]
theorem ZNum.dvd_to_int (m : ZNum) (n : ZNum) :
m n m n
theorem PosNum.divMod_to_nat_aux {n : PosNum} {d : PosNum} {q : Num} {r : Num} (h₁ : r + d * (q + q) = n) (h₂ : r < 2 * d) :
(d.divModAux q r).2 + d * (d.divModAux q r).1 = n (d.divModAux q r).2 < d
theorem PosNum.divMod_to_nat (d : PosNum) (n : PosNum) :
n / d = (d.divMod n).1 n % d = (d.divMod n).2
@[simp]
theorem PosNum.div'_to_nat (n : PosNum) (d : PosNum) :
(n.div' d) = n / d
@[simp]
theorem PosNum.mod'_to_nat (n : PosNum) (d : PosNum) :
(n.mod' d) = n % d
@[simp]
theorem Num.div_zero (n : Num) :
n / 0 = 0
@[simp]
theorem Num.div_to_nat (n : Num) (d : Num) :
(n / d) = n / d
@[simp]
theorem Num.mod_zero (n : Num) :
n % 0 = n
@[simp]
theorem Num.mod_to_nat (n : Num) (d : Num) :
(n % d) = n % d
theorem Num.gcd_to_nat_aux {n : } {a : Num} {b : Num} :
a b(a * b).natSize n(Num.gcdAux n a b) = (↑a).gcd b
@[simp]
theorem Num.gcd_to_nat (a : Num) (b : Num) :
(a.gcd b) = (↑a).gcd b
theorem Num.dvd_iff_mod_eq_zero {m : Num} {n : Num} :
m n n % m = 0
instance Num.decidableDvd :
DecidableRel fun (x1 x2 : Num) => x1 x2
Equations
instance PosNum.decidableDvd :
DecidableRel fun (x1 x2 : PosNum) => x1 x2
Equations
@[simp]
theorem ZNum.div_zero (n : ZNum) :
n / 0 = 0
@[simp]
theorem ZNum.div_to_int (n : ZNum) (d : ZNum) :
(n / d) = n / d
@[simp]
theorem ZNum.mod_to_int (n : ZNum) (d : ZNum) :
(n % d) = n % d
@[simp]
theorem ZNum.gcd_to_nat (a : ZNum) (b : ZNum) :
(a.gcd b) = (↑a).gcd b
theorem ZNum.dvd_iff_mod_eq_zero {m : ZNum} {n : ZNum} :
m n n % m = 0
instance ZNum.decidableDvd :
DecidableRel fun (x1 x2 : ZNum) => x1 x2
Equations

Cast a SNum to the corresponding integer.

Equations
Instances For
instance Int.snumCoe :
Equations
instance SNum.lt :
Equations
instance SNum.le :
Equations