Library mathcomp.ssreflect.generic_quotient

Quotient Types NB: See CONTRIBUTING.md for an introduction to HB concepts and commands. Provided a base type T, this files defines an interface for quotients Q of the type T with explicit functions for canonical surjection (\pi : T -> Q) and for choosing a representative (repr : Q -> T). It then provides a helper to quotient T by a decidable equivalence relation (e : rel T) if T is a choiceType (or encodable as a choiceType modulo e). Reference: Cyril Cohen, Pragmatic Quotient Types in Coq, ITP 2013

Generic Quotienting ***

quotType T == the type of quotient types based on T The HB class is called Quotient. The quotType interface supports these operations (in quotient_scope): \pi_Q x == the class in Q of the element x of T \pi x == the class of x where Q is inferred from the context repr c == canonical representative in T of the class c x = y % [mod Q] := \pi_Q x = \pi_Q y <-> x and y are equal modulo Q x <> y % [mod Q] := \pi_Q x <> \pi_Q y x == y % [mod Q] := \pi_Q x == \pi_Q y x != y % [mod Q] := \pi_Q x != \pi_Q y The quotient_scope is delimited by %qT, The most useful lemmas are piE and reprK. List of factories: isQuotient.Build T Q (reprK : cancel repr pi) == builds the quotient whose canonical surjection function is (pi : T -> Q) and whose representative selection function is repr

Morphisms ***

One may declare existing functions and predicates as liftings of some morphisms for a quotient. PiMorph1 pi_f == where pi_f : {morph \pi : x / f x >-> fq x} declares fq : Q -> Q as the lifting of f : T -> T PiMorph2 pi_g == idem with pi_g : {morph \pi : x y / g x y >-> gq x y} PiMono1 pi_p == idem with pi_p : {mono \pi : x / p x >-> pq x} PiMono2 pi_r == idem with pi_r : {morph \pi : x y / r x y >-> rq x y} PiMorph11 pi_f == idem with pi_f : {morph \pi : x / f x >-> fq x} where fq : Q -> Q' and f : T -> T'. PiMorph eq == Most general declaration of compatibility, /!\ use with caution /!\ One can use the following helpers to build the liftings which may or may not satisfy the above properties (but if they do not, it is probably not a good idea to define them): lift_op1 Q f := lifts f : T -> T lift_op2 Q g := lifts g : T -> T -> T lift_fun1 Q p := lifts p : T -> R lift_fun2 Q r := lifts r : T -> T -> R lift_op11 Q Q' f := lifts f : T -> T' There is also the special case of constants and embedding functions that one may define and declare as compatible with Q using: lift_cst Q x := lifts x : T to Q PiConst c := declare the result c of the previous construction as compatible with Q lift_embed Q e := lifts e : R -> T to R -> Q PiEmbed f := declare the result f of the previous construction as compatible with Q

Quotients that have an eqType structure ***

Having a canonical (eqQuotType e) structure enables piE to replace terms of the form (x == y) by terms of the form (e x' y') if x and y are canonical surjections of some x' and y'. eqQuotType e == the type of quotients types on T which mirror the equivalence relation (e : rel T) the HB class is called EqQuotient. The most useful property is that an eqQuotType is an eqType. List of factories: isEqQuotient.Build T e Q m == builds an (eqQuotType e) structure on Q from the morphism property m where m : {mono \pi : x y / e x y >-> x == y}

Equivalence and quotient by an equivalence ***

EquivRel r er es et == builds an equiv_rel structure based on the reflexivity, symmetry and transitivity property of a boolean relation. {eq_quot e} == builds the quotType of T by equiv where e : rel T is an equiv_rel and T is a choiceType or a (choiceTypeMod e) it is canonically an eqType, a choiceType, a quotType and an eqQuotType x = y % [mod_eq e] := x = y % [mod {eq_quot e} ] <-> x and y are equal modulo e ...

Definition of the quotient interface.

Protecting some symbols.

Fancy Notations

Exporting the theory

About morphisms This was pi_morph T (x : T) := PiMorph { pi_op : T; _ : x = pi_op }.

Internal Lemmas : do not use directly

Declaration of morphisms

lifting helpers

constant declaration

embedding declaration, please don't redefine \pi

About eqQuotType

Even if a quotType is a natural subType, we do not make this subType canonical, to allow the user to define the subtyping he wants. However one can:

• get the hasDecEq and the hasChoice by subtyping
• get the subType structure and maybe declare it Canonical.

Definition of a (decidable) equivalence relation

Encoding to another type modulo an equivalence

Quotient by a equivalence relation

If the type is directly a choiceType, no need to encode

Recovering a potential countable type structure