Properties of the binary representation of integers #

source

@[simp]

theorem PosNum.cast_one {α : Type u_1} [One α] [Add α] :

↑1 = 1

source

@[simp]

theorem PosNum.cast_one' {α : Type u_1} [One α] [Add α] :

↑one = 1

source

@[simp]

theorem PosNum.cast_bit0 {α : Type u_1} [One α] [Add α] (n : PosNum) :

↑n.bit0 = ↑n + ↑n

source

@[simp]

theorem PosNum.cast_bit1 {α : Type u_1} [One α] [Add α] (n : PosNum) :

↑n.bit1 = ↑n + ↑n + 1

source

@[simp]

theorem PosNum.cast_to_nat {α : Type u_1} [AddMonoidWithOne α] (n : PosNum) :

↑↑n = ↑n

source

theorem PosNum.to_nat_to_int (n : PosNum) :

↑↑n = ↑n

source

@[simp]

theorem PosNum.cast_to_int {α : Type u_1} [AddGroupWithOne α] (n : PosNum) :

↑↑n = ↑n

source

theorem PosNum.succ_to_nat (n : PosNum) :

↑n.succ = ↑n + 1

source

theorem PosNum.one_add (n : PosNum) :

1 + n = n.succ

source

theorem PosNum.add_one (n : PosNum) :

n + 1 = n.succ

source

theorem PosNum.add_to_nat (m n : PosNum) :

↑(m + n) = ↑m + ↑n

source

theorem PosNum.add_succ (m n : PosNum) :

m + n.succ = (m + n).succ

source

theorem PosNum.bit0_of_bit0 (n : PosNum) :

n + n = n.bit0

source

theorem PosNum.bit1_of_bit1 (n : PosNum) :

n + n + 1 = n.bit1

source

theorem PosNum.mul_to_nat (m n : PosNum) :

↑(m * n) = ↑m * ↑n

source

theorem PosNum.to_nat_pos (n : PosNum) :

0 < ↑n

source

theorem PosNum.cmp_to_nat_lemma {m n : PosNum} :

↑m < ↑n → ↑m.bit1 < ↑n.bit0

source

theorem PosNum.cmp_swap (m n : PosNum) :

(m.cmp n).swap = n.cmp m

source

theorem PosNum.cmp_to_nat (m n : PosNum) :

Ordering.casesOn (m.cmp n) (↑m < ↑n) (m = n) (↑n < ↑m)

source

theorem PosNum.lt_to_nat {m n : PosNum} :

↑m < ↑n ↔ m < n

source

theorem PosNum.le_to_nat {m n : PosNum} :

↑m ≤ ↑n ↔ m ≤ n

source

theorem Num.add_zero (n : Num) :

n + 0 = n

source

theorem Num.zero_add (n : Num) :

0 + n = n

source

theorem Num.add_one (n : Num) :

n + 1 = n.succ

source

theorem Num.add_succ (m n : Num) :

m + n.succ = (m + n).succ

source

theorem Num.bit0_of_bit0 (n : Num) :

n + n = n.bit0

source

theorem Num.bit1_of_bit1 (n : Num) :

n + n + 1 = n.bit1

source

@[simp]

theorem Num.ofNat'_zero :

ofNat' 0 = 0

source

theorem Num.ofNat'_bit (b : Bool) (n : ℕ) :

ofNat' (Nat.bit b n) = (bif b then Num.bit1 else Num.bit0) (ofNat' n)

source

@[simp]

theorem Num.ofNat'_one :

ofNat' 1 = 1

source

theorem Num.bit1_succ (n : Num) :

n.bit1.succ = n.succ.bit0

source

theorem Num.ofNat'_succ {n : ℕ} :

ofNat' (n + 1) = ofNat' n + 1

source

@[simp]

theorem Num.add_ofNat' (m n : ℕ) :

ofNat' (m + n) = ofNat' m + ofNat' n

source

@[simp]

theorem Num.cast_zero {α : Type u_1} [Zero α] [One α] [Add α] :

↑0 = 0

source

@[simp]

