feat(data/num/basic): add div,mod,gcd for num,znum

algebra/ordered_ring.lean

@@ -27,6 +27,13 @@ variable [linear_ordered_semiring α]
 @[simp] lemma mul_lt_mul_right {a b c : α} (h : 0 < c) : a * c < b * c ↔ a < b :=
 ⟨λ h', lt_of_mul_lt_mul_right h' (le_of_lt h), λ h', mul_lt_mul_of_pos_right h' h⟩
 
+lemma mul_lt_mul'' {a b c d : α} (h1 : a < c) (h2 : b < d) (h3 : 0 ≤ a) (h4 : 0 ≤ b) :
+       a * b < c * d :=
+(lt_or_eq_of_le h4).elim
+  (λ b0, mul_lt_mul h1 (le_of_lt h2) b0 (le_trans h3 (le_of_lt h1)))
+  (λ b0, by rw [← b0, mul_zero]; exact
+    mul_pos (lt_of_le_of_lt h3 h1) (lt_of_le_of_lt h4 h2))
+
 lemma le_mul_iff_one_le_left {a b : α} (hb : b > 0) : b ≤ a * b ↔ 1 ≤ a :=
 suffices 1 * b ≤ a * b ↔ 1 ≤ a, by rwa one_mul at this,
 mul_le_mul_right hb

data/int/basic.lean

@@ -96,9 +96,11 @@ end
 
 /- /  -/
 
-theorem of_nat_div (m n : nat) : of_nat (m / n) = (of_nat m) / (of_nat n) := rfl
+@[simp] theorem of_nat_div (m n : ℕ) : of_nat (m / n) = (of_nat m) / (of_nat n) := rfl
 
-theorem neg_succ_of_nat_div (m : nat) {b : ℤ} (H : b > 0) :
+@[simp] theorem coe_nat_div (m n : ℕ) : ((m / n : ℕ) : ℤ) = m / n := rfl
+
+theorem neg_succ_of_nat_div (m : ℕ) {b : ℤ} (H : b > 0) :
   -[1+m] / b = -(m / b + 1) :=
 match b, eq_succ_of_zero_lt H with ._, ⟨n, rfl⟩ := rfl end
 
@@ -638,6 +640,14 @@ by rw [to_nat_eq_max]; apply le_max_left
 by rw [(coe_nat_le_coe_nat_iff _ _).symm, to_nat_eq_max, max_le_iff];
    exact and_iff_left (coe_zero_le _)
 
+def to_nat' : ℤ → option ℕ
+| (n : ℕ) := some n
+| -[1+ n] := none
+
+theorem mem_to_nat' : ∀ (a : ℤ) (n : ℕ), n ∈ to_nat' a ↔ a = n
+| (m : ℕ) n := option.some_inj.trans coe_nat_inj'.symm
+| -[1+ m] n := by split; intro h; cases h
+
 /- bitwise ops -/
 
 @[simp] lemma bodd_zero : bodd 0 = ff := rfl

data/num/basic.lean

@@ -109,6 +109,11 @@ namespace pos_num
   | (bit0 n) := succ (size n)
   | (bit1 n) := succ (size n)
 
+  def nat_size : pos_num → nat
+  | 1        := 1
+  | (bit0 n) := nat.succ (nat_size n)
+  | (bit1 n) := nat.succ (nat_size n)
+
   protected def mul (a : pos_num) : pos_num → pos_num
   | 1        := a
   | (bit0 b) := bit0 (mul b)
@@ -158,6 +163,9 @@ section
   @[priority 0] instance pos_num_coe : has_coe pos_num α := ⟨cast_pos_num⟩
 
   @[priority 0] instance num_nat_coe : has_coe num α := ⟨cast_num⟩
+
+  instance : has_repr pos_num := ⟨λ n, repr (n : ℕ)⟩
+  instance : has_repr num := ⟨λ n, repr (n : ℕ)⟩
 end
 
 namespace num
@@ -190,6 +198,10 @@ namespace num
   | 0       := 0
   | (pos n) := pos (pos_num.size n)
 
+  def nat_size : num → nat
+  | 0       := 0
+  | (pos n) := pos_num.nat_size n
+
   protected def mul : num → num → num
   | 0       _       := 0
   | _       0       := 0
@@ -233,6 +245,11 @@ namespace znum
 
   instance : has_neg znum := ⟨zneg⟩
 
+  def abs : znum → num
+  | 0       := 0
+  | (pos a) := num.pos a
+  | (neg a) := num.pos a
+
   def succ : znum → znum
   | 0       := 1
   | (pos a) := pos (pos_num.succ a)
@@ -297,6 +314,12 @@ namespace num
   | 0       := 0
   | (pos p) := p.pred'
 
