refactor(library): use subtype instead of sigma

library/data/nat/bquant.lean

@@ -14,41 +14,43 @@ without assuming classical axioms.
 
 More importantly, they can be reduced inside of the Lean kernel.
 -/
-import data.nat.order
+import data.subtype data.nat.order data.nat.div
 
 namespace nat
+  open subtype
+
   definition bex [reducible] (n : nat) (P : nat → Prop) : Prop :=
   ∃ x, x < n ∧ P x
 
-  definition bsig [reducible] (n : nat) (P : nat → Prop) : Type₁ :=
+  definition bsub [reducible] (n : nat) (P : nat → Prop) : Type₁ :=
-  Σ x, x < n ∧ P x
+  {x | x < n ∧ P x}
 
   definition ball [reducible] (n : nat) (P : nat → Prop) : Prop :=
   ∀ x, x < n → P x
 
-  lemma bex_of_bsig {n : nat} {P : nat → Prop} : bsig n P → bex n P :=
+  lemma bex_of_bsub {n : nat} {P : nat → Prop} : bsub n P → bex n P :=
-  assume h, ex_of_sig h
+  assume h, ex_of_sub h
 
   theorem not_bex_zero (P : nat → Prop) : ¬ bex 0 P :=
   λ H, obtain (w : nat) (Hw : w < 0 ∧ P w), from H,
     and.rec_on Hw (λ h₁ h₂, absurd h₁ (not_lt_zero w))
 
-  theorem not_bsig_zero (P : nat → Prop) : bsig 0 P → false :=
+  theorem not_bsub_zero (P : nat → Prop) : bsub 0 P → false :=
-  λ H, absurd (bex_of_bsig H) (not_bex_zero P)
+  λ H, absurd (bex_of_bsub H) (not_bex_zero P)
 
-  definition bsig_succ {P : nat → Prop} {n : nat} (H : bsig n P) : bsig (succ n) P :=
+  definition bsub_succ {P : nat → Prop} {n : nat} (H : bsub n P) : bsub (succ n) P :=
   obtain (w : nat) (Hw : w < n ∧ P w), from H,
-    and.rec_on Hw (λ hlt hp, ⟨w, (and.intro (lt.step hlt) hp)⟩)
+    and.rec_on Hw (λ hlt hp, tag w (and.intro (lt.step hlt) hp))
 
   theorem bex_succ {P : nat → Prop} {n : nat} (H : bex n P) : bex (succ n) P :=
   obtain (w : nat) (Hw : w < n ∧ P w), from H,
     and.rec_on Hw (λ hlt hp, exists.intro w (and.intro (lt.step hlt) hp))
 
-  definition bsig_succ_of_pred {P : nat → Prop} {a : nat} (H : P a) : bsig (succ a) P :=
+  definition bsub_succ_of_pred {P : nat → Prop} {a : nat} (H : P a) : bsub (succ a) P :=
-  ⟨a, and.intro (lt.base a) H⟩
+  tag a (and.intro (lt.base a) H)
 
   theorem bex_succ_of_pred {P : nat → Prop} {a : nat} (H : P a) : bex (succ a) P :=
-  bex_of_bsig (bsig_succ_of_pred H)
+  bex_of_bsub (bsub_succ_of_pred H)
 
   theorem not_bex_succ {P : nat → Prop} {n : nat} (H₁ : ¬ bex n P) (H₂ : ¬ P n) : ¬ bex (succ n) P :=
   λ H, obtain (w : nat) (Hw : w < succ n ∧ P w), from H,
@@ -56,8 +58,8 @@ namespace nat
       (λ heq : w = n, absurd (eq.rec_on heq hp) H₂)
       (λ hltn : w < n, absurd (exists.intro w (and.intro hltn hp)) H₁))
 
-  theorem not_bsig_succ {P : nat → Prop} {n : nat} (H₁ : ¬ bex n P) (H₂ : ¬ P n) : bsig (succ n) P → false :=
+  theorem not_bsub_succ {P : nat → Prop} {n : nat} (H₁ : ¬ bex n P) (H₂ : ¬ P n) : bsub (succ n) P → false :=
-  λ H, absurd (bex_of_bsig H) (not_bex_succ H₁ H₂)
+  λ H, absurd (bex_of_bsub H) (not_bex_succ H₁ H₂)
 
   theorem ball_zero (P : nat → Prop) : ball zero P :=
   λ x Hlt, absurd Hlt !not_lt_zero
@@ -117,18 +119,18 @@ namespace nat
   variable [decP : decidable_pred P]
   include decP
 