theorem Num.cast_zero' {α : Type u_1} [Zero α] [One α] [Add α] :

↑zero = 0

source

@[simp]

theorem Num.cast_one {α : Type u_1} [Zero α] [One α] [Add α] :

↑1 = 1

source

@[simp]

theorem Num.cast_pos {α : Type u_1} [Zero α] [One α] [Add α] (n : PosNum) :

↑(pos n) = ↑n

source

theorem Num.succ'_to_nat (n : Num) :

↑n.succ' = ↑n + 1

source

theorem Num.succ_to_nat (n : Num) :

↑n.succ = ↑n + 1

source

@[simp]

theorem Num.cast_to_nat {α : Type u_1} [AddMonoidWithOne α] (n : Num) :

↑↑n = ↑n

source

theorem Num.add_to_nat (m n : Num) :

↑(m + n) = ↑m + ↑n

source

theorem Num.mul_to_nat (m n : Num) :

↑(m * n) = ↑m * ↑n

source

theorem Num.cmp_to_nat (m n : Num) :

Ordering.casesOn (m.cmp n) (↑m < ↑n) (m = n) (↑n < ↑m)

source

theorem Num.lt_to_nat {m n : Num} :

↑m < ↑n ↔ m < n

source

theorem Num.le_to_nat {m n : Num} :

↑m ≤ ↑n ↔ m ≤ n

source

@[simp]

theorem PosNum.of_to_nat' (n : PosNum) :

Num.ofNat' ↑n = Num.pos n

source

@[simp]

theorem Num.of_to_nat' (n : Num) :

ofNat' ↑n = n

source

theorem Num.toNat_injective :

Function.Injective castNum

source

theorem Num.to_nat_inj {m n : Num} :

↑m = ↑n ↔ m = n

source

def Num.transfer_rw :

Lean.ParserDescr

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
  exact Nat.le_add_right _ _

Equations

Instances For

source

def Num.transfer :

Lean.ParserDescr

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

source

instance Num.addMonoid :

AddMonoid Num

Equations

source

instance Num.addMonoidWithOne :

AddMonoidWithOne Num

Equations

source

instance Num.commSemiring :

CommSemiring Num

Equations

source

instance Num.partialOrder :

PartialOrder Num

Equations

source

instance Num.isOrderedCancelAddMonoid :

IsOrderedCancelAddMonoid Num

source

instance Num.linearOrder :

LinearOrder Num

Equations

source

instance Num.isStrictOrderedRing :

IsStrictOrderedRing Num

source

theorem Num.add_of_nat (m n : ℕ) :

↑(m + n) = ↑m + ↑n

source

theorem Num.to_nat_to_int (n : Num) :

↑↑n = ↑n

source

@[simp]

theorem Num.cast_to_int {α : Type u_1} [AddGroupWithOne α] (n : Num) :

↑↑n = ↑n

source

theorem Num.to_of_nat (n : ℕ) :

↑↑n = n

source

@[simp]

theorem Num.of_natCast {α : Type u_1} [AddMonoidWithOne α] (n : ℕ) :

↑↑n = ↑n

source

theorem Num.of_nat_inj {m n : ℕ} :

↑m = ↑n ↔ m = n

source

@[simp]

theorem Num.of_to_nat (n : Num) :

↑↑n = n

source

theorem Num.dvd_to_nat (m n : Num) :

↑m ∣ ↑n ↔ m ∣ n

source

@[simp]

theorem PosNum.of_to_nat (n : PosNum) :

↑↑n = Num.pos n

source

theorem PosNum.to_nat_inj {m n : PosNum} :

↑m = ↑n ↔ m = n

source

theorem PosNum.pred'_to_nat (n : PosNum) :

↑n.pred' = (↑n).pred

source

@[simp]

theorem PosNum.pred'_succ' (n : Num) :

n.succ'.pred' = n

source

@[simp]

theorem PosNum.succ'_pred' (n : PosNum) :

n.pred'.succ' = n

source

instance PosNum.dvd :

Dvd PosNum

Equations

source

