feat(library/init/num): define sub and le for binary numerals

library/init/num.lean

@@ -45,6 +45,28 @@ namespace pos_num
 
   notation a * b := mul a b
 
+  definition lt (a b : pos_num) : bool :=
+  pos_num.rec_on a
+    (λ b, pos_num.cases_on b
+      ff
+      (λm, tt)
+      (λm, tt))
+    (λn f b, pos_num.cases_on b
+      ff
+      (λm, f m)
+      (λm, f m))
+    (λn f b, pos_num.cases_on b
+      ff
+      (λm, f (succ m))
+      (λm, f m))
+    b
+
+  definition le (a b : pos_num) : bool :=
+  lt a (succ b)
+
+  definition equal (a b : pos_num) : bool :=
+  le a b && le b a
+
 end pos_num
 
 definition num.is_inhabited [instance] : inhabited num :=
@@ -60,11 +82,39 @@ namespace num
   num.rec_on a (pos one) (λp, pos (size p))
 
   definition add (a b : num) : num :=
-  num.rec_on a b (λp_a, num.rec_on b (pos p_a) (λp_b, pos (pos_num.add p_a p_b)))
+  num.rec_on a b (λpa, num.rec_on b (pos pa) (λpb, pos (pos_num.add pa pb)))
 
   definition mul (a b : num) : num :=
-  num.rec_on a zero (λp_a, num.rec_on b zero (λp_b, pos (pos_num.mul p_a p_b)))
+  num.rec_on a zero (λpa, num.rec_on b zero (λpb, pos (pos_num.mul pa pb)))
 
   notation a + b := add a b
   notation a * b := mul a b
+
+  definition le (a b : num) : bool :=
+  num.rec_on a tt (λpa, num.rec_on b ff (λpb, pos_num.le pa pb))
+
+  private definition psub (a b : pos_num) : num :=
+  pos_num.rec_on a
+    (λb, zero)
+    (λn f b,
+      cond (pos_num.le (bit1 n) b)
+        zero
+        (pos_num.cases_on b
+           (pos (bit0 n))
+           (λm, 2 * f m)
+           (λm, 2 * f m + 1)))
+    (λn f b,
+      cond (pos_num.le (bit0 n) b)
+        zero
+        (pos_num.cases_on b
+           (pos (pos_num.pred (bit0 n)))
+           (λm, pred (2 * f m))
+           (λm, 2 * f m)))
+    b
+
+  definition sub (a b : num) : num :=
+  num.rec_on a zero (λpa, num.rec_on b a (λpb, psub pa pb))
+
+  notation a ≤ b := le a b
+  notation a - b := sub a b
 end num

tests/lean/run/num_sub.lean

@@ -0,0 +1,83 @@
+open num bool
+
+example : le 0 0 = tt := rfl
+example : le 0 1 = tt := rfl
+example : le 0 2 = tt := rfl
+example : le 0 3 = tt := rfl
+
+example : le 1 0 = ff := rfl
+example : le 1 1 = tt := rfl
+example : le 1 2 = tt := rfl
+example : le 1 3 = tt := rfl
+
+example : le 2 0 = ff := rfl
+example : le 2 1 = ff := rfl
+example : le 2 2 = tt := rfl
+example : le 2 3 = tt := rfl
+example : le 2 4 = tt := rfl
+example : le 2 5 = tt := rfl
+
+example : le 3 0 = ff := rfl
+example : le 3 1 = ff := rfl
+example : le 3 2 = ff := rfl
+example : le 3 3 = tt := rfl
+example : le 3 4 = tt := rfl
+example : le 3 5 = tt := rfl
+
+example : le 4 0 = ff := rfl
+example : le 4 1 = ff := rfl
+example : le 4 2 = ff := rfl
+example : le 4 3 = ff := rfl
+example : le 4 4 = tt := rfl
+example : le 4 5 = tt := rfl
+
+example : le 5 0 = ff := rfl
+example : le 5 1 = ff := rfl
+example : le 5 2 = ff := rfl
+example : le 5 3 = ff := rfl
+example : le 5 4 = ff := rfl
+example : le 5 5 = tt := rfl
+example : le 5 6 = tt := rfl
+
+example : 0 - 0 = 0 := rfl
+example : 0 - 1 = 0 := rfl
+example : 0 - 2 = 0 := rfl
+example : 0 - 3 = 0 := rfl
+
+example : 1 - 0 = 1 := rfl
+example : 1 - 1 = 0 := rfl
+example : 1 - 2 = 0 := rfl
+example : 1 - 3 = 0 := rfl
+
+example : 2 - 0 = 2 := rfl
+example : 2 - 1 = 1 := rfl
+example : 2 - 2 = 0 := rfl
+example : 2 - 3 = 0 := rfl
+example : 2 - 4 = 0 := rfl
+
+example : 3 - 0 = 3 := rfl
+example : 3 - 1 = 2 := rfl
+example : 3 - 2 = 1 := rfl
+example : 3 - 3 = 0 := rfl
+example : 3 - 4 = 0 := rfl
+example : 3 - 5 = 0 := rfl
+
+example : 4 - 0 = 4 := rfl
+example : 4 - 1 = 3 := rfl
+example : 4 - 2 = 2 := rfl
+example : 4 - 3 = 1 := rfl
+example : 4 - 4 = 0 := rfl
+example : 4 - 5 = 0 := rfl
+
+example : 5 - 0 = 5 := rfl
+example : 5 - 1 = 4 := rfl
+example : 5 - 2 = 3 := rfl
+example : 5 - 3 = 2 := rfl
+example : 5 - 4 = 1 := rfl
+example : 5 - 5 = 0 := rfl
+
+example : 11 - 5 = 6 := rfl
+example : 5 - 11 = 0 := rfl
+example : 12 - 7 = 5 := rfl
+example : 120 - 12 = 108 := rfl
+example : 111 - 11 = 100 := rfl