lint(data/num/*): add docs and remove some [has_zero] requirements (#…

…4604)

src/data/num/basic.lean

@@ -160,10 +160,10 @@ namespace pos_num
 end pos_num
 
 section
-  variables {α : Type*} [has_zero α] [has_one α] [has_add α]
+  variables {α : Type*} [has_one α] [has_add α]
 
   /--
-  `cast_pos_num` casts a `pos_num` into any type which has `0`, `1` and `+`.
+  `cast_pos_num` casts a `pos_num` into any type which has `1` and `+`.
   -/
   def cast_pos_num : pos_num → α
   | 1                := 1
@@ -173,15 +173,15 @@ section
   /--
   `cast_num` casts a `num` into any type which has `0`, `1` and `+`.
   -/
-  def cast_num : num → α
+  def cast_num [z : has_zero α] : num → α
   | 0           := 0
   | (num.pos p) := cast_pos_num p
 
   -- see Note [coercion into rings]
   @[priority 900] instance pos_num_coe : has_coe_t pos_num α := ⟨cast_pos_num⟩
 
   -- see Note [coercion into rings]
-  @[priority 900] instance num_nat_coe : has_coe_t num α := ⟨cast_num⟩
+  @[priority 900] instance num_nat_coe [z : has_zero α] : has_coe_t num α := ⟨cast_num⟩
 
   instance : has_repr pos_num := ⟨λ n, repr (n : ℕ)⟩
   instance : has_repr num := ⟨λ n, repr (n : ℕ)⟩
@@ -525,6 +525,7 @@ end znum
 
 namespace pos_num
 
+  /-- Auxiliary definition for `pos_num.divmod`. -/
   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')
@@ -551,16 +552,18 @@ namespace pos_num
   -/
   def mod' (n d : pos_num) : num := (divmod d n).2
 
-  def sqrt_aux1 (b : pos_num) (r n : num) : num × num :=
+  /-
+  private 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
+  private 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 : ℕ → ℕ → ℕ → ℕ
@@ -603,6 +606,7 @@ namespace num
   instance : has_div num := ⟨num.div⟩
   instance : has_mod num := ⟨num.mod⟩
 
+  /-- Auxiliary definition for `num.gcd`. -/
   def gcd_aux : nat → num → num → num
   | 0            a b := b
   | (nat.succ n) 0 b := b

src/data/num/bitwise.lean

@@ -18,6 +18,7 @@ import data.bitvec.core
 
 namespace pos_num
 
+  /-- Bitwise "or" for `pos_num`. -/
   def lor : pos_num → pos_num → pos_num
   | 1        (bit0 q) := bit1 q
   | 1        q        := q
@@ -28,6 +29,7 @@ namespace pos_num
   | (bit1 p) (bit0 q) := bit1 (lor p q)
   | (bit1 p) (bit1 q) := bit1 (lor p q)
 
+  /-- Bitwise "and" for `pos_num`. -/
   def land : pos_num → pos_num → num
   | 1        (bit0 q) := 0
   | 1        _        := 1
@@ -38,6 +40,14 @@ namespace pos_num
   | (bit1 p) (bit0 q) := num.bit0 (land p q)
   | (bit1 p) (bit1 q) := num.bit1 (land p q)
 
+  /-- Bitwise `λ a b, a && !b` for `pos_num`. For example, `ldiff 5 9 = 4`:
+
+     101
+    1001
+    ----
+     100
+
+  -/
   def ldiff : pos_num → pos_num → num
   | 1        (bit0 q) := 1
   | 1        _        := 0
@@ -48,6 +58,7 @@ namespace pos_num
   | (bit1 p) (bit0 q) := num.bit1 (ldiff p q)
   | (bit1 p) (bit1 q) := num.bit0 (ldiff p q)
 
+  /-- Bitwise "xor" for `pos_num`. -/
   def lxor : pos_num → pos_num → num
   | 1        1        := 0
   | 1        (bit0 q) := num.pos (bit1 q)
@@ -59,6 +70,8 @@ namespace pos_num
   | (bit1 p) (bit0 q) := num.bit1 (lxor p q)
   | (bit1 p) (bit1 q) := num.bit0 (lxor p q)
 
+  /-- `a.test_bit n` is `tt` iff the `n`-th bit (starting from the LSB) in the binary representation
+      of `a` is active. If the size of `a` is less than `n`, this evaluates to `ff`. -/
   def test_bit : pos_num → nat → bool
   | 1        0     := tt
   | 1        (n+1) := ff
@@ -67,15 +80,18 @@ namespace pos_num
   | (bit1 p) 0     := tt
   | (bit1 p) (n+1) := test_bit p n
 
+  /-- `n.one_bits 0` is the list of indices of active bits in the binary representation of `n`. -/
   def one_bits : pos_num → nat → list nat
   | 1        d := [d]
   | (bit0 p) d := one_bits p (d+1)
   | (bit1 p) d := d :: one_bits p (d+1)
 
+  /-- Left-shift the binary representation of a `pos_num`. -/
   def shiftl (p : pos_num) : nat → pos_num
   | 0     := p
   | (n+1) := bit0 (shiftl n)
 
+  /-- Right-shift the binary representation of a `pos_num`. -/
   def shiftr : pos_num → nat → num
   | p        0     := num.pos p
   | 1        (n+1) := 0
@@ -86,49 +102,67 @@ end pos_num
 
 namespace num
 
+  /-- Bitwise "or" for `num`. -/
   def lor : num → num → num
   | 0       q       := q
   | p       0       := p
   | (pos p) (pos q) := pos (p.lor q)
 
+  /-- Bitwise "and" for `num`. -/
   def land : num → num → num
   | 0       q       := 0
   | p       0       := 0
   | (pos p) (pos q) := p.land q
 
+  /-- Bitwise `λ a b, a && !b` for `num`. For example, `ldiff 5 9 = 4`:
+
+     101
+    1001
+    ----
+     100
+
+  -/
   def ldiff : num → num → num
   | 0       q       := 0
   | p       0       := p
   | (pos p) (pos q) := p.ldiff q
 
+  /-- Bitwise "xor" for `num`. -/
   def lxor : num → num → num
   | 0       q       := q
   | p       0       := p
   | (pos p) (pos q) := p.lxor q
 
+  /-- Left-shift the binary representation of a `num`. -/
   def shiftl : num → nat → num
   | 0       n := 0
   | (pos p) n := pos (p.shiftl n)
 
+  /-- Right-shift the binary representation of a `pos_num`. -/
   def shiftr : num → nat → num
   | 0       n := 0
   | (pos p) n := p.shiftr n
 
+  /-- `a.test_bit n` is `tt` iff the `n`-th bit (starting from the LSB) in the binary representation
+      of `a` is active. If the size of `a` is less than `n`, this evaluates to `ff`. -/
   def test_bit : num → nat → bool
   | 0       n := ff
   | (pos p) n := p.test_bit n
 
+  /-- `n.one_bits` is the list of indices of active bits in the binary representation of `n`. -/
   def one_bits : num → list nat
   | 0       := []
   | (pos p) := p.one_bits 0
 
 end num
 
-/-- See `snum`. -/
+/-- This is a nonzero (and "non minus one") version of `snum`.
+    See the documentation of `snum` for more details. -/
 @[derive has_reflect, derive decidable_eq]
 inductive nzsnum : Type
 | msb : bool → nzsnum
 | bit : bool → nzsnum → nzsnum
+
 /-- Alternative representation of integers using a sign bit at the end.
   The convention on sign here is to have the argument to `msb` denote
   the sign of the MSB itself, with all higher bits set to the negation
@@ -161,22 +195,30 @@ and the negation of the MSB is sign-extended to all higher bits.
 namespace nzsnum
   notation a :: b := bit a b
 
+  /-- Sign of a `nzsnum`. -/
   def sign : nzsnum → bool
   | (msb b) := bnot b
   | (b :: p) := sign p
 
+  /-- Bitwise `not` for `nzsnum`. -/
   @[pattern] def not : nzsnum → nzsnum
   | (msb b) := msb (bnot b)
   | (b :: p) := bnot b :: not p
   prefix ~ := not
 
+  /-- Add an inactive bit at the end of a `nzsnum`. This mimics `pos_num.bit0`. -/
   def bit0 : nzsnum → nzsnum := bit ff
+
+  /-- Add an active bit at the end of a `nzsnum`. This mimics `pos_num.bit1`. -/
   def bit1 : nzsnum → nzsnum := bit tt
 
+  /-- The `head` of a `nzsnum` is the boolean value of its LSB. -/
   def head : nzsnum → bool
   | (msb b)  := b
   | (b :: p) := b
 
+  /-- The `tail` of a `nzsnum` is the `snum` obtained by removing the LSB.
+      Edge cases: `tail 1 = 0` and `tail (-2) = -1`. -/
   def tail : nzsnum → snum
   | (msb b)  := snum.zero (bnot b)
   | (b :: p) := p
@@ -186,22 +228,28 @@ end nzsnum
 namespace snum
   open nzsnum
 
+  /-- Sign of a `snum`. -/
   def sign : snum → bool
   | (zero z) := z
   | (nz p)   := p.sign
 
+  /-- Bitwise `not` for `snum`. -/
   @[pattern] def not : snum → snum
   | (zero z) := zero (bnot z)
   | (nz p)   := ~p
   prefix ~ := not
 
+  /-- Add a bit at the end of a `snum`. This mimics `nzsnum.bit`. -/
   @[pattern] def bit : bool → snum → snum
   | b (zero z) := if b = z then zero b else msb b
   | b (nz p)   := p.bit b
 
   notation a :: b := bit a b
 
+  /-- Add an inactive bit at the end of a `snum`. This mimics `znum.bit0`. -/
   def bit0 : snum → snum := bit ff
+
+  /-- Add an active bit at the end of a `snum`. This mimics `znum.bit1`. -/
   def bit1 : snum → snum := bit tt
 
   theorem bit_zero (b) : b :: zero b = zero b := by cases b; refl
@@ -213,6 +261,8 @@ end snum
 namespace nzsnum
   open snum
 
+  /-- A dependent induction principle for `nzsnum`, with base cases
+      `0 : snum` and `(-1) : snum`. -/
   def drec' {C : snum → Sort*} (z : Π b, C (snum.zero b))
     (s : Π b p, C p → C (b :: p)) : Π p : nzsnum, C p
   | (msb b)  := by rw ←bit_one; exact s b (snum.zero (bnot b)) (z (bnot b))
@@ -222,37 +272,48 @@ end nzsnum
 namespace snum
   open nzsnum
 
+  /-- The `head` of a `snum` is the boolean value of its LSB. -/
   def head : snum → bool
   | (zero z) := z
   | (nz p)   := p.head
 
+  /-- The `tail` of a `snum` is obtained by removing the LSB.
+      Edge cases: `tail 1 = 0`, `tail (-2) = -1`, `tail 0 = 0` and `tail (-1) = -1`. -/
   def tail : snum → snum
   | (zero z) := zero z
   | (nz p)   := p.tail
 
+  /-- A dependent induction principle for `snum` which avoids relying on `nzsnum`. -/
   def drec' {C : snum → Sort*} (z : Π b, C (snum.zero b))
     (s : Π b p, C p → C (b :: p)) : Π p, C p
   | (zero b) := z b
   | (nz p)   := p.drec' z s
 
+  /-- An induction principle for `snum` which avoids relying on `nzsnum`. -/
   def rec' {α} (z : bool → α) (s : bool → snum → α → α) : snum → α :=
   drec' z s
 
+  /-- `snum.test_bit n a` is `tt` iff the `n`-th bit (starting from the LSB) of `a` is active.
+      If the size of `a` is less than `n`, this evaluates to `ff`. -/
   def test_bit : nat → snum → bool
   | 0     p := head p
   | (n+1) p := test_bit n (tail p)
 
+  /-- The successor of a `snum` (i.e. the operation adding one). -/
   def succ : snum → snum :=
   rec' (λ b, cond b 0 1) (λb p succp, cond b (ff :: succp) (tt :: p))
 
+  /-- The predecessor of a `snum` (i.e. the operation of removing one). -/
   def pred : snum → snum :=
   rec' (λ b, cond b (~1) ~0) (λb p predp, cond b (ff :: p) (tt :: predp))
 
+  /-- The opposite of a `snum`. -/
   protected def neg (n : snum) : snum := succ ~n
 
   instance : has_neg snum := ⟨snum.neg⟩
 
-  -- First bit is 0 or 1 (`tt`), second bit is 0 or -1 (`tt`)
+  /-- `snum.czadd a b n` is `n + a - b` (where `a` and `b` should be read as either 0 or 1).
+      This is useful to implement the carry system in `cadd`. -/
   def czadd : bool → bool → snum → snum
   | ff ff p := p
   | ff tt p := pred p
@@ -263,6 +324,7 @@ end snum
 
 namespace snum
 
+/-- `a.bits n` is the vector of the `n` first bits of `a` (starting from the LSB). -/
 def bits : snum → Π n, vector bool n
 | p 0     := vector.nil
 | p (n+1) := head p ::ᵥ bits (tail p) n
@@ -272,14 +334,17 @@ rec' (λ a p c, czadd c a p) $ λa p IH,
 rec' (λb c, czadd c b (a :: p)) $ λb q _ c,
 bitvec.xor3 a b c :: IH q (bitvec.carry a b c)
 
+/-- Add two `snum`s. -/
 protected def add (a b : snum) : snum := cadd a b ff
 
 instance : has_add snum := ⟨snum.add⟩
 
+/-- Substract two `snum`s. -/
 protected def sub (a b : snum) : snum := a + -b
 
 instance : has_sub snum := ⟨snum.sub⟩
 
+/-- Multiply two `snum`s. -/
 protected def mul (a : snum) : snum → snum :=
 rec' (λ b, cond b (-a) 0) $ λb q IH,
 cond b (bit0 IH + a) (bit0 IH)