theorem PosNum.dvd_to_nat {m n : PosNum} :

↑m ∣ ↑n ↔ m ∣ n

source

theorem PosNum.size_to_nat (n : PosNum) :

↑n.size = (↑n).size

source

theorem PosNum.size_eq_natSize (n : PosNum) :

↑n.size = n.natSize

source

theorem PosNum.natSize_to_nat (n : PosNum) :

n.natSize = (↑n).size

source

theorem PosNum.natSize_pos (n : PosNum) :

0 < n.natSize

source

def PosNum.transfer_rw :

Lean.ParserDescr

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
  exact Nat.le_add_right _ _

Equations

Instances For

source

def PosNum.transfer :

Lean.ParserDescr

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

source

instance PosNum.addCommSemigroup :

AddCommSemigroup PosNum

Equations

source

instance PosNum.commMonoid :

CommMonoid PosNum

Equations

source

instance PosNum.distrib :

Distrib PosNum

Equations

source

instance PosNum.linearOrder :

LinearOrder PosNum

Equations

source

@[simp]

theorem PosNum.cast_to_num (n : PosNum) :

↑n = Num.pos n

source

@[simp]

theorem PosNum.bit_to_nat (b : Bool) (n : PosNum) :

↑(bit b n) = Nat.bit b ↑n

source

@[simp]

theorem PosNum.cast_add {α : Type u_1} [AddMonoidWithOne α] (m n : PosNum) :

↑(m + n) = ↑m + ↑n

source

@[simp]

theorem PosNum.cast_succ {α : Type u_1} [AddMonoidWithOne α] (n : PosNum) :

↑n.succ = ↑n + 1

source

@[simp]

theorem PosNum.cast_inj {α : Type u_1} [AddMonoidWithOne α] [CharZero α] {m n : PosNum} :

↑m = ↑n ↔ m = n

source

@[simp]

theorem PosNum.one_le_cast {α : Type u_1} [Semiring α] [PartialOrder α] [IsStrictOrderedRing α] (n : PosNum) :

1 ≤ ↑n

source

@[simp]

theorem PosNum.cast_pos {α : Type u_1} [Semiring α] [PartialOrder α] [IsStrictOrderedRing α] (n : PosNum) :

0 < ↑n

source

@[simp]

theorem PosNum.cast_mul {α : Type u_1} [NonAssocSemiring α] (m n : PosNum) :

↑(m * n) = ↑m * ↑n

source

@[simp]

theorem PosNum.cmp_eq (m n : PosNum) :

m.cmp n = Ordering.eq ↔ m = n

source

@[simp]

theorem PosNum.cast_lt {α : Type u_1} [Semiring α] [PartialOrder α] [IsStrictOrderedRing α] {m n : PosNum} :

↑m < ↑n ↔ m < n

source

@[simp]

theorem PosNum.cast_le {α : Type u_1} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] {m n : PosNum} :

↑m ≤ ↑n ↔ m ≤ n

source

theorem Num.bit_to_nat (b : Bool) (n : Num) :

↑(bit b n) = Nat.bit b ↑n

source

theorem Num.cast_succ' {α : Type u_1} [AddMonoidWithOne α] (n : Num) :

↑n.succ' = ↑n + 1

source

theorem Num.cast_succ {α : Type u_1} [AddMonoidWithOne α] (n : Num) :

↑n.succ = ↑n + 1

source

@[simp]

theorem Num.cast_add {α : Type u_1} [AddMonoidWithOne α] (m n : Num) :

↑(m + n) = ↑m + ↑n

source

@[simp]

theorem Num.cast_bit0 {α : Type u_1} [NonAssocSemiring α] (n : Num) :

↑n.bit0 = 2 * ↑n

source

@[simp]

theorem Num.cast_bit1 {α : Type u_1} [NonAssocSemiring α] (n : Num) :

↑n.bit1 = 2 * ↑n + 1

source

@[simp]

theorem Num.cast_mul {α : Type u_1} [NonAssocSemiring α] (m n : Num) :

↑(m * n) = ↑m * ↑n

source

