Tweak code related to canonical mixins

Remove some unused canonical mixins.
  Change simplification behavior of concrete comparison functions to allow for
better simplification using unfolding and sebsequent folding back e.g. with
`rewrite !eqE /= -!eqE`.
  A bit of cleanup for `Prenex Implicits` declarations.
  Document some explanations by G. Gonthier.

5 files changed, 41 insertions, 22 deletions

diff --git a/mathcomp/algebra/vector.v b/mathcomp/algebra/vector.v
index a2346a2..cda2876 100644
--- a/mathcomp/algebra/vector.v
+++ b/mathcomp/algebra/vector.v
@@ -1302,7 +1302,7 @@ Section LfunZmodType.
 Variables (R : ringType) (aT rT : vectType R).
 Implicit Types f g h : 'Hom(aT, rT).
 
-Canonical lfun_eqMixin := Eval hnf in [eqMixin of 'Hom(aT, rT) by <:].
+Definition lfun_eqMixin := Eval hnf in [eqMixin of 'Hom(aT, rT) by <:].
 Canonical lfun_eqType := EqType 'Hom(aT, rT) lfun_eqMixin.
 Definition lfun_choiceMixin := [choiceMixin of 'Hom(aT, rT) by <:].
 Canonical lfun_choiceType := ChoiceType 'Hom(aT, rT) lfun_choiceMixin.
diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v
index cd907ce..76b0521 100644
--- a/mathcomp/ssreflect/eqtype.v
+++ b/mathcomp/ssreflect/eqtype.v
@@ -107,7 +107,7 @@ Require Import ssrfun ssrbool.
 (*   [eqMixin 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 mad Canonical.                                   *)
+(* 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.                                                   *)
@@ -155,6 +155,17 @@ Export Equality.Exports.
 
 Definition eq_op T := Equality.op (Equality.class T).
 
+(* 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_eqMixin for GenTree.tree in library choice is not   *)
+(* declared Canonical.                                                        *)
 Lemma eqE T x : eq_op x = Equality.op (Equality.class T) x.
 Proof. by []. Qed.
 
@@ -745,7 +756,7 @@ Section ProdEqType.
 
 Variable T1 T2 : eqType.
 
-Definition pair_eq := [rel u v : T1 * T2 | (u.1 == v.1) && (u.2 == v.2)].
+Definition pair_eq : rel (T1 * T2) := fun u v => (u.1 == v.1) && (u.2 == v.2).
 
 Lemma pair_eqP : Equality.axiom pair_eq.
 Proof.
@@ -753,7 +764,7 @@ move=> [x1 x2] [y1 y2] /=; apply: (iffP andP) => [[]|[<- <-]] //=.
 by do 2!move/eqP->.
 Qed.
 
-Definition prod_eqMixin := EqMixin pair_eqP.
+Canonical prod_eqMixin := EqMixin pair_eqP.
 Canonical prod_eqType := Eval hnf in EqType (T1 * T2) prod_eqMixin.
 
 Lemma pair_eqE : pair_eq = eq_op :> rel _. Proof. by []. Qed.
@@ -770,9 +781,8 @@ Proof. by case/andP. Qed.
 
 End ProdEqType.
 
-Arguments pair_eqP [T1 T2].
-
-Prenex Implicits pair_eqP.
+Arguments pair_eq {T1 T2} _ _ /.
+Arguments pair_eqP {T1 T2}.
 
 Definition predX T1 T2 (p1 : pred T1) (p2 : pred T2) :=
   [pred z | p1 z.1 & p2 z.2].
@@ -797,6 +807,8 @@ Canonical option_eqType := Eval hnf in EqType (option T) option_eqMixin.
 
 End OptionEqType.
 
+Arguments opt_eq {T} !_ !_.
+
 Section TaggedAs.
 
 Variables (I : eqType) (T_ : I -> Type).
@@ -841,8 +853,8 @@ Proof. by rewrite -tag_eqE /tag_eq eqxx tagged_asE. Qed.
 
 End TagEqType.
 
-Arguments tag_eqP [I T_ x y].
-Prenex Implicits tag_eqP.
+Arguments tag_eq {I T_} !_ !_.
+Arguments tag_eqP {I T_ x y}.
 
 Section SumEqType.
 
@@ -865,5 +877,5 @@ Lemma sum_eqE : sum_eq = eq_op. Proof. by []. Qed.
 
 End SumEqType.
 
-Arguments sum_eqP [T1 T2 x y].
-Prenex Implicits sum_eqP.
+Arguments sum_eq {T1 T2} !_ !_.
+Arguments sum_eqP {T1 T2 x y}.
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v
index 4e4c77b..9c13df3 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/mathcomp/ssreflect/seq.v
@@ -1309,14 +1309,14 @@ Definition inE := (mem_seq1, in_cons, inE).
 
 Prenex Implicits mem_seq1 uniq undup index.
 
-Arguments eqseqP [T x y].
-Arguments hasP [T a s].
-Arguments hasPn [T a s].
-Arguments allP [T a s].
-Arguments allPn [T a s].
-Arguments nseqP [T n x y].
-Arguments count_memPn [T x s].
-Prenex Implicits eqseqP hasP hasPn allP allPn nseqP count_memPn.
+Arguments eqseq {T} !_ !_.
+Arguments eqseqP {T x y}.
+Arguments hasP {T a s}.
+Arguments hasPn {T a s}.
+Arguments allP {T a s}.
+Arguments allPn {T a s}.
+Arguments nseqP {T n x y}.
+Arguments count_memPn {T x s}.
 
 Section NthTheory.
 
diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v
index f7cd700..78d50b6 100644
--- a/mathcomp/ssreflect/ssrnat.v
+++ b/mathcomp/ssreflect/ssrnat.v
@@ -174,8 +174,8 @@ Qed.
 Canonical nat_eqMixin := EqMixin eqnP.
 Canonical nat_eqType := Eval hnf in EqType nat nat_eqMixin.
 
-Arguments eqnP [x y].
-Prenex Implicits eqnP.
+Arguments eqn !_ !_.
+Arguments eqnP {x y}.
 
 Lemma eqnE : eqn = eq_op. Proof. by []. Qed.
 
@@ -1454,6 +1454,8 @@ Qed.
 Canonical bin_nat_eqMixin := EqMixin eq_binP.
 Canonical bin_nat_eqType := Eval hnf in EqType N bin_nat_eqMixin.
 
+Arguments N.eqb !_ !_.
+
 Section NumberInterpretation.
 
 Import BinPos.
diff --git a/mathcomp/ssreflect/tuple.v b/mathcomp/ssreflect/tuple.v
index 64585f6..38e3dbe 100644
--- a/mathcomp/ssreflect/tuple.v
+++ b/mathcomp/ssreflect/tuple.v
@@ -360,7 +360,12 @@ Section UseFinTuple.
 
 Variables (n : nat) (T : finType).
 
-Canonical tuple_finMixin := Eval hnf in FinMixin (@FinTuple.enumP n T).
+(* tuple_finMixin could, in principle, be made Canonical to allow for folding *)
+(* Finite.enum of a finite tuple type (see comments around eqE in eqtype.v),  *)
+(* but in practice it will not work because the mixin_enum projector          *)
+(* has been burried under an opaque alias, to avoid some performance issues   *)
+(* during type inference.                                                     *)
+Definition tuple_finMixin := Eval hnf in FinMixin (@FinTuple.enumP n T).
 Canonical tuple_finType := Eval hnf in FinType (n.-tuple T) tuple_finMixin.
 Canonical tuple_subFinType := Eval hnf in [subFinType of n.-tuple T].