Documentation

Mathlib.Data.Num.Lemmas

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) :
↑(PosNum.bit0 n) = bit0 n
@[simp]
theorem PosNum.cast_bit1 {α : Type u_1} [One α] [Add α] (n : PosNum) :
↑(PosNum.bit1 n) = bit1 n
@[simp]
theorem PosNum.cast_to_nat {α : Type u_1} [AddMonoidWithOne α] (n : PosNum) :
n = n
theorem PosNum.to_nat_to_int (n : PosNum) :
n = n
@[simp]
theorem PosNum.cast_to_int {α : Type u_1} [AddGroupWithOne α] (n : PosNum) :
n = n
theorem PosNum.succ_to_nat (n : PosNum) :
↑(PosNum.succ n) = n + 1
theorem PosNum.add_to_nat (m : PosNum) (n : PosNum) :
↑(m + n) = m + n
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 < 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 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 = Num.succ n
theorem Num.add_succ (m : Num) (n : Num) :
m + Num.succ n = Num.succ (m + n)
@[simp]
@[simp]
@[simp]
theorem Num.add_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 α] :
Num.zero = 0
@[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) :
↑(Num.succ' n) = n + 1
theorem Num.succ_to_nat (n : Num) :
↑(Num.succ n) = n + 1
@[simp]
theorem Num.cast_to_nat {α : Type u_1} [AddMonoidWithOne α] (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 (Num.cmp m 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]
@[simp]
theorem Num.of_to_nat' (n : Num) :
Num.ofNat' n = 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
  exact Nat.le_add_right _ _
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
    
    Instances For
      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} [AddGroupWithOne α] (n : Num) :
      n = n
      theorem Num.to_of_nat (n : ) :
      n = n
      @[simp]
      theorem Num.of_nat_cast {α : Type u_1} [AddMonoidWithOne α] (n : ) :
      n = n
      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 = Num.pos n
      theorem PosNum.to_nat_inj {m : PosNum} {n : PosNum} :
      m = n m = n
      @[simp]
      theorem PosNum.dvd_to_nat {m : PosNum} {n : PosNum} :
      m n m n

      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 _ _
      
      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
        
        Instances For
          @[simp]
          theorem PosNum.cast_to_num (n : PosNum) :
          n = Num.pos 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} [AddMonoidWithOne α] (m : PosNum) (n : PosNum) :
          ↑(m + n) = m + n
          @[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} :
          m = n m = n
          @[simp]
          theorem PosNum.one_le_cast {α : Type u_1} [LinearOrderedSemiring α] (n : PosNum) :
          1 n
          @[simp]
          theorem PosNum.cast_pos {α : Type u_1} [LinearOrderedSemiring α] (n : PosNum) :
          0 < n
          @[simp]
          theorem PosNum.cast_mul {α : Type u_1} [Semiring α] (m : PosNum) (n : PosNum) :
          ↑(m * n) = m * n
          @[simp]
          theorem PosNum.cmp_eq (m : PosNum) (n : PosNum) :
          @[simp]
          theorem PosNum.cast_lt {α : Type u_1} [LinearOrderedSemiring α] {m : PosNum} {n : PosNum} :
          m < n m < n
          @[simp]
          theorem PosNum.cast_le {α : Type u_1} [LinearOrderedSemiring α] {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} [AddMonoidWithOne α] (n : Num) :
          ↑(Num.succ' n) = n + 1
          theorem Num.cast_succ {α : Type u_1} [AddMonoidWithOne α] (n : Num) :
          ↑(Num.succ n) = n + 1
          @[simp]
          theorem Num.cast_add {α : Type u_1} [Semiring α] (m : Num) (n : Num) :
          ↑(m + n) = m + n
          @[simp]
          theorem Num.cast_bit0 {α : Type u_1} [Semiring α] (n : Num) :
          ↑(Num.bit0 n) = bit0 n
          @[simp]
          theorem Num.cast_bit1 {α : Type u_1} [Semiring α] (n : Num) :
          ↑(Num.bit1 n) = bit1 n
          @[simp]
          theorem Num.cast_mul {α : Type u_1} [Semiring α] (m : Num) (n : Num) :
          ↑(m * n) = m * n
          theorem Num.size_to_nat (n : Num) :
          ↑(Num.size n) = Nat.size n
          @[simp]
          theorem Num.ofNat'_eq (n : ) :
          Num.ofNat' n = n
          theorem Num.toZNum_inj {m : Num} {n : Num} :
          @[simp]
          theorem Num.cast_toZNum {α : Type u_1} [Zero α] [One α] [Add α] [Neg α] (n : Num) :
          ↑(Num.toZNum n) = n
          @[simp]
          theorem Num.cast_toZNumNeg {α : Type u_1} [AddGroup α] [One α] (n : Num) :
          ↑(Num.toZNumNeg n) = -n
          @[simp]
          theorem Num.add_toZNum (m : Num) (n : Num) :
          theorem PosNum.pred_to_nat {n : PosNum} (h : 1 < n) :
          ↑(PosNum.pred n) = Nat.pred n
          theorem Num.pred_to_nat (n : Num) :
          ↑(Num.pred n) = Nat.pred n
          theorem Num.ppred_to_nat (n : Num) :
          castNum <$> Num.ppred n = Nat.ppred n
          theorem Num.cmp_swap (m : Num) (n : Num) :
          theorem Num.cmp_eq (m : Num) (n : Num) :
          @[simp]
          theorem Num.cast_lt {α : Type u_1} [LinearOrderedSemiring α] {m : Num} {n : Num} :
          m < n m < n
          @[simp]
          theorem Num.cast_le {α : Type u_1} [LinearOrderedSemiring α] {m : Num} {n : Num} :
          m n m n
          @[simp]
          theorem Num.cast_inj {α : Type u_1} [LinearOrderedSemiring α] {m : Num} {n : Num} :
          m = n m = n
          theorem Num.lt_iff_cmp {m : Num} {n : Num} :
          theorem Num.le_iff_cmp {m : Num} {n : Num} :
          theorem Num.bitwise'_to_nat {f : NumNumNum} {g : BoolBoolBool} (p : PosNumPosNumNum) (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]
          theorem Num.lor'_to_nat (m : Num) (n : Num) :
          ↑(Num.lor m n) = Nat.lor' m n
          @[simp]
          theorem Num.land'_to_nat (m : Num) (n : Num) :
          ↑(Num.land m n) = Nat.land' m n
          @[simp]
          theorem Num.ldiff'_to_nat (m : Num) (n : Num) :
          ↑(Num.ldiff m n) = Nat.ldiff' m n
          @[simp]
          theorem Num.lxor'_to_nat (m : Num) (n : Num) :
          ↑(Num.lxor m n) = Nat.lxor' m n
          @[simp]
          theorem Num.shiftl_to_nat (m : Num) (n : ) :
          ↑(Num.shiftl m n) = m <<< n
          @[simp]
          theorem Num.shiftr_to_nat (m : Num) (n : ) :
          ↑(Num.shiftr m n) = m >>> n
          @[simp]
          theorem Num.testBit_to_nat (m : Num) (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} [AddGroup α] [One α] (n : ZNum) :
          ↑(-n) = -n
          theorem ZNum.neg_zero :
          -0 = 0
          theorem ZNum.zneg_zneg (n : ZNum) :
          - -n = n
          @[simp]
          theorem ZNum.abs_to_nat (n : ZNum) :
          ↑(ZNum.abs n) = Int.natAbs n
          @[simp]
          theorem ZNum.abs_toZNum (n : Num) :
          @[simp]
          theorem ZNum.cast_to_int {α : Type u_1} [AddGroupWithOne α] (n : ZNum) :
          n = n
          @[simp]
          theorem ZNum.cast_bit0 {α : Type u_1} [AddGroupWithOne α] (n : ZNum) :
          ↑(ZNum.bit0 n) = bit0 n
          @[simp]
          theorem ZNum.cast_bit1 {α : Type u_1} [AddGroupWithOne α] (n : ZNum) :
          ↑(ZNum.bit1 n) = bit1 n
          @[simp]
          theorem ZNum.cast_bitm1 {α : Type u_1} [AddGroupWithOne α] (n : ZNum) :
          ↑(ZNum.bitm1 n) = bit0 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 = ZNum.succ n
          theorem PosNum.cast_sub' {α : Type u_1} [AddGroupWithOne α] (m : PosNum) (n : PosNum) :
          ↑(PosNum.sub' m n) = m - n
          theorem PosNum.to_int_eq_succ_pred (n : PosNum) :
          n = ↑(PosNum.pred' n) + 1
          @[simp]
          theorem Num.cast_sub' {α : Type u_1} [AddGroupWithOne α] (m : Num) (n : Num) :
          ↑(Num.sub' m n) = m - n
          @[simp]
          theorem Num.pred_succ (n : ZNum) :
          theorem Num.ofZNum'_toNat (n : ZNum) :
          castNum <$> Num.ofZNum' n = Int.toNat' n
          @[simp]
          theorem Num.ofZNum_toNat (n : ZNum) :
          ↑(Num.ofZNum n) = Int.toNat n
          @[simp]
          theorem Num.cast_ofZNum {α : Type u_1} [AddGroupWithOne α] (n : ZNum) :
          ↑(Num.ofZNum n) = ↑(Int.toNat n)
          @[simp]
          theorem Num.sub_to_nat (m : Num) (n : Num) :
          ↑(m - n) = m - n
          @[simp]
          theorem ZNum.cast_add {α : Type u_1} [AddGroupWithOne α] (m : ZNum) (n : ZNum) :
          ↑(m + n) = m + n
          @[simp]
          theorem ZNum.cast_succ {α : Type u_1} [AddGroupWithOne α] (n : ZNum) :
          ↑(ZNum.succ n) = 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.of_to_int' (n : ZNum) :
          ZNum.ofInt' n = 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 (ZNum.cmp m 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} [LinearOrderedRing α] {m : ZNum} {n : ZNum} :
          m < n m < n
          @[simp]
          theorem ZNum.cast_le {α : Type u_1} [LinearOrderedRing α] {m : ZNum} {n : ZNum} :
          m n m n
          @[simp]
          theorem ZNum.cast_inj {α : Type u_1} [LinearOrderedRing α] {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
            exact le_add_of_nonneg_right (mul_self_nonneg _)
          
          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 _
            
            Instances For
              @[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 : ) :
              ZNum.ofInt' n = n
              @[simp]
              theorem ZNum.of_nat_toZNum (n : ) :
              Num.toZNum n = 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 : ) :
              Num.toZNumNeg n = -n
              @[simp]
              theorem ZNum.of_int_cast {α : Type u_1} [AddGroupWithOne α] (n : ) :
              n = n
              @[simp]
              theorem ZNum.of_nat_cast {α : Type u_1} [AddGroupWithOne α] (n : ) :
              n = n
              @[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 * 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
              @[simp]
              theorem PosNum.div'_to_nat (n : PosNum) (d : PosNum) :
              ↑(PosNum.div' n d) = n / d
              @[simp]
              theorem PosNum.mod'_to_nat (n : PosNum) (d : PosNum) :
              ↑(PosNum.mod' n 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 bNum.natSize (a * b) n↑(Num.gcdAux n a b) = Nat.gcd a b
              @[simp]
              theorem Num.gcd_to_nat (a : Num) (b : Num) :
              ↑(Num.gcd a b) = Nat.gcd a b
              theorem Num.dvd_iff_mod_eq_zero {m : Num} {n : Num} :
              m n n % m = 0
              instance Num.decidableDvd :
              DecidableRel fun x x_1 => x x_1
              instance PosNum.decidableDvd :
              DecidableRel fun x x_1 => x x_1
              @[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) :
              ↑(ZNum.gcd a b) = Int.gcd a b
              theorem ZNum.dvd_iff_mod_eq_zero {m : ZNum} {n : ZNum} :
              m n n % m = 0
              instance ZNum.decidableDvd :
              DecidableRel fun x x_1 => x x_1

              Cast a SNum to the corresponding integer.

              Instances For