From bdc93cb7f4b150f84e6844d9fc3326d7eef6850e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 23 Jul 2016 12:30:11 -0700 Subject: [PATCH] refactor(library/init): change subtype notation and put it on the top-level --- library/data/nat/bquant.lean | 6 +++--- library/data/nat/find.lean | 4 ++-- library/init/classical.lean | 8 ++++---- library/init/instances.lean | 2 +- library/init/subtype.lean | 11 ++++++----- 5 files changed, 16 insertions(+), 15 deletions(-) diff --git a/library/data/nat/bquant.lean b/library/data/nat/bquant.lean index edb871e884..dacb4812e7 100644 --- a/library/data/nat/bquant.lean +++ b/library/data/nat/bquant.lean @@ -23,7 +23,7 @@ namespace nat ∃ x, x < n ∧ P x 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 @@ -127,13 +127,13 @@ namespace nat variable [decP : decidable_pred P] include decP - definition bsub_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 ¬ ball n P, from assume b : ball n P, absurd (ball_succ_of_ball b hp) h, - have {i | i < n ∧ ¬ P i}, from bsub_not_of_not_ball this, + have {i \ i < n ∧ ¬ P i}, from bsub_not_of_not_ball this, bsub_succ this) (λ hn : ¬ P n, bsub_succ_of_pred hn) diff --git a/library/data/nat/find.lean b/library/data/nat/find.lean index 20f0b2ec71..c4d6f2a557 100644 --- a/library/data/nat/find.lean +++ b/library/data/nat/find.lean @@ -95,7 +95,7 @@ lt.by_cases private lemma wf_gtb : well_founded gtb := well_founded.intro acc_of_ex -private definition find.F (x : nat) : (Π x₁, x₁ ≺ x → lbp x₁ → {a : nat | p a}) → lbp x → {a : nat | p a} := +private definition find.F (x : nat) : (Π x₁, x₁ ≺ x → lbp x₁ → {a : nat \ p a}) → lbp x → {a : nat \ p a} := match x with | 0 := λ f l0, by_cases (λ p0 : p 0, tag 0 p0) @@ -111,7 +111,7 @@ match x with f (succ (succ n)) this lss) end include ex -- todo remove -private definition find_x : {x : nat | p x} := +private definition find_x : {x : nat \ p x} := @fix _ _ _ wf_gtb find.F 0 lbp_zero end find_x diff --git a/library/init/classical.lean b/library/init/classical.lean index 5bf4110e3a..d62820fce0 100644 --- a/library/init/classical.lean +++ b/library/init/classical.lean @@ -14,13 +14,13 @@ open subtype -- In the presence of classical logic, we could prove this from a weaker statement: -- axiom indefinite_description {A : Type} {P : A->Prop} (H : ∃x, P x) : {x : A, P x} axiom strong_indefinite_description {A : Type} (P : A → Prop) (H : nonempty A) : - { x | (∃y : A, P y) → P x} + { x \ (∃y : A, P y) → P x} theorem exists_true_of_nonempty {A : Type} (H : nonempty A) : ∃x : A, true := nonempty.elim H (take x, exists.intro x trivial) noncomputable definition inhabited_of_nonempty {A : Type} (H : nonempty A) : inhabited A := -let u : {x | (∃y : A, true) → true} := strong_indefinite_description (λa, true) H in +let u : {x \ (∃y : A, true) → true} := strong_indefinite_description (λa, true) H in inhabited.mk (elt_of u) noncomputable definition inhabited_of_exists {A : Type} {P : A → Prop} (H : ∃x, P x) : inhabited A := @@ -29,13 +29,13 @@ inhabited_of_nonempty (exists.elim H (λ w Hw, nonempty.intro w)) /- the Hilbert epsilon function -/ noncomputable definition epsilon {A : Type} [H : nonempty A] (P : A → Prop) : A := -let u : {x | (∃y, P y) → P x} := +let u : {x \ (∃y, P y) → P x} := strong_indefinite_description P H in elt_of u theorem epsilon_spec_aux {A : Type} (H : nonempty A) (P : A → Prop) (Hex : ∃y, P y) : P (@epsilon A H P) := -let u : {x | (∃y, P y) → P x} := +let u : {x \ (∃y, P y) → P x} := strong_indefinite_description P H in have aux : (∃y, P y) → P (elt_of (strong_indefinite_description P H)), from has_property u, aux Hex diff --git a/library/init/instances.lean b/library/init/instances.lean index 530562a742..c14b9b5a1d 100644 --- a/library/init/instances.lean +++ b/library/init/instances.lean @@ -8,7 +8,7 @@ import init.meta.mk_dec_eq_instance init.subtype init.meta.occurrences open tactic subtype -definition subtype_decidable_eq [instance] {A : Type} {P : A → Prop} [decidable_eq A] : decidable_eq {x | P x} := +definition subtype_decidable_eq [instance] {A : Type} {P : A → Prop} [decidable_eq A] : decidable_eq {x \ P x} := by mk_dec_eq_instance definition list_decidable_eq [instance] {A : Type} [decidable_eq A] : decidable_eq (list A) := diff --git a/library/init/subtype.lean b/library/init/subtype.lean index 78817181a0..6e2958eb5e 100644 --- a/library/init/subtype.lean +++ b/library/init/subtype.lean @@ -12,10 +12,11 @@ set_option structure.proj_mk_thm true structure subtype {A : Type} (P : A → Prop) := tag :: (elt_of : A) (has_property : P elt_of) -namespace subtype - notation `{` binder ` | ` r:(scoped:1 P, subtype P) `}` := r +notation `{` binder ` \ `:0 r:(scoped:1 P, subtype P) `}` := r - definition exists_of_subtype {A : Type} {P : A → Prop} : { x | P x } → ∃ x, P x +namespace subtype + + definition exists_of_subtype {A : Type} {P : A → Prop} : { x \ P x } → ∃ x, P x | (subtype.tag a h) := exists.intro a h variables {A : Type} {P : A → Prop} @@ -26,12 +27,12 @@ namespace subtype theorem tag_eq {a1 a2 : A} {H1 : P a1} {H2 : P a2} (H3 : a1 = a2) : tag a1 H1 = tag a2 H2 := eq.subst H3 (tag_irrelevant H1) H2 - protected theorem eq : ∀ {a1 a2 : {x | P x}} (H : elt_of a1 = elt_of a2), a1 = a2 + protected theorem eq : ∀ {a1 a2 : {x \ P x}} (H : elt_of a1 = elt_of a2), a1 = a2 | (tag x1 H1) (tag x2 H2) := tag_eq end subtype open subtype variables {A : Type} {P : A → Prop} -protected definition subtype.is_inhabited [instance] {a : A} (H : P a) : inhabited {x | P x} := +protected definition subtype.is_inhabited [instance] {a : A} (H : P a) : inhabited {x \ P x} := inhabited.mk (tag a H)