From 9d83361fdcdeab257df0f6d311c843d4d2553a93 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 16 Jul 2015 22:48:33 -0400 Subject: [PATCH] refactor(library): use subtype instead of sigma --- library/data/nat/bquant.lean | 40 ++++++++++++---------- library/data/subtype.lean | 3 ++ library/theories/number_theory/primes.lean | 34 +++++++++--------- 3 files changed, 41 insertions(+), 36 deletions(-) diff --git a/library/data/nat/bquant.lean b/library/data/nat/bquant.lean index 0e95f27e6..26ae85568 100644 --- a/library/data/nat/bquant.lean +++ b/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₁ := - Σ x, x < n ∧ P x + definition bsub [reducible] (n : nat) (P : nat → Prop) : Type₁ := + {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 := - assume h, ex_of_sig h + lemma bex_of_bsub {n : nat} {P : nat → Prop} : bsub n P → bex n P := + 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 := - λ H, absurd (bex_of_bsig H) (not_bex_zero P) + theorem not_bsub_zero (P : nat → Prop) : bsub 0 P → false := + λ 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 := - ⟨a, and.intro (lt.base a) H⟩ + definition bsub_succ_of_pred {P : nat → Prop} {a : nat} (H : P a) : bsub (succ a) P := + 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 := - λ H, absurd (bex_of_bsig H) (not_bex_succ H₁ H₂) + 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_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₁, - bsig_succ h₂) - (λ hn : ¬ P n, bsig_succ_of_pred hn) + have h₂ : {i | i < n ∧ ¬ P i}, from bsub_not_of_not_ball h₁, + bsub_succ h₂) + (λ 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 _ diff --git a/library/data/subtype.lean b/library/data/subtype.lean index 14a807e59..72cdc4d2d 100644 --- a/library/data/subtype.lean +++ b/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} diff --git a/library/theories/number_theory/primes.lean b/library/theories/number_theory/primes.lean index f60233e34..186d42242 100644 --- a/library/theories/number_theory/primes.lean +++ b/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,