feat(library/data): define unordered pairs using quotients

library/data/uprod.lean

@@ -0,0 +1,99 @@
+/-
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Module: data.uprod
+Author: Leonardo de Moura
+
+Unordered pairs
+-/
+import data.prod logic.identities algebra.function
+open prod prod.ops quot function
+
+private definition eqv {A : Type} (p₁ p₂ : A × A) : Prop :=
+p₁ = p₂ ∨ swap p₁ = p₂
+
+infix `~` := eqv    -- this is "~"
+
+private theorem eqv.refl {A : Type} : ∀ p : A × A, p ~ p :=
+take p, or.inl rfl
+
+private theorem eqv.symm {A : Type} : ∀ p₁ p₂ : A × A, p₁ ~ p₂ → p₂ ~ p₁ :=
+take p₁ p₂ h, or.elim h
+  (λ e, by rewrite e; apply eqv.refl)
+  (λ e, begin esimp [eqv], rewrite [-e, swap_swap], exact (or.inr rfl) end)
+
+private theorem eqv.trans {A : Type} : ∀ p₁ p₂ p₃ : A × A, p₁ ~ p₂ → p₂ ~ p₃ → p₁ ~ p₃ :=
+take p₁ p₂ p₃ h₁ h₂, or.elim h₁
+  (λ e₁₂,  or.elim h₂
+    (λ e₂₃,  by rewrite [e₁₂, e₂₃]; apply eqv.refl)
+    (λ es₂₃, begin esimp [eqv], rewrite -es₂₃, exact (or.inr (congr_arg swap e₁₂)) end))
+  (λ es₁₂, or.elim h₂
+    (λ e₂₃,  begin esimp [eqv], rewrite es₁₂, exact (or.inr e₂₃) end)
+    (λ es₂₃, begin esimp [eqv], rewrite [-es₁₂ at es₂₃, swap_swap at es₂₃], exact (or.inl es₂₃) end))
+
+private theorem is_equivalence (A : Type) : equivalence (@eqv A) :=
+mk_equivalence (@eqv A) (@eqv.refl A) (@eqv.symm A) (@eqv.trans A)
+
+definition uprod.setoid [instance] (A : Type) : setoid (A × A) :=
+setoid.mk (@eqv A) (is_equivalence A)
+
+definition uprod (A : Type) : Type :=
+quot (uprod.setoid A)
+
+namespace uprod
+  definition mk {A : Type} (a b : A) : uprod A :=
+  ⟦(a, b)⟧
+
+  theorem mk_eq_mk {A : Type} (a b : A) : mk a b = mk b a :=
+  quot.sound (or.inr rfl)
+
+  private definition mem_fn {A : Type} (a : A) : A × A → Prop
+  | (a₁, a₂) := a = a₁ ∨ a = a₂
+
+  private lemma mem_swap {A : Type} {a : A} : ∀ {p : A × A}, mem_fn a p ↔ mem_fn a (swap p)
+  | (a₁, a₂) := iff.intro
+    (λ l : a = a₁ ∨ a = a₂, or.swap l)
+    (λ r : a = a₂ ∨ a = a₁, or.swap r)
+
+  private lemma mem_coherent {A : Type} : ∀ {p₁ p₂ : A × A} (a : A),  p₁ ~ p₂ → mem_fn a p₁ = mem_fn a p₂
+  | (a₁, b₁) (a₂, b₂) a h :=
+    or.elim h
+     (λ e,  by rewrite e)
+     (λ es, begin rewrite -es, apply propext, rewrite (propext mem_swap) end)
+
+  definition mem {A : Type} (a : A) (u : uprod A) : Prop :=
+  quot.lift_on u (λ p, mem_fn a p) (λ p₁ p₂ e, mem_coherent a e)
+
+  infix `∈` := mem
+
+  theorem mem_mk_left {A : Type} (a b : A) : a ∈ mk a b :=
+  or.inl rfl
+
+  theorem mem_mk_right {A : Type} (a b : A) : b ∈ mk a b :=
+  or.inr rfl
+
+  theorem mem_or_mem_of_mem_mk {A : Type} {a b c : A} : c ∈ mk a b → c = a ∨ c = b :=
+  λ h, h
+
+  private definition map_fn {A B : Type} (f : A → B) : A × A → uprod B
+  | (a₁, a₂) := mk (f a₁) (f a₂)
+
+  private lemma map_coherent {A B : Type} (f : A → B) : ∀ {p₁ p₂ : A × A}, p₁ ~ p₂ → map_fn f p₁ = map_fn f p₂
+  | (a₁, b₁) (a₂, b₂) h :=
+    or.elim h
+      (λ e,  by rewrite e)
+      (λ es, begin rewrite -es, apply quot.sound, exact (or.inr rfl) end)
+
+  definition map {A B : Type} (f : A → B) (u : uprod A) : uprod B :=
+  quot.lift_on u (λ p, map_fn f p) (λ p₁ p₂ c, map_coherent f c)
+
+  theorem mem_map_mk_left {A B : Type} (f : A → B) (a₁ a₂ : A) : f a₁ ∈ map f (mk a₁ a₂) :=
+  or.inl rfl
+
+  theorem mem_map_mk_right {A B : Type} (f : A → B) (a₁ a₂ : A) : f a₂ ∈ map f (mk a₁ a₂) :=
+  or.inr rfl
+
+  theorem map_map {A B C : Type} (g : B → C) (f : A → B) (u : uprod A) : map g (map f u) = map (g ∘ f) u :=
+  quot.induction_on u (λ p : A × A, begin cases p, apply rfl end)
+end uprod