feat (data/pnat): extensions to pnat (#1073)

* Extended API, especially divisibility and primes

* Positive euclidean algorithm

* Disambiguate overloaded ::

* Tweak broken proof of flip_is_special

* Change to mathlib style

* Update src/data/pnat.lean

Co-Authored-By: Johan Commelin <johan@commelin.net>

* Update src/data/pnat.lean

Co-Authored-By: Johan Commelin <johan@commelin.net>

* Adjust style for mathlib

* Moved and renamed

* Move some material from basic.lean to prime.lean

* Move some material from basic.lean to factors.lean

* Update import to data.pnat.basic.

* Update import to data.pnat.basic

* Fix import of data.pnat.basic

* Use monoid.pow instead of nat.pow

* Fix pnat.pow_succ -> pow_succ; stylistic changes

* More systematic use of coercion

* More consistent use of coercion

* Formatting; change flip' to prod.swap

Author: NeilStrickland

src/data/hash_map.lean

@@ -3,7 +3,7 @@ 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.basic data.pnat data.array.lemmas
+import data.list.basic data.pnat.basic data.array.lemmas
    logic.basic algebra.group
    data.list.defs data.nat.basic data.option.basic
    data.bool data.prod
@@ -227,13 +227,13 @@ theorem valid.replace_aux (a : α) (b : β a) : Π (l : list (Σ a, β a)), a 
 | (⟨a', b'⟩::t) := begin
   by_cases e : a' = a,
   { subst a',
-    suffices : ∃ u w (b'' : β a),
-      sigma.mk a b' :: t = u ++ ⟨a, b''⟩ :: w ∧
+    suffices : ∃ (u w : list Σ a, β a) (b'' : β a),
+      (sigma.mk a b') :: t = u ++ ⟨a, b''⟩ :: w ∧
       replace_aux a b (⟨a, b'⟩ :: t) = u ++ ⟨a, b⟩ :: w, {simpa},
     refine ⟨[], t, b', _⟩, simp [replace_aux] },
   { suffices : ∀ (x : β a) (_ : sigma.mk a x ∈ t), ∃ u w (b'' : β a),
-      sigma.mk a' b' :: t = u ++ ⟨a, b''⟩ :: w ∧
-      sigma.mk a' b' :: replace_aux a b t = u ++ ⟨a, b⟩ :: w,
+      (sigma.mk a' b') :: t = u ++ ⟨a, b''⟩ :: w ∧
+      (sigma.mk a' b') :: (replace_aux a b t) = u ++ ⟨a, b⟩ :: w,
     { simpa [replace_aux, ne.symm e, e] },
     intros x m,
     have IH : ∀ (x : β a) (_ : sigma.mk a x ∈ t), ∃ u w (b'' : β a),
@@ -282,11 +282,12 @@ theorem valid.erase_aux (a : α) : Π (l : list (Σ a, β a)), a ∈ l.map sigma
   by_cases e : a' = a,
   { subst a',
     simpa [erase_aux, and_comm] using show ∃ u w (x : β a),
-      t = u ++ w ∧ sigma.mk a b' :: t = u ++ ⟨a, x⟩ :: w, from ⟨[], t, b', by simp⟩ },
+      t = u ++ w ∧ (sigma.mk a b') :: t = u ++ ⟨a, x⟩ :: w,
+      from ⟨[], t, b', by simp⟩ },
   { simp [erase_aux, e, ne.symm e],
     suffices : ∀ (b : β a) (_ : sigma.mk a b ∈ t), ∃ u w (x : β a),
-      sigma.mk a' b' :: t = u ++ ⟨a, x⟩ :: w ∧
-      sigma.mk a' b' :: erase_aux a t = u ++ w,
+      (sigma.mk a' b') :: t = u ++ ⟨a, x⟩ :: w ∧
+      (sigma.mk a' b') :: (erase_aux a t) = u ++ w,
     { simpa [replace_aux, ne.symm e, e] },
     intros b m,
     have IH : ∀ (x : β a) (_ : sigma.mk a x ∈ t), ∃ u w (x : β a),

src/data/nat/prime.lean

@@ -421,4 +421,18 @@ show p^k*p ∣ m ∨ p^l*p ∣ n, from
     (assume : p ∣ m / p ^ k, or.inl $ mul_dvd_of_dvd_div hpm this)
     (assume : p ∣ n / p ^ l, or.inr $ mul_dvd_of_dvd_div hpn this)
 
+/-- The type of prime numbers -/
+def primes := {p : ℕ // p.prime}
+
+namespace primes
+
+instance : has_repr nat.primes := ⟨λ p, repr p.val⟩
+
+instance coe_nat  : has_coe nat.primes ℕ  := ⟨subtype.val⟩
+
+theorem coe_nat_inj (p q : nat.primes) : (p : ℕ) = (q : ℕ) → p = q :=
+λ h, subtype.eq h
+
+end primes
+
 end nat