From e993486301713f07cd3c03dae525cb3ef116ccd1 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 7 Nov 2014 08:21:42 -0800
Subject: [PATCH] refactor(library/data/num): break into pieces to reduce
 dependencies

---
 library/data/num.lean         | 150 ----------------------------------
 library/data/num/decl.lean    |  17 ++++
 library/data/num/default.lean |   6 ++
 library/data/num/ops.lean     |  72 ++++++++++++++++
 library/data/num/thms.lean    |  69 ++++++++++++++++
 library/tools/tactic.lean     |   2 +-
 tests/lean/notation7.lean     |   2 +-
 tests/lean/run/class1.lean    |   2 +-
 tests/lean/run/class2.lean    |   2 +-
 tests/lean/run/tactic26.lean  |   2 +-
 tests/lean/run/tactic28.lean  |   2 +-
 11 files changed, 170 insertions(+), 156 deletions(-)
 delete mode 100644 library/data/num.lean
 create mode 100644 library/data/num/decl.lean
 create mode 100644 library/data/num/default.lean
 create mode 100644 library/data/num/ops.lean
 create mode 100644 library/data/num/thms.lean

diff --git a/library/data/num.lean b/library/data/num.lean
deleted file mode 100644
index 892467214..000000000
--- a/library/data/num.lean
+++ /dev/null
@@ -1,150 +0,0 @@
-----------------------------------------------------------------------------------------------------
--- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
--- Released under Apache 2.0 license as described in the file LICENSE.
--- Author: Leonardo de Moura
-----------------------------------------------------------------------------------------------------
-import logic.inhabited data.bool general_notation
-open bool
-
--- pos_num and num are two auxiliary datatypes used when parsing numerals such as 13, 0, 26.
--- The parser will generate the terms (pos (bit1 (bit1 (bit0 one)))), zero, and (pos (bit0 (bit1 (bit1 one)))).
--- This representation can be coerced in whatever we want (e.g., naturals, integers, reals, etc).
-inductive pos_num : Type :=
-one  : pos_num,
-bit1 : pos_num → pos_num,
-bit0 : pos_num → pos_num
-
-definition pos_num.is_inhabited [instance] : inhabited pos_num :=
-inhabited.mk pos_num.one
-
-namespace pos_num
-  definition succ (a : pos_num) : pos_num :=
-  rec_on a (bit0 one) (λn r, bit0 r) (λn r, bit1 n)
-
-  definition is_one (a : pos_num) : bool :=
-  rec_on a tt (λn r, ff) (λn r, ff)
-
-  definition pred (a : pos_num) : pos_num :=
-  rec_on a one (λn r, bit0 n) (λn r, cond (is_one n) one (bit1 r))
-
-  definition size (a : pos_num) : pos_num :=
-  rec_on a one (λn r, succ r) (λn r, succ r)
-
-  theorem succ_not_is_one (a : pos_num) : is_one (succ a) = ff :=
-  induction_on a rfl (take n iH, rfl) (take n iH, rfl)
-
-  theorem pred.succ (a : pos_num) : pred (succ a) = a :=
-  rec_on a
-    rfl
-    (take (n : pos_num) (iH : pred (succ n) = n),
-      calc
-        pred (succ (bit1 n)) = cond ff one (bit1 (pred (succ n))) : {!succ_not_is_one}
-                       ...   = bit1 (pred (succ n))               : rfl
-                       ...   = bit1 n                             : {iH})
-    (take (n : pos_num) (iH : pred (succ n) = n), rfl)
-
-  definition add (a b : pos_num) : pos_num :=
-  rec_on a
-    succ
-    (λn f b, rec_on b
-      (succ (bit1 n))
-      (λm r, succ (bit1 (f m)))
-      (λm r, bit1 (f m)))
-    (λn f b, rec_on b
-      (bit1 n)
-      (λm r, bit1 (f m))
-      (λm r, bit0 (f m)))
-    b
-
-  notation a + b := add a b
-
-  section
-  variables (a b : pos_num)
-
-  theorem add.one_one : one + one = bit0 one :=
-  rfl
-
-  theorem add.one_bit0 : one + (bit0 a) = bit1 a :=
-  rfl
-
-  theorem add.one_bit1 : one + (bit1 a) = succ (bit1 a) :=
-  rfl
-
-  theorem add.bit0_one : (bit0 a) + one = bit1 a :=
-  rfl
-
-  theorem add.bit1_one : (bit1 a) + one = succ (bit1 a) :=
-  rfl
-
-  theorem add.bit0_bit0 : (bit0 a) + (bit0 b) = bit0 (a + b) :=
-  rfl
-
-  theorem add.bit0_bit1 : (bit0 a) + (bit1 b) = bit1 (a + b) :=
-  rfl
-
-  theorem add.bit1_bit0 : (bit1 a) + (bit0 b) = bit1 (a + b) :=
-  rfl
-
-  theorem add.bit1_bit1 : (bit1 a) + (bit1 b) = succ (bit1 (a + b)) :=
-  rfl
-  end
-
-  definition mul (a b : pos_num) : pos_num :=
-  rec_on a
-    b
-    (λn r, bit0 r + b)
-    (λn r, bit0 r)
-
-  notation a * b := mul a b
-
-  theorem mul.one_left (a : pos_num) : one * a = a :=
-  rfl
-
-  theorem mul.one_right (a : pos_num) : a * one = a :=
-  induction_on a
-    rfl
-    (take (n : pos_num) (iH : n * one = n),
-      calc bit1 n * one = bit0 (n * one) + one : rfl
-                   ...  = bit0 n + one : {iH}
-                   ...  = bit1 n       : !add.bit0_one)
-    (take (n : pos_num) (iH : n * one = n),
-      calc bit0 n * one = bit0 (n * one) : rfl
-                    ... = bit0 n         : {iH})
-end pos_num
-
-inductive num : Type :=
-zero  : num,
-pos   : pos_num → num
-
-definition num.is_inhabited [instance] : inhabited num :=
-inhabited.mk num.zero
-
-namespace num
-  open pos_num
-  definition succ (a : num) : num :=
-  rec_on a (pos one) (λp, pos (succ p))
-
-  definition pred (a : num) : num :=
-  rec_on a zero (λp, cond (is_one p) zero (pos (pred p)))
-
-  definition size (a : num) : num :=
-  rec_on a (pos one) (λp, pos (size p))
-
-  theorem pred.succ (a : num) : pred (succ a) = a :=
-  rec_on a
-    rfl
-    (λp, calc
-      pred (succ (pos p)) = pred (pos (pos_num.succ p)) : rfl
-                   ...    = cond ff zero (pos (pos_num.pred (pos_num.succ p))) : {!succ_not_is_one}
-                   ...    = pos (pos_num.pred (pos_num.succ p)) : !cond.ff
-                   ...    = pos p : {!pos_num.pred.succ})
-
-  definition add (a b : num) : num :=
-  rec_on a b (λp_a, rec_on b (pos p_a) (λp_b, pos (pos_num.add p_a p_b)))
-
-  definition mul (a b : num) : num :=
-  rec_on a zero (λp_a, rec_on b zero (λp_b, pos (pos_num.mul p_a p_b)))
-
-  notation a + b := add a b
-  notation a * b := mul a b
-end num
diff --git a/library/data/num/decl.lean b/library/data/num/decl.lean
new file mode 100644
index 000000000..e1f821d5b
--- /dev/null
+++ b/library/data/num/decl.lean
@@ -0,0 +1,17 @@
+----------------------------------------------------------------------------------------------------
+-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Author: Leonardo de Moura
+----------------------------------------------------------------------------------------------------
+
+-- pos_num and num are two auxiliary datatypes used when parsing numerals such as 13, 0, 26.
+-- The parser will generate the terms (pos (bit1 (bit1 (bit0 one)))), zero, and (pos (bit0 (bit1 (bit1 one)))).
+-- This representation can be coerced in whatever we want (e.g., naturals, integers, reals, etc).
+inductive pos_num : Type :=
+one  : pos_num,
+bit1 : pos_num → pos_num,
+bit0 : pos_num → pos_num
+
+inductive num : Type :=
+zero  : num,
+pos   : pos_num → num
diff --git a/library/data/num/default.lean b/library/data/num/default.lean
new file mode 100644
index 000000000..4fdc6da6c
--- /dev/null
+++ b/library/data/num/default.lean
@@ -0,0 +1,6 @@
+----------------------------------------------------------------------------------------------------
+-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Author: Leonardo de Moura
+----------------------------------------------------------------------------------------------------
+import data.num.decl data.num.ops data.num.thms
diff --git a/library/data/num/ops.lean b/library/data/num/ops.lean
new file mode 100644
index 000000000..b9b9bc093
--- /dev/null
+++ b/library/data/num/ops.lean
@@ -0,0 +1,72 @@
+----------------------------------------------------------------------------------------------------
+-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Author: Leonardo de Moura
+----------------------------------------------------------------------------------------------------
+import data.num.decl logic.inhabited data.bool
+open bool
+
+definition pos_num.is_inhabited [instance] : inhabited pos_num :=
+inhabited.mk pos_num.one
+
+namespace pos_num
+  definition succ (a : pos_num) : pos_num :=
+  rec_on a (bit0 one) (λn r, bit0 r) (λn r, bit1 n)
+
+  definition is_one (a : pos_num) : bool :=
+  rec_on a tt (λn r, ff) (λn r, ff)
+
+  definition pred (a : pos_num) : pos_num :=
+  rec_on a one (λn r, bit0 n) (λn r, cond (is_one n) one (bit1 r))
+
+  definition size (a : pos_num) : pos_num :=
+  rec_on a one (λn r, succ r) (λn r, succ r)
+
+  definition add (a b : pos_num) : pos_num :=
+  rec_on a
+    succ
+    (λn f b, rec_on b
+      (succ (bit1 n))
+      (λm r, succ (bit1 (f m)))
+      (λm r, bit1 (f m)))
+    (λn f b, rec_on b
+      (bit1 n)
+      (λm r, bit1 (f m))
+      (λm r, bit0 (f m)))
+    b
+
+  notation a + b := add a b
+
+  definition mul (a b : pos_num) : pos_num :=
+  rec_on a
+    b
+    (λn r, bit0 r + b)
+    (λn r, bit0 r)
+
+  notation a * b := mul a b
+
+end pos_num
+
+definition num.is_inhabited [instance] : inhabited num :=
+inhabited.mk num.zero
+
+namespace num
+  open pos_num
+  definition succ (a : num) : num :=
+  rec_on a (pos one) (λp, pos (succ p))
+
+  definition pred (a : num) : num :=
+  rec_on a zero (λp, cond (is_one p) zero (pos (pred p)))
+
+  definition size (a : num) : num :=
+  rec_on a (pos one) (λp, pos (size p))
+
+  definition add (a b : num) : num :=
+  rec_on a b (λp_a, rec_on b (pos p_a) (λp_b, pos (pos_num.add p_a p_b)))
+
+  definition mul (a b : num) : num :=
+  rec_on a zero (λp_a, rec_on b zero (λp_b, pos (pos_num.mul p_a p_b)))
+
+  notation a + b := add a b
+  notation a * b := mul a b
+end num
diff --git a/library/data/num/thms.lean b/library/data/num/thms.lean
new file mode 100644
index 000000000..087a62a16
--- /dev/null
+++ b/library/data/num/thms.lean
@@ -0,0 +1,69 @@
+----------------------------------------------------------------------------------------------------
+-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Author: Leonardo de Moura
+----------------------------------------------------------------------------------------------------
+import data.num.ops logic.eq
+open bool
+
+namespace pos_num
+  theorem succ_not_is_one (a : pos_num) : is_one (succ a) = ff :=
+  induction_on a rfl (take n iH, rfl) (take n iH, rfl)
+
+  theorem pred.succ (a : pos_num) : pred (succ a) = a :=
+  rec_on a
+    rfl
+    (take (n : pos_num) (iH : pred (succ n) = n),
+      calc
+        pred (succ (bit1 n)) = cond (is_one (succ n)) one (bit1 (pred (succ n))) : rfl
+                       ...   = cond ff one (bit1 (pred (succ n)))                : succ_not_is_one
+                       ...   = bit1 (pred (succ n))                              : rfl
+                       ...   = bit1 n                                            : iH)
+    (take (n : pos_num) (iH : pred (succ n) = n), rfl)
+
+  section
+  variables (a b : pos_num)
+
+  theorem add.one_one : one + one = bit0 one :=
+  rfl
+
+  theorem add.one_bit0 : one + (bit0 a) = bit1 a :=
+  rfl
+
+  theorem add.one_bit1 : one + (bit1 a) = succ (bit1 a) :=
+  rfl
+
+  theorem add.bit0_one : (bit0 a) + one = bit1 a :=
+  rfl
+
+  theorem add.bit1_one : (bit1 a) + one = succ (bit1 a) :=
+  rfl
+
+  theorem add.bit0_bit0 : (bit0 a) + (bit0 b) = bit0 (a + b) :=
+  rfl
+
+  theorem add.bit0_bit1 : (bit0 a) + (bit1 b) = bit1 (a + b) :=
+  rfl
+
+  theorem add.bit1_bit0 : (bit1 a) + (bit0 b) = bit1 (a + b) :=
+  rfl
+
+  theorem add.bit1_bit1 : (bit1 a) + (bit1 b) = succ (bit1 (a + b)) :=
+  rfl
+  end
+
+  theorem mul.one_left (a : pos_num) : one * a = a :=
+  rfl
+
+  theorem mul.one_right (a : pos_num) : a * one = a :=
+  induction_on a
+    rfl
+    (take (n : pos_num) (iH : n * one = n),
+      calc bit1 n * one = bit0 (n * one) + one : rfl
+                   ...  = bit0 n + one         : iH
+                   ...  = bit1 n               : add.bit0_one)
+    (take (n : pos_num) (iH : n * one = n),
+      calc bit0 n * one = bit0 (n * one)       : rfl
+                    ... = bit0 n               : iH)
+
+end pos_num
diff --git a/library/tools/tactic.lean b/library/tools/tactic.lean
index 5742fe5e0..4641999db 100644
--- a/library/tools/tactic.lean
+++ b/library/tools/tactic.lean
@@ -4,7 +4,7 @@
 -- Author: Leonardo de Moura
 ----------------------------------------------------------------------------------------------------
 
