lean2/library/data/quotient/classical.lean
Leonardo de Moura ea739100b3 fix(library/unifier): broken optimization in the unifier
See new comments and tests for details.
2014-10-28 16:09:41 -07:00

59 lines
2 KiB
Text

-- Copyright (c) 2014 Floris van Doorn. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Floris van Doorn
import algebra.relation logic.nonempty data.subtype
import logic.axioms.classical logic.axioms.hilbert logic.axioms.funext
import .basic
namespace quotient
open relation nonempty subtype
-- abstract quotient
-- -----------------
definition prelim_map {A : Type} (R : A → A → Prop) (a : A) :=
-- TODO: it is interesting how the elaborator fails here
-- epsilon (fun b, R a b)
@epsilon _ (nonempty.intro a) (fun b, R a b)
-- TODO: only needed R reflexive (or weaker: R a a)
theorem prelim_map_rel {A : Type} {R : A → A → Prop} (H : is_equivalence R) (a : A)
: R a (prelim_map R a) :=
have reflR : reflexive R, from is_reflexive.infer R,
epsilon_spec (exists_intro a (reflR a))
-- TODO: only needed: R PER
theorem prelim_map_congr {A : Type} {R : A → A → Prop} (H1 : is_equivalence R) {a b : A}
(H2 : R a b) : prelim_map R a = prelim_map R b :=
have symmR : symmetric R, from is_symmetric.infer R,
have transR : transitive R, from is_transitive.infer R,
have H3 : ∀c, R a c ↔ R b c, from
take c,
iff.intro
(assume H4 : R a c, transR (symmR H2) H4)
(assume H4 : R b c, transR H2 H4),
have H4 : (fun c, R a c) = (fun c, R b c), from
funext (take c, iff_to_eq (H3 c)),
have H5 [visible] : nonempty A, from
nonempty.intro a,
show epsilon (λc, R a c) = epsilon (λc, R b c), from
congr_arg _ H4
definition quotient {A : Type} (R : A → A → Prop) : Type := image (prelim_map R)
definition quotient_abs {A : Type} (R : A → A → Prop) : A → quotient R :=
fun_image (prelim_map R)
definition quotient_elt_of {A : Type} (R : A → A → Prop) : quotient R → A := elt_of
-- TODO: I had to make is_quotient transparent -- change this?
theorem quotient_is_quotient {A : Type} (R : A → A → Prop) (H : is_equivalence R)
: is_quotient R (quotient_abs R) (quotient_elt_of R) :=
representative_map_to_quotient_equiv
H
(prelim_map_rel H)
(@prelim_map_congr _ _ H)
end quotient