theorem Num.size_to_nat (n : Num) :

↑n.size = (↑n).size

source

theorem Num.size_eq_natSize (n : Num) :

↑n.size = n.natSize

source

theorem Num.natSize_to_nat (n : Num) :

n.natSize = (↑n).size

source

@[simp]

theorem Num.ofNat'_eq (n : ℕ) :

ofNat' n = ↑n

source

theorem Num.zneg_toZNum (n : Num) :

-n.toZNum = n.toZNumNeg

source

theorem Num.zneg_toZNumNeg (n : Num) :

-n.toZNumNeg = n.toZNum

source

theorem Num.toZNum_inj {m n : Num} :

m.toZNum = n.toZNum ↔ m = n

source

@[simp]

theorem Num.cast_toZNum {α : Type u_1} [Zero α] [One α] [Add α] [Neg α] (n : Num) :

↑n.toZNum = ↑n

source

@[simp]

theorem Num.cast_toZNumNeg {α : Type u_1} [SubtractionMonoid α] [One α] (n : Num) :

↑n.toZNumNeg = -↑n

source

@[simp]

theorem Num.add_toZNum (m n : Num) :

(m + n).toZNum = m.toZNum + n.toZNum

source

theorem PosNum.pred_to_nat {n : PosNum} (h : 1 < n) :

↑n.pred = (↑n).pred

source

theorem PosNum.sub'_one (a : PosNum) :

a.sub' 1 = a.pred'.toZNum

source

theorem PosNum.one_sub' (a : PosNum) :

sub' 1 a = a.pred'.toZNumNeg

source

theorem PosNum.lt_iff_cmp {m n : PosNum} :

m < n ↔ m.cmp n = Ordering.lt

source

theorem PosNum.le_iff_cmp {m n : PosNum} :

m ≤ n ↔ m.cmp n ≠ Ordering.gt

source

theorem Num.pred_to_nat (n : Num) :

↑n.pred = (↑n).pred

source

theorem Num.ppred_to_nat (n : Num) :

castNum <$> n.ppred = (↑n).ppred

source

theorem Num.cmp_swap (m n : Num) :

(m.cmp n).swap = n.cmp m

source

theorem Num.cmp_eq (m n : Num) :

m.cmp n = Ordering.eq ↔ m = n

source

@[simp]

theorem Num.cast_lt {α : Type u_1} [Semiring α] [PartialOrder α] [IsStrictOrderedRing α] {m n : Num} :

↑m < ↑n ↔ m < n

source

@[simp]

theorem Num.cast_le {α : Type u_1} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] {m n : Num} :

↑m ≤ ↑n ↔ m ≤ n

source

@[simp]

theorem Num.cast_inj {α : Type u_1} [Semiring α] [PartialOrder α] [IsStrictOrderedRing α] {m n : Num} :

↑m = ↑n ↔ m = n

source

theorem Num.lt_iff_cmp {m n : Num} :

m < n ↔ m.cmp n = Ordering.lt

source

theorem Num.le_iff_cmp {m n : Num} :

m ≤ n ↔ m.cmp n ≠ Ordering.gt

source

theorem Num.castNum_eq_bitwise {f : Num → Num → Num} {g : Bool → Bool → Bool} (p : PosNum → PosNum → Num) (gff : g false false = false) (f00 : f 0 0 = 0) (f0n : ∀ (n : PosNum), f 0 (pos n) = bif g false true then pos n else 0) (fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0) (fnn : ∀ (m n : PosNum), f (pos m) (pos n) = p m n) (p11 : p 1 1 = bif g true true then 1 else 0) (p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then pos n else 0)) (pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then pos m else 0)) (pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)) (m n : Num) :

↑(f m n) = Nat.bitwise g ↑m ↑n

source

@[simp]

theorem Num.castNum_or (m n : Num) :

↑(m ||| n) = ↑m ||| ↑n

source

@[simp]

theorem Num.castNum_and (m n : Num) :

↑(m &&& n) = ↑m &&& ↑n

source

@[simp]

theorem Num.castNum_ldiff (m n : Num) :