-import data.string data.num
+import data.string data.num.decl
 -- This is just a trick to embed the 'tactic language' as a
 -- Lean expression. We should view 'tactic' as automation
 -- that when execute produces a term.
diff --git a/tests/lean/notation7.lean b/tests/lean/notation7.lean
index 8c2af5a1b..9792c8c3c 100644
--- a/tests/lean/notation7.lean
+++ b/tests/lean/notation7.lean
@@ -1,4 +1,4 @@
-import logic
+import logic data.num
 open num
 
 constant f : num → num
diff --git a/tests/lean/run/class1.lean b/tests/lean/run/class1.lean
index 2edc27d8f..16b5a3ebe 100644
--- a/tests/lean/run/class1.lean
+++ b/tests/lean/run/class1.lean
@@ -1,4 +1,4 @@
-import logic data.prod
+import logic data.prod data.num
 open prod inhabited
 
 definition H : inhabited (Prop × num × (num → num)) := _
diff --git a/tests/lean/run/class2.lean b/tests/lean/run/class2.lean
index 302ce888e..434df42a9 100644
--- a/tests/lean/run/class2.lean
+++ b/tests/lean/run/class2.lean
@@ -1,4 +1,4 @@
-import logic data.prod
+import logic data.prod data.num
 open prod nonempty inhabited
 
 theorem H {A B : Type} (H1 : inhabited A) : inhabited (Prop × A × (B → num))
diff --git a/tests/lean/run/tactic26.lean b/tests/lean/run/tactic26.lean
index ca254f9d6..3530578b5 100644
--- a/tests/lean/run/tactic26.lean
+++ b/tests/lean/run/tactic26.lean
@@ -1,4 +1,4 @@
-import logic
+import logic data.num
 open tactic inhabited
 
 namespace foo
diff --git a/tests/lean/run/tactic28.lean b/tests/lean/run/tactic28.lean
index a68d58e77..5c70900a5 100644
--- a/tests/lean/run/tactic28.lean
+++ b/tests/lean/run/tactic28.lean
@@ -1,4 +1,4 @@
-import logic
+import logic data.num
 open tactic inhabited
 
 namespace foo