Properties of the binary representation of integers #
@[simp]
@[simp]
theorem
PosNum.cmp_to_nat_lemma
{m : PosNum}
{n : PosNum}
:
↑m < ↑n → ↑(PosNum.bit1 m) < ↑(PosNum.bit0 n)
theorem
PosNum.cmp_to_nat
(m : PosNum)
(n : PosNum)
:
Ordering.casesOn (PosNum.cmp m n) (↑m < ↑n) (m = n) (↑n < ↑m)
theorem
Num.ofNat'_bit
(b : Bool)
(n : ℕ)
:
Num.ofNat' (Nat.bit b n) = cond b Num.bit1 Num.bit0 (Num.ofNat' n)
@[simp]
theorem
Num.cmp_to_nat
(m : Num)
(n : Num)
:
Ordering.casesOn (Num.cmp m n) (↑m < ↑n) (m = n) (↑n < ↑m)
This tactic tries to turn an (in)equality about Num
s to one about Nat
s by rewriting.
example (n : Num) (m : Num) : n ≤ n + m := by
transfer_rw
exact Nat.le_add_right _ _
Instances For
This tactic tries to turn an (in)equality about PosNum
s to one about Nat
s by rewriting.
example (n : PosNum) (m : PosNum) : n ≤ n + m := by
transfer_rw
exact Nat.le_add_right _ _
Instances For
@[simp]
@[simp]
theorem
PosNum.cast_succ
{α : Type u_1}
[AddMonoidWithOne α]
(n : PosNum)
:
↑(PosNum.succ n) = ↑n + 1
@[simp]
theorem
PosNum.cast_inj
{α : Type u_1}
[AddMonoidWithOne α]
[CharZero α]
{m : PosNum}
{n : PosNum}
:
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem
Num.cast_toZNum
{α : Type u_1}
[Zero α]
[One α]
[Add α]
[Neg α]
(n : Num)
:
↑(Num.toZNum n) = ↑n
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem
Num.bitwise'_to_nat
{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 (Num.pos n) = bif g false true then Num.pos n else 0)
(fn0 : ∀ (n : PosNum), f (Num.pos n) 0 = bif g true false then Num.pos n else 0)
(fnn : ∀ (m n : PosNum), f (Num.pos m) (Num.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) = Num.bit (g true b) (bif g false true then Num.pos n else 0))
(pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = Num.bit (g a true) (bif g true false then Num.pos m 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]
@[simp]
@[simp]
theorem
ZNum.cast_bitm1
{α : Type u_1}
[AddGroupWithOne α]
(n : ZNum)
:
↑(ZNum.bitm1 n) = bit0 ↑n - 1
theorem
PosNum.cast_sub'
{α : Type u_1}
[AddGroupWithOne α]
(m : PosNum)
(n : PosNum)
:
↑(PosNum.sub' m n) = ↑m - ↑n
@[simp]
@[simp]
theorem
Num.cast_ofZNum
{α : Type u_1}
[AddGroupWithOne α]
(n : ZNum)
:
↑(Num.ofZNum n) = ↑(Int.toNat ↑n)
@[simp]
@[simp]
theorem
ZNum.cmp_to_int
(m : ZNum)
(n : ZNum)
:
Ordering.casesOn (ZNum.cmp m n) (↑m < ↑n) (m = n) (↑n < ↑m)
@[simp]
@[simp]
@[simp]
This tactic tries to turn an (in)equality about ZNum
s to one about Int
s by rewriting.
example (n : ZNum) (m : ZNum) : n ≤ n + m * m := by
transfer_rw
exact le_add_of_nonneg_right (mul_self_nonneg _)
Instances For
This tactic tries to prove (in)equalities about ZNum
s 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 _
Instances For
theorem
PosNum.divMod_to_nat_aux
{n : PosNum}
{d : PosNum}
{q : Num}
{r : Num}
(h₁ : ↑r + ↑d * bit0 ↑q = ↑n)
(h₂ : ↑r < 2 * ↑d)
:
↑(PosNum.divModAux d q r).snd + ↑d * ↑(PosNum.divModAux d q r).fst = ↑n ∧ ↑(PosNum.divModAux d q r).snd < ↑d
theorem
PosNum.divMod_to_nat
(d : PosNum)
(n : PosNum)
:
↑n / ↑d = ↑(PosNum.divMod d n).fst ∧ ↑n % ↑d = ↑(PosNum.divMod d n).snd
theorem
Num.gcd_to_nat_aux
{n : ℕ}
{a : Num}
{b : Num}
:
a ≤ b → Num.natSize (a * b) ≤ n → ↑(Num.gcdAux n a b) = Nat.gcd ↑a ↑b