refactor(data/subtype): organise in namespaces, use variables, add two simp-lemmas (#760)

Author: jcommelin

src/data/subtype.lean

@@ -4,43 +4,34 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Johannes Hölzl
 -/
 
+-- Lean complains if this section is turned into a namespace
 section subtype
-variables {α : Sort*} {β : α → Prop}
+variables {α : Sort*} {p : α → Prop}
 
-protected lemma subtype.eq' : ∀ {a1 a2 : {x // β x}}, a1.val = a2.val → a1 = a2
-| ⟨x, h1⟩ ⟨.(x), h2⟩ rfl := rfl
-
-lemma subtype.ext {a1 a2 : {x // β x}} : a1 = a2 ↔ a1.val = a2.val :=
-⟨congr_arg _, subtype.eq'⟩
-
-lemma subtype.coe_ext {a1 a2 : {x // β x}} : a1 = a2 ↔ (a1 : α) = a2 :=
-subtype.ext
-
-theorem subtype.val_injective : function.injective (@subtype.val _ β) :=
-λ a b, subtype.eq'
-
-@[simp] theorem subtype.coe_eta {α : Type*} {β : α → Prop}
- (a : {a // β a}) (h : β a) : subtype.mk ↑a h = a := subtype.eta _ _
-
-@[simp] theorem subtype.coe_mk {α : Type*} {β : α → Prop}
- (a h) : (@subtype.mk α β a h : α) = a := rfl
-
-@[simp] theorem subtype.mk_eq_mk {α : Type*} {β : α → Prop}
- {a h a' h'} : @subtype.mk α β a h = @subtype.mk α β a' h' ↔ a = a' :=
-⟨λ H, by injection H, λ H, by congr; assumption⟩
-
-@[simp] theorem subtype.forall {p : {a // β a} → Prop} :
-  (∀ x, p x) ↔ (∀ a b, p ⟨a, b⟩) :=
+@[simp] theorem subtype.forall {q : {a // p a} → Prop} :
+  (∀ x, q x) ↔ (∀ a b, q ⟨a, b⟩) :=
 ⟨assume h a b, h ⟨a, b⟩, assume h ⟨a, b⟩, h a b⟩
 
-@[simp] theorem subtype.exists {p : {a // β a} → Prop} :
-  (∃ x, p x) ↔ (∃ a b, p ⟨a, b⟩) :=
+@[simp] theorem subtype.exists {q : {a // p a} → Prop} :
+  (∃ x, q x) ↔ (∃ a b, q ⟨a, b⟩) :=
 ⟨assume ⟨⟨a, b⟩, h⟩, ⟨a, b, h⟩, assume ⟨a, b, h⟩, ⟨⟨a, b⟩, h⟩⟩
 
 end subtype
 
 namespace subtype
-variables {α : Sort*} {β : Sort*} {γ : Sort*}
+variables {α : Sort*} {β : Sort*} {γ : Sort*} {p : α → Prop}
+
+protected lemma eq' : ∀ {a1 a2 : {x // p x}}, a1.val = a2.val → a1 = a2
+| ⟨x, h1⟩ ⟨.(x), h2⟩ rfl := rfl
+
+lemma ext {a1 a2 : {x // p x}} : a1 = a2 ↔ a1.val = a2.val :=
+⟨congr_arg _, subtype.eq'⟩
+
+lemma coe_ext {a1 a2 : {x // p x}} : a1 = a2 ↔ (a1 : α) = a2 :=
+ext
+
+theorem val_injective : function.injective (@val _ p) :=
+λ a b, subtype.eq'
 
 /-- Restriction of a function to a function on subtypes. -/
 def map {p : α → Prop} {q : β → Prop} (f : α → β) (h : ∀a, p a → q (f a)) :
@@ -55,19 +46,14 @@ rfl
 theorem map_id {p : α → Prop} {h : ∀a, p a → p (id a)} : map (@id α) h = id :=
 funext $ assume ⟨v, h⟩, rfl
 
-end subtype
-
-namespace subtype
-variables {α : Sort*}
-
 instance [has_equiv α] (p : α → Prop) : has_equiv (subtype p) :=
 ⟨λ s t, s.val ≈ t.val⟩
 
 theorem equiv_iff [has_equiv α] {p : α → Prop} {s t : subtype p} :
   s ≈ t ↔ s.val ≈ t.val :=
 iff.rfl
 
-variables [setoid α] {p : α → Prop}
+variables [setoid α]
 
 protected theorem refl (s : subtype p) : s ≈ s :=
 setoid.refl s.val
@@ -79,9 +65,28 @@ protected theorem trans {s t u : subtype p} (h₁ : s ≈ t) (h₂ : t ≈ u) :
 setoid.trans h₁ h₂
 
 theorem equivalence (p : α → Prop) : equivalence (@has_equiv.equiv (subtype p) _) :=
-mk_equivalence _ subtype.refl (@subtype.symm _ _ p) (@subtype.trans _ _ p)
+mk_equivalence _ subtype.refl (@subtype.symm _ p _) (@subtype.trans _ p _)
 
 instance (p : α → Prop) : setoid (subtype p) :=
 setoid.mk (≈) (equivalence p)
 
 end subtype
+
+namespace subtype
+variables {α : Type*} {β : Type*} {γ : Type*} {p : α → Prop}
+
+@[simp] theorem coe_eta {α : Type*} {p : α → Prop}
+ (a : {a // p a}) (h : p a) : mk ↑a h = a := eta _ _
+
+@[simp] theorem coe_mk {α : Type*} {p : α → Prop}
+ (a h) : (@mk α p a h : α) = a := rfl
+
+@[simp] theorem mk_eq_mk {α : Type*} {p : α → Prop}
+ {a h a' h'} : @mk α p a h = @mk α p a' h' ↔ a = a' :=
+⟨λ H, by injection H, λ H, by congr; assumption⟩
+
+@[simp] lemma val_prop {S : set α} (a : {a // a ∈ S}) : a.val ∈ S := a.property
+
+@[simp] lemma val_prop' {S : set α} (a : {a // a ∈ S}) : ↑a ∈ S := a.property
+
+end subtype