-  definition bsig_not_of_not_ball : ∀ {n : nat}, ¬ ball n P → Σ i, i < n ∧ ¬ P i
+  definition bsub_not_of_not_ball : ∀ {n : nat}, ¬ ball n P → {i | i < n ∧ ¬ P i}
   | 0        h := absurd (ball_zero P) h
   | (succ n) h := decidable.by_cases
     (λ hp : P n,
       have h₁ : ¬ ball n P, from
         assume b : ball n P, absurd (ball_succ_of_ball b hp) h,
-      have h₂ : Σ i, i < n ∧ ¬ P i, from bsig_not_of_not_ball h₁,
+      have h₂ : {i | i < n ∧ ¬ P i}, from bsub_not_of_not_ball h₁,
-      bsig_succ h₂)
+      bsub_succ h₂)
-    (λ hn : ¬ P n, bsig_succ_of_pred hn)
+    (λ hn : ¬ P n, bsub_succ_of_pred hn)
 
   theorem bex_not_of_not_ball {n : nat} (H : ¬ ball n P) : bex n (λ n, ¬ P n) :=
-  bex_of_bsig (bsig_not_of_not_ball H)
+  bex_of_bsub (bsub_not_of_not_ball H)
 
   theorem ball_not_of_not_bex : ∀ {n : nat}, ¬ bex n P → ball n (λ n, ¬ P n)
   | 0        h := ball_zero _

library/data/subtype.lean

@@ -12,6 +12,9 @@ tag :: (elt_of : A) (has_property : P elt_of)
 
 notation `{` binders `|` r:(scoped:1 P, subtype P) `}` := r
 
+definition ex_of_sub {A : Type} {P : A → Prop} : { x | P x } → ∃ x, P x
+| (subtype.tag a h) := exists.intro a h
+
 namespace subtype
   variables {A : Type} {P : A → Prop}
 

library/theories/number_theory/primes.lean

@@ -69,26 +69,26 @@ have h₂ : p ≥ 2, from ge_two_of_prime ipp,
 have h₃ : p ≤ i, from le_of_dvd pos h₁,
 lt_of_succ_le (le.trans h₂ h₃)
 
-definition sig_dvd_of_not_prime {n : nat} : n ≥ 2 → ¬ prime n → Σ m, m ∣ n ∧ m ≠ 1 ∧ m ≠ n :=
+definition sub_dvd_of_not_prime {n : nat} : n ≥ 2 → ¬ prime n → {m | m ∣ n ∧ m ≠ 1 ∧ m ≠ n} :=
 assume h₁ h₂,
 have h₃ : ¬ prime_ext n, from iff.mp' (not_iff_not_of_iff !prime_ext_iff_prime) h₂,
 have h₄ : ¬ n ≥ 2 ∨ ¬ (∀ m, m ≤ n → m ∣ n → m = 1 ∨ m = n), from iff.mp !not_and_iff_not_or_not h₃,
 have h₅ : ¬ (∀ m, m ≤ n → m ∣ n → m = 1 ∨ m = n), from or_resolve_right h₄ (not_not_intro h₁),
 have h₆ : ¬ (∀ m, m < succ n → m ∣ n → m = 1 ∨ m = n), from
   assume h, absurd (λ m hl hd, h m (lt_succ_of_le hl) hd) h₅,
-have h₇ : Σ m, m < succ n ∧ ¬(m ∣ n → m = 1 ∨ m = n), from bsig_not_of_not_ball h₆,
+have h₇ : {m | m < succ n ∧ ¬(m ∣ n → m = 1 ∨ m = n)}, from bsub_not_of_not_ball h₆,
 obtain m hlt (h₈ : ¬(m ∣ n → m = 1 ∨ m = n)), from h₇,
 obtain (h₈ : m ∣ n) (h₉ : ¬ (m = 1 ∨ m = n)), from iff.mp !not_implies_iff_and_not h₈,
 have h₁₀ : ¬ m = 1 ∧ ¬ m = n, from iff.mp !not_or_iff_not_and_not h₉,
-⟨m,  and.intro h₈ h₁₀⟩
+subtype.tag m (and.intro h₈ h₁₀)
 
 theorem ex_dvd_of_not_prime {n : nat} : n ≥ 2 → ¬ prime n → ∃ m, m ∣ n ∧ m ≠ 1 ∧ m ≠ n :=
-assume h₁ h₂, ex_of_sig (sig_dvd_of_not_prime h₁ h₂)
+assume h₁ h₂, ex_of_sub (sub_dvd_of_not_prime h₁ h₂)
 
-definition sig_dvd_of_not_prime2 {n : nat} : n ≥ 2 → ¬ prime n → Σ m, m ∣ n ∧ m ≥ 2 ∧ m < n :=
+definition sub_dvd_of_not_prime2 {n : nat} : n ≥ 2 → ¬ prime n → {m | m ∣ n ∧ m ≥ 2 ∧ m < n} :=
 assume h₁ h₂,
 have n_ne_0 : n ≠ 0, from assume h, begin subst n, exact absurd h₁ dec_trivial end,