+  def div2 : num → num
+  | 0 := 0
+  | 1 := 0
+  | (pos (pos_num.bit0 p)) := pos p
+  | (pos (pos_num.bit1 p)) := pos p
+
   def of_znum' : znum → option num
   | 0            := some 0
   | (znum.pos p) := some (pos p)
@@ -365,6 +388,107 @@ namespace znum
 
 end znum
 
+namespace pos_num
+
+  def divmod_aux (d : pos_num) (q r : num) : num × num :=
+  match num.of_znum' (num.sub' r (num.pos d)) with
+  | some r' := (num.bit1 q, r')
+  | none    := (num.bit0 q, r)
+  end
+
+  def divmod (d : pos_num) : pos_num → num × num
+  | (bit0 n) := let (q, r₁) := divmod n in
+    divmod_aux d q (num.bit0 r₁)
+  | (bit1 n) := let (q, r₁) := divmod n in
+    divmod_aux d q (num.bit1 r₁)
+  | 1        := divmod_aux d 0 1
+
+  def div' (n d : pos_num) : num := (divmod d n).1
+
+  def mod' (n d : pos_num) : num := (divmod d n).2
+
+  def sqrt_aux1 (b : pos_num) (r n : num) : num × num :=
+  match num.of_znum' (n.sub' (r + num.pos b)) with
+  | some n' := (r.div2 + num.pos b, n')
+  | none := (r.div2, n)
+  end
+
+  def sqrt_aux : pos_num → num → num → num
+  | b@(bit0 b') r n := let (r', n') := sqrt_aux1 b r n in sqrt_aux b' r' n'
+  | b@(bit1 b') r n := let (r', n') := sqrt_aux1 b r n in sqrt_aux b' r' n'
+  | 1           r n := (sqrt_aux1 1 r n).1
+/-
+
+def sqrt_aux : ℕ → ℕ → ℕ → ℕ
+| b r n := if b0 : b = 0 then r else
+  let b' := shiftr b 2 in
+  have b' < b, from sqrt_aux_dec b0,
+  match (n - (r + b : ℕ) : ℤ) with
+  | (n' : ℕ) := sqrt_aux b' (div2 r + b) n'
+  | _ := sqrt_aux b' (div2 r) n
+  end
+
+/-- `sqrt n` is the square root of a natural number `n`. If `n` is not a
+  perfect square, it returns the largest `k:ℕ` such that `k*k ≤ n`. -/
+def sqrt (n : ℕ) : ℕ :=
+match size n with
+| 0      := 0
+| succ s := sqrt_aux (shiftl 1 (bit0 (div2 s))) 0 n
+end
+-/
+
+end pos_num
+
+namespace num
+
+  def div : num → num → num
+  | 0       _       := 0
+  | _       0       := 0
+  | (pos n) (pos d) := pos_num.div' n d
+
+  def mod : num → num → num
+  | 0       _       := 0
+  | n       0       := n
+  | (pos n) (pos d) := pos_num.mod' n d
+
+  instance : has_div num := ⟨num.div⟩
+  instance : has_mod num := ⟨num.mod⟩
+
+  def gcd_aux : nat → num → num → num
+  | 0            a b := b
+  | (nat.succ n) 0 b := b
+  | (nat.succ n) a b := gcd_aux n (b % a) a
+
+  def gcd (a b : num) : num :=
+  if a ≤ b then
+    gcd_aux (a.nat_size + b.nat_size) a b
+  else
+    gcd_aux (b.nat_size + a.nat_size) b a
+
+end num
+
+namespace znum
+
+  def div : znum → znum → znum
+  | 0       _       := 0
+  | _       0       := 0
+  | (pos n) (pos d) := num.to_znum (pos_num.div' n d)
+  | (pos n) (neg d) := num.to_znum_neg (pos_num.div' n d)
+  | (neg n) (pos d) := neg (pos_num.pred' n / num.pos d).succ'
+  | (neg n) (neg d) := pos (pos_num.pred' n / num.pos d).succ'
+
+  def mod : znum → znum → znum
+  | 0       d := 0
+  | (pos n) d := num.to_znum (num.pos n % d.abs)
+  | (neg n) d := d.abs.sub' (pos_num.pred' n % d.abs).succ
+
+  instance : has_div znum := ⟨znum.div⟩
+  instance : has_mod znum := ⟨znum.mod⟩
+
+  def gcd (a b : znum) : num := a.abs.gcd b.abs
+
+end znum
+
 section
   variables {α : Type*} [has_zero α] [has_one α] [has_add α] [has_neg α]
 
@@ -374,6 +498,8 @@ section
   | (znum.neg p) := -p
 
   @[priority 0] instance znum_coe : has_coe znum α := ⟨cast_znum⟩
+
+  instance : has_repr znum := ⟨λ n, repr (n : ℤ)⟩
 end
 
 /- The snum representation uses a bit string, essentially a list of 0 (ff) and 1 (tt) bits,