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.

Types with a decidable equality NB: See CONTRIBUTING.md for an introduction to HB concepts and commands. This file defines two "base" combinatorial structures: eqType == types with a decidable equality The HB class is called Equality. The equality operation on an eqType is proof-irrelevant (lemma eq_irrelevance). The main notation is the boolean equality "==", see below. subType P == types isomorphic to {x : T | P x} with P : pred T for some type T The HB class is called SubType. subEqType P == join of eqType and subType P The HB class is called SubEquality. The eqType interface supports the following operations (in bool_scope): 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 (see lemma eqE below for generic folding of equality predicates) eqP == proof of Equality.axiom eq_op behind the =P notation 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 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 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

Sub

Specific notations

[isSub of S for S_val] == subtype for S where S_val : S -> T is the first projection of a type S isomorphic to {x : T | P}; if S_val is specified, then it replaces the inferred projector. [isSub for S_val] := [isSub of _ for S_val] It clones the canonical subType structure for S. [isNew of S for S_val] == subtype for S where S_val : S -> T is the projection of a type S isomorphic to T; in this case P must be predT [isNew for S_val] := [isNew of _ for S_val] [isSub for S_val by Srect], [isNew 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). Subtypes inherit the eqType structure of their base types; the generic structure should be explicitly instantiated using the [Equality of S by <: ] construct; this pattern is repeated for all the combinatorial interfaces (Choice, Countable, Finite). List of factories with a dedicated alias (not generated automatically): inj_type injf == alias of T to copy an interface from another T' already equipped with it and injf : injective f with f : T -> T' pcan_type fK == alias of T to similarly derive an interface from f and a left inverse partial function g and fK : pcancel f g can_type fK == alias of T to similarly derive an interface from f and a left inverse function g and fK : cancel f g sub_type sT == alias of sT : subType _ comparable T <-> equality on T is decidable. := forall x y : T, decidable (x = y) comparableMixin compT == equality mixin for compT : comparable T 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 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 }.

#[deprecated(since="mathcomp 2.0.0", note="Use Equality.clone instead.")]
Notation "[ 'eqType' 'of' T 'for' C ]" := (Equality.clone T%type C)
  (at level 0, format "[ 'eqType' 'of' T 'for' C ]") : form_scope.
#[deprecated(since="mathcomp 2.0.0", note="Use Equality.clone instead.")]
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 [in A])
  (at level 0, format "[ 'predU1' x & A ]") : fun_scope.
Notation "[ 'predD1' A & x ]" := (predD1 [in 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 SubType (T : Type) (P : pred T) := { S of isSub T P S }.

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

#[deprecated(since="mathcomp 2.0.0", note="Use Sub instead.")]
Notation sub := Sub.

#[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.

Local Notation val := (isSub.val_subdef (SubType.on sT)).
Local Notation Sub := (@Sub _ _ sT).

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.

#[deprecated(since="mathcomp 2.0.0", note="Use SubK instead.")]
Notation subK := SubK.
#[deprecated(since="mathcomp 2.0.0", note="Use Sub_spec instead.")]
Notation sub_spec := Sub_spec.
#[deprecated(since="mathcomp 2.0.0", note="Use SubP instead.")]
Notation subP := SubP.

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.

Local Notation inlined_sub_rect :=
  (fun K K_S ulet (x, Px) as u return K u := u in K_S x Px).

Local Notation inlined_new_rect :=
  (fun K K_S ulet (x) as u return K u := u in K_S x).

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).


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 deprecated_InjEqMixin f_inj := hasDecEq.Build T (inj_eqAxiom f_inj).
Definition deprecated_PcanEqMixin g (fK : pcancel f g) :=
  deprecated_InjEqMixin (pcan_inj fK).
Definition deprecated_CanEqMixin g (fK : cancel f g) :=
  deprecated_InjEqMixin (can_inj fK).

End TransferEqType.

#[deprecated(since="mathcomp 2.0.0",
  note="Use Equality.copy T (inj_type f_inj) instead")]
Notation InjEqMixin := deprecated_InjEqMixin.
#[deprecated(since="mathcomp 2.0.0",
  note="Use Equality.copy T (pcan_type fK) instead")]
Notation PcanEqMixin := deprecated_PcanEqMixin.
#[deprecated(since="mathcomp 2.0.0",
  note="Use Equality.copy T (can_type fK) instead")]
Notation CanEqMixin := deprecated_CanEqMixin.

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).

Local Notation ev_ax := (fun T v ⇒ @Equality.axiom T (fun x yv x == v y)).
Lemma val_eqP : ev_ax sT val.

#[hnf] HB.instance Definition _ := Equality.copy (sub_type sT) (pcan_type valK).

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%type))
  (at level 0, format "[ 'Equality' 'of' T 'by' <: ]") : form_scope.
#[deprecated(since="mathcomp 2.0.0", note="Use [Equality of _ by <:] instead.")]
Notation "[ 'eqMixin' 'of' T 'by' <: ]" := [Equality of T%type by <:]
  (at level 0, format "[ 'eqMixin' '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 [in A1] [in 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.