# Library mathcomp.ssreflect.eqtype

(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B.                                  *)

From HB Require Import structures.
From mathcomp Require Import ssreflect ssrfun ssrbool.

This file defines two "base" combinatorial interfaces: eqType == the structure for types with a decidable equality. subType P == the structure for types isomorphic to {x : T | P x} with P : pred T for some type T.

# EqType (types with boolean equality relation)

Equality.axiom e <-> e : rel T is a valid comparison decision procedure for type T: reflect (x = y) (e x y) for all x y : T.
List of factories (to use with HB.instance Definition _ := )
• hasDecEq.Build T eqP Declares an EqType on T from the equality axiom for some relation eqP must be an instance of Equality.axiom
for generic folding of equality predicates (see lemma eqE below). [eqType of T for eT] == clone for T of eT, where eT is an eqType for a type convertible, but usually not identical, to T. [eqType of T] == clone for T of the eqType inferred for T, possibly after unfolding some definitions. [hasDecEq of T] == mixin of the eqType inferred for T. comparable T <-> equality on T is decidable. := forall x y : T, decidable (x = y) comparableMixin compT == equality mixin for compT : comparable T. InjEqMixin injf == an Equality mixin for T, using an f : T -> U where U has an eqType structure and injf : injective f. PcanEqMixin fK == an Equality mixin similarly derived from f and a left inverse partial function g and fK : pcancel f g. CanEqMixin fK == an Equality mixin similarly derived from f and a left inverse function g and fK : cancel f g. > Equality mixins derived by the above should never be made Canonical as they provide only comparisons with a generic head constant. The eqType interface supports the following operations: x == y <=> x compares equal to y (this is a boolean test). x == y :> T <=> x == y at type T. x != y <=> x and y compare unequal. x != y :> T <=> x and y compare unequal at type T. x =P y :: a proof of reflect (x = y) (x == y); x =P y coerces to x == y -> x = y. eqbLHS := (X in (X == _))%pattern (for rewriting) eqbRHS := (X in (_ == X))%pattern (for rewriting) eq_op == the boolean relation behind the == notation. pred1 a == the singleton predicate [pred x | x == a]. pred2, pred3, pred4 == pair, triple, quad predicates. predC1 a == [pred x | x != a]. [predU1 a & A] == [pred x | (x == a) || (x \in A) ]. [predD1 A & a] == [pred x | x != a & x \in A]. predU1 a P, predD1 P a == applicative versions of the above. frel f == the relation associated with f : T -> T. := [rel x y | f x == y]. invariant f k == elements of T whose k-class is f-invariant. := [pred x | k (f x) == k x] with f : T -> T. [fun x : T => e0 with a1 |-> e1, .., a_n |-> e_n] [eta f with a1 |-> e1, .., a_n |-> e_n] == the auto-expanding function that maps x = a_i to e_i, and other values of x to e0 (resp. f x). In the first form the `: T' is optional and x can occur in a_i or e_i. Equality on an eqType is proof-irrelevant (lemma eq_irrelevance). The eqType interface is implemented for most standard datatypes: bool, unit, void, option, prod (denoted A * B), sum (denoted A + B), sig (denoted {x | P}), sigT (denoted {i : I & T}). We also define tagged_as u v == v cast as T(tag u) if tag v == tag u, else u.
• > We have u == v <=> (tag u == tag v) && (tagged u == tagged_as u v).
The subType interface supports the following operations: val == the generic injection from a subType S of T into T. For example, if u : {x : T | P}, then val u : T. val is injective because P is proof-irrelevant (P is in bool, and the is_true coercion expands to P = true). valP == the generic proof of P (val u) for u : subType P. Sub x Px == the generic constructor for a subType P; Px is a proof of P x and P should be inferred from the expected return type. insub x == the generic partial projection of T into a subType S of T. This returns an option S; if S : subType P then insub x = Some u with val u = x if P x, None if ~~ P x The insubP lemma encapsulates this dichotomy. P should be inferred from the expected return type. innew x == total (non-option) variant of insub when P = predT. {? x | P} == option {x | P} (syntax for casting insub x). insubd u0 x == the generic projection with default value u0. := odflt u0 (insub x). insigd A0 x == special case of insubd for S == {x | x \in A}, where A0 is a proof of x0 \in A. insub_eq x == transparent version of insub x that expands to Some/None when P x can evaluate. The subType P interface is most often implemented using one of: [subType for S_val] where S_val : S -> T is the first projection of a type S isomorphic to {x : T | P}. [newType for S_val] where S_val : S -> T is the projection of a type S isomorphic to wrapped T; in this case P must be predT. [subType for S_val by Srect], [newType for S_val by Srect] variants of the above where the eliminator is explicitly provided. Here S no longer needs to be syntactically identical to {x | P x} or wrapped T, but it must have a derived constructor S_Sub satisfying an eliminator Srect identical to the one the Coq Inductive command would have generated, and S_val (S_Sub x Px) (resp. S_val (S_sub x) for the newType form) must be convertible to x. variant of the above when S is a wrapper type for T (so P = predT). [subType of S], [subType of S for S_val] clones the canonical subType structure for S; if S_val is specified, then it replaces the inferred projector. Subtypes inherit the eqType structure of their base types; the generic structure should be explicitly instantiated using the [hasDecEq of S by <: ] construct to declare the equality mixin; this pattern is repeated for all the combinatorial interfaces (Choice, Countable, Finite). As noted above, such mixins should not be made Canonical. We add the following to the standard suffixes documented in ssrbool.v: 1, 2, 3, 4 -- explicit enumeration predicate for 1 (singleton), 2, 3, or 4 values.

Set Implicit Arguments.

Declare Scope eq_scope.
Declare Scope fun_delta_scope.

Definition eq_axiom T (e : rel T) := x y, reflect (x = y) (e x y).

#[mathcomp(axiom="eq_axiom"), short(type="eqType")]
HB.structure Definition Equality := { T of hasDecEq T }.

Notation "[ 'hasDecEq' 'of' T ]" := (Equality.on T%type)
(at level 0, format "[ 'hasDecEq' 'of' T ]") : form_scope.
Notation "[ 'eqType' 'of' T 'for' C ]" := (Equality.clone T%type C)
(at level 0, format "[ 'eqType' 'of' T 'for' C ]") : form_scope.
Notation "[ 'eqType' 'of' T ]" := (Equality.clone T%type _)
(at level 0, format "[ 'eqType' 'of' T ]") : form_scope.

eqE is a generic lemma that can be used to fold back recursive comparisons after using partial evaluation to simplify comparisons on concrete instances. The eqE lemma can be used e.g. like so: rewrite !eqE /= -!eqE. For instance, with the above rewrite, n.+1 == n.+1 gets simplified to n == n. For this to work, we need to declare equality mixins as canonical. Canonical declarations remove the need for specific inverses to eqE (like eqbE, eqnE, eqseqE, etc.) for new recursive comparisons, but can only be used for manifest mixing with a bespoke comparison function, and so is incompatible with PcanEqMixin and the like
• this is why the tree_hasDecEq for GenTree.tree in library choice is not
declared Canonical.
Lemma eqE (T : eqType) x : eq_op x = hasDecEq.eq_op (Equality.class T) x.

Arguments eqP {T x y} : rename.

Delimit Scope eq_scope with EQ.
Open Scope eq_scope.

Notation "x == y" := (eq_op x y)
(at level 70, no associativity) : bool_scope.
Notation "x == y :> T" := ((x : T) == (y : T))
(at level 70, y at next level) : bool_scope.
Notation "x != y" := (~~ (x == y))
(at level 70, no associativity) : bool_scope.
Notation "x != y :> T" := (~~ (x == y :> T))
(at level 70, y at next level) : bool_scope.
Notation "x =P y" := (eqP : reflect (x = y) (x == y))
(at level 70, no associativity) : eq_scope.
Notation "x =P y :> T" := (eqP : reflect (x = y :> T) (x == y :> T))
(at level 70, y at next level, no associativity) : eq_scope.

Notation eqbLHS := (X in (X == _))%pattern.
Notation eqbRHS := (X in (_ == X))%pattern.

Lemma eq_refl (T : eqType) (x : T) : x == x.
Notation eqxx := eq_refl.

Lemma eq_sym (T : eqType) (x y : T) : (x == y) = (y == x).

#[global] Hint Resolve eq_refl eq_sym : core.

Variant eq_xor_neq (T : eqType) (x y : T) : bool bool Set :=
| EqNotNeq of x = y : eq_xor_neq x y true true
| NeqNotEq of x != y : eq_xor_neq x y false false.

Lemma eqVneq (T : eqType) (x y : T) : eq_xor_neq x y (y == x) (x == y).

Arguments eqVneq {T} x y, {T x y}.

Section Contrapositives.

Variables (T1 T2 : eqType).
Implicit Types (A : pred T1) (b : bool) (P : Prop) (x : T1) (z : T2).

Lemma contraTeq b x y : (x != y ~~ b) b x = y.

Lemma contraNeq b x y : (x != y b) ~~ b x = y.

Lemma contraFeq b x y : (x != y b) b = false x = y.

Lemma contraPeq P x y : (x != y ¬ P) P x = y.

Lemma contra_not_eq P x y : (x != y P) ¬ P x = y.

Lemma contra_not_neq P x y : (x = y P) ¬ P x != y.

Lemma contraTneq b x y : (x = y ~~ b) b x != y.

Lemma contraNneq b x y : (x = y b) ~~ b x != y.

Lemma contraFneq b x y : (x = y b) b = false x != y.

Lemma contraPneq P x y : (x = y ¬ P) P x != y.

Lemma contra_eqN b x y : (b x != y) x = y ~~ b.

Lemma contra_eqF b x y : (b x != y) x = y b = false.

Lemma contra_eqT b x y : (~~ b x != y) x = y b.

Lemma contra_neqN b x y : (b x = y) x != y ~~ b.

Lemma contra_neqF b x y : (b x = y) x != y b = false.

Lemma contra_neqT b x y : (~~ b x = y) x != y b.

Lemma contra_eq_not P x y : (P x != y) x = y ¬ P.

Lemma contra_neq_not P x y : (P x = y) x != y ¬ P.

Lemma contra_eq z1 z2 x1 x2 : (x1 != x2 z1 != z2) z1 = z2 x1 = x2.

Lemma contra_neq z1 z2 x1 x2 : (x1 = x2 z1 = z2) z1 != z2 x1 != x2.

Lemma contra_neq_eq z1 z2 x1 x2 : (x1 != x2 z1 = z2) z1 != z2 x1 = x2.

Lemma contra_eq_neq z1 z2 x1 x2 : (z1 = z2 x1 != x2) x1 = x2 z1 != z2.

Lemma memPn A x : reflect {in A, y, y != x} (x \notin A).

Lemma memPnC A x : reflect {in A, y, x != y} (x \notin A).

Lemma ifN_eq R x y vT vF : x != y (if x == y then vT else vF) = vF :> R.

Lemma ifN_eqC R x y vT vF : x != y (if y == x then vT else vF) = vF :> R.

End Contrapositives.

Arguments memPn {T1 A x}.
Arguments memPnC {T1 A x}.

Theorem eq_irrelevance (T : eqType) x y : e1 e2 : x = y :> T, e1 = e2.

Corollary eq_axiomK (T : eqType) (x : T) : all_equal_to (erefl x).

We use the module system to circumvent a silly limitation that forbids using the same constant to coerce to different targets.
Module Type EqTypePredSig.
Parameter sort : eqType predArgType.
End EqTypePredSig.
Module MakeEqTypePred (eqmod : EqTypePredSig).
Coercion eqmod.sort : eqType >-> predArgType.
End MakeEqTypePred.
Module Export EqTypePred := MakeEqTypePred eqtype.Equality.

Lemma unit_eqP : Equality.axiom (fun _ _ : unittrue).

Comparison for booleans.
This is extensionally equal, but not convertible to Bool.eqb.
Definition eqb b := addb (~~ b).

Lemma eqbP : Equality.axiom eqb.

Lemma eqbE : eqb = eq_op.

Lemma bool_irrelevance (b : bool) (p1 p2 : b) : p1 = p2.

Lemma negb_add b1 b2 : ~~ (b1 (+) b2) = (b1 == b2).

Lemma negb_eqb b1 b2 : (b1 != b2) = b1 (+) b2.

Lemma eqb_id b : (b == true) = b.

Lemma eqbF_neg b : (b == false) = ~~ b.

Lemma eqb_negLR b1 b2 : (~~ b1 == b2) = (b1 == ~~ b2).

Equality-based predicates.

Notation xpred1 := (fun a1 xx == a1).
Notation xpred2 := (fun a1 a2 x(x == a1) || (x == a2)).
Notation xpred3 := (fun a1 a2 a3 x[|| x == a1, x == a2 | x == a3]).
Notation xpred4 :=
(fun a1 a2 a3 a4 x[|| x == a1, x == a2, x == a3 | x == a4]).
Notation xpredU1 := (fun a1 (p : pred _) x(x == a1) || p x).
Notation xpredC1 := (fun a1 xx != a1).
Notation xpredD1 := (fun (p : pred _) a1 x(x != a1) && p x).

Section EqPred.

Variable T : eqType.

Definition pred1 (a1 : T) := SimplPred (xpred1 a1).
Definition pred2 (a1 a2 : T) := SimplPred (xpred2 a1 a2).
Definition pred3 (a1 a2 a3 : T) := SimplPred (xpred3 a1 a2 a3).
Definition pred4 (a1 a2 a3 a4 : T) := SimplPred (xpred4 a1 a2 a3 a4).
Definition predU1 (a1 : T) p := SimplPred (xpredU1 a1 p).
Definition predC1 (a1 : T) := SimplPred (xpredC1 a1).
Definition predD1 p (a1 : T) := SimplPred (xpredD1 p a1).

Lemma pred1E : pred1 =2 eq_op.

Variables (T2 : eqType) (x y : T) (z u : T2) (b : bool).

Lemma predU1P : reflect (x = y b) ((x == y) || b).

Lemma pred2P : reflect (x = y z = u) ((x == y) || (z == u)).

Lemma predD1P : reflect (x y b) ((x != y) && b).

Lemma predU1l : x = y (x == y) || b.

Lemma predU1r : b (x == y) || b.

End EqPred.

Arguments predU1P {T x y b}.
Arguments pred2P {T T2 x y z u}.
Arguments predD1P {T x y b}.

Notation "[ 'predU1' x & A ]" := (predU1 x [mem A])
(at level 0, format "[ 'predU1' x & A ]") : fun_scope.
Notation "[ 'predD1' A & x ]" := (predD1 [mem A] x)
(at level 0, format "[ 'predD1' A & x ]") : fun_scope.

Lemmas for reflected equality and functions.

Section EqFun.

Section Exo.

Variables (aT rT : eqType) (D : pred aT) (f : aT rT) (g : rT aT).

Lemma inj_eq : injective f x y, (f x == f y) = (x == y).

Lemma can_eq : cancel f g x y, (f x == f y) = (x == y).

Lemma bij_eq : bijective f x y, (f x == f y) = (x == y).

Lemma can2_eq : cancel f g cancel g f x y, (f x == y) = (x == g y).

Lemma inj_in_eq :
{in D &, injective f} {in D &, x y, (f x == f y) = (x == y)}.

Lemma can_in_eq :
{in D, cancel f g} {in D &, x y, (f x == f y) = (x == y)}.

End Exo.

Section Endo.

Variable T : eqType.

Definition frel f := [rel x y : T | f x == y].

Lemma inv_eq f : involutive f x y : T, (f x == y) = (x == f y).

Lemma eq_frel f f' : f =1 f' frel f =2 frel f'.

End Endo.

Variable aT : Type.

The invariant of a function f wrt a projection k is the pred of points that have the same projection as their image.

Definition invariant (rT : eqType) f (k : aT rT) :=
[pred x | k (f x) == k x].

Variables (rT1 rT2 : eqType) (f : aT aT) (h : rT1 rT2) (k : aT rT1).

Lemma invariant_comp : subpred (invariant f k) (invariant f (h \o k)).

Lemma invariant_inj : injective h invariant f (h \o k) =1 invariant f k.

End EqFun.

The coercion to rel must be explicit for derived Notations to unparse.
Notation coerced_frel f := (rel_of_simpl (frel f)) (only parsing).

Section FunWith.

Variables (aT : eqType) (rT : Type).

Variant fun_delta : Type := FunDelta of aT & rT.

Definition fwith x y (f : aT rT) := [fun z if z == x then y else f z].

Definition app_fdelta df f z :=
let: FunDelta x y := df in if z == x then y else f z.

End FunWith.

Notation "x |-> y" := (FunDelta x y)
(at level 190, no associativity,
format "'[hv' x '/ ' |-> y ']'") : fun_delta_scope.

Delimit Scope fun_delta_scope with FUN_DELTA.
Arguments app_fdelta {aT rT%type} df%FUN_DELTA f z.

Notation "[ 'fun' z : T => F 'with' d1 , .. , dn ]" :=
(SimplFunDelta (fun z : T
app_fdelta d1%FUN_DELTA .. (app_fdelta dn%FUN_DELTA (fun _F)) ..))
(at level 0, z name, only parsing) : fun_scope.

Notation "[ 'fun' z => F 'with' d1 , .. , dn ]" :=
(SimplFunDelta (fun z
app_fdelta d1%FUN_DELTA .. (app_fdelta dn%FUN_DELTA (fun _F)) ..))
(at level 0, z name, format
"'[hv' [ '[' 'fun' z => '/ ' F ']' '/' 'with' '[' d1 , '/' .. , '/' dn ']' ] ']'"
) : fun_scope.

Notation "[ 'eta' f 'with' d1 , .. , dn ]" :=
(SimplFunDelta (fun _
app_fdelta d1%FUN_DELTA .. (app_fdelta dn%FUN_DELTA f) ..))
(at level 0, format
"'[hv' [ '[' 'eta' '/ ' f ']' '/' 'with' '[' d1 , '/' .. , '/' dn ']' ] ']'"
) : fun_scope.

Various EqType constructions.

Section ComparableType.

Variable T : Type.

Definition comparable := x y : T, decidable (x = y).

Hypothesis compare_T : comparable.

Definition compareb x y : bool := compare_T x y.

Lemma compareP : Equality.axiom compareb.

Definition comparableMixin := hasDecEq.Build T compareP.

End ComparableType.

Definition eq_comparable (T : eqType) : comparable T :=
fun x ydecP (x =P y).

#[key="sub_sort"]
HB.mixin Record isSub (T : Type) (P : pred T) (sub_sort : Type) := {
val_subdef : sub_sort T;
sub : x, P x sub_sort;
sub_rect : K (_ : x Px, K (@sub x Px)) u, K u;
subK_subproof : x Px, val_subdef (@sub x Px) = x
}.

#[short(type="subType")]
HB.structure Definition Sub (T : Type) (P : pred T) := { S of isSub T P S }.

Notation val := (isSub.val_subdef (Sub.on _)).
Notation "\val" := (isSub.val_subdef (Sub.on _)) (only parsing).
Notation "\val" := (isSub.val_subdef _) (only printing).

#[short(type="subEqType")]
HB.structure Definition SubEquality T (P : pred T) :=
{ sT of Equality sT & isSub T P sT}.

Section SubType.

Variables (T : Type) (P : pred T).

Generic proof that the second property holds by conversion. The vrefl_rect alias is used to flag generic proofs of the first property.
Lemma vrefl : x, P x x = x.
Definition vrefl_rect := vrefl.

Section Theory.

Variable sT : subType P.

Lemma subK x Px : val (@sub x Px) = x.

Variant sub_spec : sT Type := subSpec x Px : sub_spec (sub x Px).

Lemma subP u : sub_spec u.
BUG in elim? sT could be inferred from u

Definition insub x := if idP is ReflectT Px then Some (sub x Px) else None.

Definition insubd u0 x := odflt u0 (insub x).

Variant insub_spec x : option sT Type :=
| InsubSome u of P x & val u = x : insub_spec x (Some u)
| InsubNone of ~~ P x : insub_spec x None.

Lemma insubP x : insub_spec x (insub x).

Lemma insubT x Px : insub x = Some (sub x Px).

Lemma insubF x : P x = false insub x = None.

Lemma insubN x : ~~ P x insub x = None.

Lemma isSome_insub : ([eta insub] : pred T) =1 P.

Lemma insubK : ocancel insub val.

Lemma valP u : P (val u).

Lemma valK : pcancel val insub.

Lemma val_inj : injective val.

Lemma valKd u0 : cancel val (insubd u0).

Lemma val_insubd u0 x : val (insubd u0 x) = if P x then x else val u0.

Lemma insubdK u0 : {in P, cancel (insubd u0) val}.

Let insub_eq_aux x isPx : P x = isPx option sT :=
if isPx as b return _ = b _ then fun PxSome (sub x Px) else fun None.
Definition insub_eq x := insub_eq_aux (erefl (P x)).

Lemma insub_eqE : insub_eq =1 insub.

End Theory.

End SubType.

Arguments val {T P sT} u : rename.
Arguments sub {T P sT} x Px : rename.
Arguments vrefl {T P} x Px.
Arguments vrefl_rect {T P} x Px.
Arguments insub {T P sT} x.
Arguments insubd {T P sT} u0 x.
Arguments insubT [T] P [sT x].
Arguments val_inj {T P sT} [u1 u2] eq_u12 : rename.
Arguments valK {T P sT} u : rename.
Arguments valKd {T P sT} u0 u : rename.
Arguments insubK {T P} sT x.
Arguments insubdK {T P sT} u0 [x] Px.

Reserved Notation "[ 'subType' 'for' v ]"
(at level 0, format "[ 'subType' 'for' v ]").
Reserved Notation "[ 'isSub' 'for' v ]"
(at level 0, format "[ 'isSub' 'for' v ]").

Notation "[ 'isSub' 'for' v ]" :=
(@isSub.phant_Build _ _ _ v _ inlined_sub_rect vrefl_rect)
(only parsing) : form_scope.

Notation "[ 'isSub' 'of' T 'for' v ]" :=
(@isSub.phant_Build _ _ T v _ inlined_sub_rect vrefl_rect)
(only parsing) : form_scope.

Notation "[ 'isSub' 'for' v 'by' rec ]" :=
(@isSub.phant_Build _ _ _ v _ rec vrefl)
(at level 0, format "[ 'isSub' 'for' v 'by' rec ]") : form_scope.

Notation "[ 'isSub' 'for' v ]" := (@isSub.phant_Build _ _ _ v _ _ _)
(only printing, at level 0, format "[ 'isSub' 'for' v ]") : form_scope.

Reserved Notation "[ 'isNew' 'for' v ]"
(at level 0, format "[ 'isNew' 'for' v ]").

Definition NewMixin T U v c Urec sk :=
let Urec' P IH := Urec P (fun x : TIH x isT : P _) in
@isSub.phant_Build _ _ U v (fun x _c x) Urec' sk.

Notation "[ 'isNew' 'for' v ]" :=
(@NewMixin _ _ v _ inlined_new_rect vrefl_rect) (only parsing) : form_scope.

Notation "[ 'isNew' 'for' v ]" := (@NewMixin _ _ v _ _ _)
(only printing, at level 0, format "[ 'isNew' 'for' v ]") : form_scope.

Notation "[ 'isNew' 'of' T 'for' v ]" :=
(@NewMixin _ T v _ inlined_new_rect vrefl_rect) (only parsing) : form_scope.

Definition innew T nT x := @sub T predT nT x (erefl true).
Arguments innew {T nT}.

Lemma innew_val T nT : cancel val (@innew T nT).

Prenex Implicits and renaming.
Notation sval := (@proj1_sig _ _).
Notation "@ 'sval'" := (@proj1_sig) (at level 10, format "@ 'sval'").

Section SigProj.

Variables (T : Type) (P Q : T Prop).

Lemma svalP : u : sig P, P (sval u).

Definition s2val (u : sig2 P Q) := let: exist2 x _ _ := u in x.

Lemma s2valP u : P (s2val u).

Lemma s2valP' u : Q (s2val u).

End SigProj.

Shorthand for sigma types over collective predicates.
Notation "{ x 'in' A }" := {x | x \in A}
(at level 0, x at level 99, format "{ x 'in' A }") : type_scope.
Notation "{ x 'in' A | P }" := {x | (x \in A) && P}
(at level 0, x at level 99, format "{ x 'in' A | P }") : type_scope.

Shorthand for the return type of insub.
Notation "{ ? x : T | P }" := (option {x : T | is_true P})
(at level 0, x at level 99, only parsing) : type_scope.
Notation "{ ? x | P }" := {? x : _ | P}
(at level 0, x at level 99, format "{ ? x | P }") : type_scope.
Notation "{ ? x 'in' A }" := {? x | x \in A}
(at level 0, x at level 99, format "{ ? x 'in' A }") : type_scope.
Notation "{ ? x 'in' A | P }" := {? x | (x \in A) && P}
(at level 0, x at level 99, format "{ ? x 'in' A | P }") : type_scope.

A variant of injection with default that infers a collective predicate from the membership proof for the default value.
Definition insigd T (A : mem_pred T) x (Ax : in_mem x A) :=
insubd (exist [eta A] x Ax).

There should be a rel definition for the subType equality op, but this seems to cause the simpl tactic to diverge on expressions involving == on 4+ nested subTypes in a "strict" position (e.g., after ~~). Definition feq f := [rel x y | f x == f y].

Section TransferType.

Variables (T T' : Type) (f : T T').

Definition inj_type of injective f : Type := T.
Definition pcan_type g of pcancel f g : Type := T.
Definition can_type g of cancel f g : Type := T.

End TransferType.

Section TransferEqType.

Variables (T : Type) (eT : eqType) (f : T eT).

Lemma inj_eqAxiom : injective f Equality.axiom (fun x yf x == f y).

Definition InjEqMixin f_inj := hasDecEq.Build T (inj_eqAxiom f_inj).

Definition PcanEqMixin g (fK : pcancel f g) := InjEqMixin (pcan_inj fK).

Definition CanEqMixin g (fK : cancel f g) := InjEqMixin (can_inj fK).

End TransferEqType.

Definition sub_type_of T (P : pred T) (sT : subType P) of phant sT : Type := sT.
Notation sub_type T := (sub_type_of (Phant T)).

Section SubEqType.

Variables (T : eqType) (P : pred T) (sT : subType P).

Lemma val_eqP : ev_ax sT val.

End SubEqType.

Lemma val_eqE (T : eqType) (P : pred T) (sT : subEqType P)
(u v : sT) : (val u == val v) = (u == v).

Arguments val_eqP {T P sT x y}.

Notation "[ 'Equality' 'of' T 'by' <: ]" := (Equality.copy T%type (sub_type T))
(at level 0, format "[ 'Equality' 'of' T 'by' <: ]") : form_scope.
#[deprecated(since="mathcomp 2.0.0",
note="Use [Equality of _ by <:] or [hasDecEq of _ by <:] instead")]
Notation "[ 'eqMixin' 'of' T 'by' <: ]" :=
(hasDecEq.Build (T : Type) (@val_eqP _ _ _))
(at level 0, format "[ 'eqMixin' 'of' T 'by' <: ]") : form_scope.
Notation "[ 'hasDecEq' 'of' T 'by' <: ]" :=
(hasDecEq.Build (T : Type) (@val_eqP _ _ _))
(at level 0, format "[ 'hasDecEq' 'of' T 'by' <: ]") : form_scope.

Section ProdEqType.

Variable T1 T2 : eqType.

Definition pair_eq : rel (T1 × T2) := fun u v(u.1 == v.1) && (u.2 == v.2).

Lemma pair_eqP : Equality.axiom pair_eq.

Lemma pair_eqE : pair_eq = eq_op :> rel _.

Lemma xpair_eqE (x1 y1 : T1) (x2 y2 : T2) :
((x1, x2) == (y1, y2)) = ((x1 == y1) && (x2 == y2)).

Lemma pair_eq1 (u v : T1 × T2) : u == v u.1 == v.1.

Lemma pair_eq2 (u v : T1 × T2) : u == v u.2 == v.2.

End ProdEqType.

Arguments pair_eq {T1 T2} u v /.
Arguments pair_eqP {T1 T2}.

Definition predX T1 T2 (p1 : pred T1) (p2 : pred T2) :=
[pred z | p1 z.1 & p2 z.2].

Notation "[ 'predX' A1 & A2 ]" := (predX [mem A1] [mem A2])
(at level 0, format "[ 'predX' A1 & A2 ]") : fun_scope.

Section OptionEqType.

Variable T : eqType.

Definition opt_eq (u v : option T) : bool :=
oapp (fun xoapp (eq_op x) false v) (~~ v) u.

Lemma opt_eqP : Equality.axiom opt_eq.

End OptionEqType.

Arguments opt_eq {T} !u !v.

Section TaggedAs.

Variables (I : eqType) (T_ : I Type).
Implicit Types u v : {i : I & T_ i}.

Definition tagged_as u v :=
if tag u =P tag v is ReflectT eq_uv then
eq_rect_r T_ (tagged v) eq_uv
else tagged u.

Lemma tagged_asE u x : tagged_as u (Tagged T_ x) = x.

End TaggedAs.

Section TagEqType.

Variables (I : eqType) (T_ : I eqType).
Implicit Types u v : {i : I & T_ i}.

Definition tag_eq u v := (tag u == tag v) && (tagged u == tagged_as u v).

Lemma tag_eqP : Equality.axiom tag_eq.

Lemma tag_eqE : tag_eq = eq_op.

Lemma eq_tag u v : u == v tag u = tag v.

Lemma eq_Tagged u x :(u == Tagged _ x) = (tagged u == x).

End TagEqType.

Arguments tag_eq {I T_} !u !v.
Arguments tag_eqP {I T_ x y}.

Section SumEqType.

Variables T1 T2 : eqType.
Implicit Types u v : T1 + T2.

Definition sum_eq u v :=
match u, v with
| inl x, inl y | inr x, inr yx == y
| _, _false
end.

Lemma sum_eqP : Equality.axiom sum_eq.

Lemma sum_eqE : sum_eq = eq_op.

End SumEqType.

Arguments sum_eq {T1 T2} !u !v.
Arguments sum_eqP {T1 T2 x y}.

Section MonoHomoTheory.

Variables (aT rT : eqType) (f : aT rT).
Variables (aR aR' : rel aT) (rR rR' : rel rT).

Hypothesis aR_refl : reflexive aR.
Hypothesis rR_refl : reflexive rR.
Hypothesis aR'E : x y, aR' x y = (x != y) && (aR x y).
Hypothesis rR'E : x y, rR' x y = (x != y) && (rR x y).

Let aRE x y : aR x y = (x == y) || (aR' x y).
Let rRE x y : rR x y = (x == y) || (rR' x y).

Section InDom.
Variable D : pred aT.

Section DifferentDom.
Variable D' : pred aT.

Lemma homoW_in : {in D & D', {homo f : x y / aR' x y >-> rR' x y}}
{in D & D', {homo f : x y / aR x y >-> rR x y}}.

Lemma inj_homo_in : {in D & D', injective f}
{in D & D', {homo f : x y / aR x y >-> rR x y}}
{in D & D', {homo f : x y / aR' x y >-> rR' x y}}.

End DifferentDom.

Hypothesis aR_anti : antisymmetric aR.
Hypothesis rR_anti : antisymmetric rR.

Lemma mono_inj_in : {in D &, {mono f : x y / aR x y >-> rR x y}}
{in D &, injective f}.

Lemma anti_mono_in : {in D &, {mono f : x y / aR x y >-> rR x y}}
{in D &, {mono f : x y / aR' x y >-> rR' x y}}.

Lemma total_homo_mono_in : total aR
{in D &, {homo f : x y / aR' x y >-> rR' x y}}
{in D &, {mono f : x y / aR x y >-> rR x y}}.

End InDom.

Let D := @predT aT.

Lemma homoW : {homo f : x y / aR' x y >-> rR' x y}
{homo f : x y / aR x y >-> rR x y}.

Lemma inj_homo : injective f
{homo f : x y / aR x y >-> rR x y}
{homo f : x y / aR' x y >-> rR' x y}.

Hypothesis aR_anti : antisymmetric aR.
Hypothesis rR_anti : antisymmetric rR.

Lemma mono_inj : {mono f : x y / aR x y >-> rR x y} injective f.

Lemma anti_mono : {mono f : x y / aR x y >-> rR x y}
{mono f : x y / aR' x y >-> rR' x y}.

Lemma total_homo_mono : total aR
{homo f : x y / aR' x y >-> rR' x y}
{mono f : x y / aR x y >-> rR x y}.

End MonoHomoTheory.