From 92d76c22a59087cdcacf8f3adbaa70dfdf982cda Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Sun, 28 May 2017 02:32:10 -0400
Subject: [PATCH] feat(data/pnat): positive natural numbers

---
 library/data/hash_map.lean |  5 +----
 library/data/pnat.lean     | 44 ++++++++++++++++++++++++++++++++++++++
 2 files changed, 45 insertions(+), 4 deletions(-)
 create mode 100644 library/data/pnat.lean

diff --git a/library/data/hash_map.lean b/library/data/hash_map.lean
index 0af977de46..ac573874e7 100644
--- a/library/data/hash_map.lean
+++ b/library/data/hash_map.lean
@@ -3,13 +3,10 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Mario Carneiro
 -/
-import data.list.set data.list.comb init.data.array
+import data.list.set data.list.comb init.data.array data.pnat
 
 universes u v w
 
-def pnat := {n : ℕ // n > 0}
-notation `ℕ+` := pnat
-
 def bucket_array (α : Type u) (β : α → Type v) (n : ℕ+) :=
 array (list Σ a, β a) n.1
 
diff --git a/library/data/pnat.lean b/library/data/pnat.lean
new file mode 100644
index 0000000000..6167a84d43
--- /dev/null
+++ b/library/data/pnat.lean
@@ -0,0 +1,44 @@
+/-
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Mario Carneiro
+-/
+
+def pnat := {n : ℕ // n > 0}
+notation `ℕ+` := pnat
+
+instance coe_pnat_nat : has_coe ℕ+ ℕ := ⟨subtype.val⟩
+
+meta def exact_dec_trivial : tactic unit := `[exact dec_trivial]
+
+namespace nat
+
+  def to_pnat (n : ℕ) (h : n > 0 . exact_dec_trivial) : ℕ+ := ⟨n, h⟩
+
+  def succ_pnat (n : ℕ) : ℕ+ := ⟨succ n, succ_pos n⟩
+
+  def to_pnat' (n : ℕ) : ℕ+ := succ_pnat (pred n)
+end nat
+
+instance coe_nat_pnat : has_coe ℕ ℕ+ := ⟨nat.to_pnat'⟩
+
+namespace pnat
+  open nat
+
+  instance : has_one ℕ+ := ⟨succ_pnat 0⟩
+
+  protected def add : ℕ+ → ℕ+ → ℕ+
+  | ⟨m, m0⟩ ⟨n, n0⟩ := ⟨m + n, add_pos m0 n0⟩
+
+  instance : has_add ℕ+ := ⟨pnat.add⟩
+
+  protected def mul : ℕ+ → ℕ+ → ℕ+
+  | ⟨m, m0⟩ ⟨n, n0⟩ := ⟨m * n, mul_pos m0 n0⟩
+
+  instance : has_mul ℕ+ := ⟨pnat.mul⟩
+
+  @[simp] theorem to_pnat'_val {n : ℕ} : n > 0 → n.to_pnat'.val = n := succ_pred_eq_of_pos
+  @[simp] theorem nat_coe_val  {n : ℕ} : n > 0 → (n : ℕ+).val = n := succ_pred_eq_of_pos
+  @[simp] theorem to_pnat'_coe {n : ℕ} : n > 0 → (n.to_pnat' : ℕ) = n := succ_pred_eq_of_pos
+
+end pnat