refactor(library/data/subtype): define subtype using 'structure' command

library/data/quotient/basic.lean

@@ -212,7 +212,7 @@ theorem fun_image_def {A B : Type} (f : A → B) (a : A) :
   fun_image f a = tag (f a) (exists_intro a rfl) := rfl
 
 theorem elt_of_fun_image {A B : Type} (f : A → B) (a : A) : elt_of (fun_image f a) = f a :=
-elt_of_tag _ _
+elt_of.tag _ _
 
 theorem image_elt_of {A B : Type} {f : A → B} (u : image f) : ∃a, f a = elt_of u :=
 has_property u

library/data/subtype.lean

@@ -6,41 +6,28 @@ import logic.inhabited logic.eq logic.decidable
 
 open decidable
 
-inductive subtype {A : Type} (P : A → Prop) : Type :=
+structure subtype {A : Type} (P : A → Prop) :=
-  tag : Πx : A, P x → subtype P
+tag :: (elt_of : A) (has_property : P elt_of)
 
-notation `{` binders `,` r:(scoped P, subtype P) `}` := r
+notation `{` binders `|` r:(scoped 1 P, subtype P) `}` := r
 
 namespace subtype
   variables {A : Type} {P : A → Prop}
 
-  -- TODO: make this a coercion?
-  definition  elt_of (a : {x, P x}) : A := rec (λ x y, x) a
-  theorem has_property (a : {x, P x}) : P (elt_of a) := rec (λ x y, y) a
-
-  theorem elt_of_tag (a : A) (H : P a) : elt_of (tag a H) = a := rfl
-
-  protected theorem destruct {Q : {x, P x} → Prop} (a : {x, P x})
-      (H : ∀(x : A) (H1 : P x), Q (tag x H1)) : Q a :=
-    rec H a
-
   theorem tag_irrelevant {a : A} (H1 H2 : P a) : tag a H1 = tag a H2 :=
   rfl
 
-  theorem tag_elt_of (a : subtype P) : ∀(H : P (elt_of a)), tag (elt_of a) H = a :=
-    destruct a (take (x : A) (H1 : P x) (H2 : P x), rfl)
-
   theorem tag_eq {a1 a2 : A} {H1 : P a1} {H2 : P a2} (H3 : a1 = a2) : tag a1 H1 = tag a2 H2 :=
   eq.subst H3 (take H2, tag_irrelevant H1 H2) H2
 
-  protected theorem equal {a1 a2 : {x, P x}} : ∀(H : elt_of a1 = elt_of a2), a1 = a2 :=
+  protected theorem equal {a1 a2 : {x | P x}} : ∀(H : elt_of a1 = elt_of a2), a1 = a2 :=
   destruct a1 (take x1 H1, destruct a2 (take x2 H2 H, tag_eq H))
 
-  protected definition is_inhabited [instance] {a : A} (H : P a) : inhabited {x, P x} :=
+  protected definition is_inhabited [instance] {a : A} (H : P a) : inhabited {x | P x} :=
   inhabited.mk (tag a H)
 
-  protected definition has_decidable_eq [instance] (H : decidable_eq A) : decidable_eq {x, P x} :=
+  protected definition has_decidable_eq [instance] (H : decidable_eq A) : decidable_eq {x | P x} :=
-  take a1 a2 : {x, P x},
+  take a1 a2 : {x | P x},
     have H1 : (a1 = a2) ↔ (elt_of a1 = elt_of a2), from
       iff.intro (assume H, eq.subst H rfl) (assume H, equal H),
     decidable_iff_equiv _ (iff.symm H1)

library/logic/axioms/hilbert.lean

@@ -19,7 +19,7 @@ open subtype inhabited nonempty
 -- ---------
 
 axiom strong_indefinite_description {A : Type} (P : A → Prop) (H : nonempty A) :
-  {x : A, (∃x : A, P x) → P x}
+  { x | (∃y : A, P y) → P x}
 
 -- In the presence of classical logic, we could prove this from the weaker
 -- axiom indefinite_description {A : Type} {P : A->Prop} (H : ∃x, P x) : {x : A, P x}
@@ -28,7 +28,7 @@ theorem nonempty_imp_exists_true {A : Type} (H : nonempty A) : ∃x : A, true :=
 nonempty.elim H (take x, exists_intro x trivial)
 
 theorem nonempty_imp_inhabited {A : Type} (H : nonempty A) : inhabited A :=
-let u : {x : A, (∃x : 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)
 
 theorem exists_imp_inhabited {A : Type} {P : A → Prop} (H : ∃x, P x) : inhabited A :=
@@ -39,13 +39,13 @@ nonempty_imp_inhabited (obtain w Hw, from H, nonempty.intro w)
 -- ----------------------------
 
 opaque definition epsilon {A : Type} [H : nonempty A] (P : A → Prop) : A :=
-let u : {x : A, (∃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 : A, (∃y, P y) → P x} :=
+let u : {x | (∃y, P y) → P x} :=
   strong_indefinite_description P H in
 has_property u Hex
 

tests/lean/print_ax2.lean.expected.out

@@ -1,2 +1,2 @@
 funext : ∀ {A : Type} {B : A → Type} {f g : Π (a : A), B a}, (∀ (a : A), f a = g a) → f = g
-strong_indefinite_description : Π {A : Type} (P : A → Prop), nonempty A → { (x : A), (∃ (x : A), P x) → P x }
+strong_indefinite_description : Π {A : Type} (P : A → Prop), nonempty A → { (x : A) | (∃ (x : A), P x) → P x }