-obtain m m_dvd_n m_ne_1 m_ne_n, from sig_dvd_of_not_prime h₁ h₂,
+obtain m m_dvd_n m_ne_1 m_ne_n, from sub_dvd_of_not_prime h₁ h₂,
 assert m_ne_0 : m ≠ 0, from assume h, begin subst m, exact absurd (eq_zero_of_zero_dvd m_dvd_n) n_ne_0 end,
 begin
   existsi m, split, assumption,
@@ -99,32 +99,32 @@ begin
 end
 
 theorem ex_dvd_of_not_prime2 {n : nat} : n ≥ 2 → ¬ prime n → ∃ m, m ∣ n ∧ m ≥ 2 ∧ m < n :=
-assume h₁ h₂, ex_of_sig (sig_dvd_of_not_prime2 h₁ h₂)
+assume h₁ h₂, ex_of_sub (sub_dvd_of_not_prime2 h₁ h₂)
 
-definition sig_prime_and_dvd {n : nat} : n ≥ 2 → Σ p, prime p ∧ p ∣ n :=
+definition sub_prime_and_dvd {n : nat} : n ≥ 2 → {p | prime p ∧ p ∣ n} :=
 nat.strong_rec_on n
   (take n,
-   assume ih : ∀ m, m < n → m ≥ 2 → Σ p, prime p ∧ p ∣ m,
+   assume ih : ∀ m, m < n → m ≥ 2 → {p | prime p ∧ p ∣ m},
    assume n_ge_2 : n ≥ 2,
    by_cases
-    (λ h : prime n, ⟨n,  and.intro h (dvd.refl n)⟩)
+    (λ h : prime n, subtype.tag n (and.intro h (dvd.refl n)))
     (λ h : ¬ prime n,
-      obtain m m_dvd_n m_ge_2 m_lt_n, from sig_dvd_of_not_prime2 n_ge_2 h,
+      obtain m m_dvd_n m_ge_2 m_lt_n, from sub_dvd_of_not_prime2 n_ge_2 h,
       obtain p (hp : prime p) (p_dvd_m : p ∣ m), from ih m m_lt_n m_ge_2,
       have p_dvd_n : p ∣ n, from dvd.trans p_dvd_m m_dvd_n,
-      ⟨p, and.intro hp p_dvd_n⟩))
+      subtype.tag p (and.intro hp p_dvd_n)))
 
 lemma ex_prime_and_dvd {n : nat} : n ≥ 2 → ∃ p, prime p ∧ p ∣ n :=
-assume h, ex_of_sig (sig_prime_and_dvd h)
+assume h, ex_of_sub (sub_prime_and_dvd h)
 
 open eq.ops
 
-definition infinite_primes (n : nat) : Σ p, p ≥ n ∧ prime p :=
+definition infinite_primes (n : nat) : {p | p ≥ n ∧ prime p} :=
 let m := fact (n + 1) in
 have Hn1 : n + 1 ≥ 1, from succ_le_succ (zero_le _),
 have m_ge_1 : m ≥ 1,  from le_of_lt_succ (succ_lt_succ (fact_pos _)),
 have m1_ge_2 : m + 1 ≥ 2, from succ_le_succ m_ge_1,
-obtain p (prime_p : prime p) (p_dvd_m1 : p ∣ m + 1), from sig_prime_and_dvd m1_ge_2,
+obtain p (prime_p : prime p) (p_dvd_m1 : p ∣ m + 1), from sub_prime_and_dvd m1_ge_2,
 have p_ge_2 : p ≥ 2, from ge_two_of_prime prime_p,
 have p_gt_0 : p > 0, from lt_of_succ_lt (lt_of_succ_le p_ge_2),
 have p_ge_n : p ≥ n, from by_contradiction
@@ -135,10 +135,10 @@ have p_ge_n : p ≥ n, from by_contradiction
     have h₅ : p ∣ 1, from dvd_of_dvd_add_right (!add.comm ▸ p_dvd_m1) h₄,
     have h₆ : p ≤ 1, from le_of_dvd zero_lt_one h₅,
     absurd (le.trans p_ge_2 h₆) dec_trivial),
-⟨p, and.intro p_ge_n prime_p⟩
+subtype.tag p (and.intro p_ge_n prime_p)
 
 lemma ex_infinite_primes (n : nat) : ∃ p, p ≥ n ∧ prime p :=
-ex_of_sig (infinite_primes n)
+ex_of_sub (infinite_primes n)
 
 lemma odd_of_prime {p : nat} : prime p → p > 2 → odd p :=
 λ pp p_gt_2, by_contradiction (λ hn,