Generalise use of `{pred T}` from coq/coq#9995

Use `{pred T}` systematically for generic _collective_ boolean
predicate.
Use `PredType` to construct `predType` instances.
Instrument core `ssreflect` files to replicate these and other new
features introduces by coq/coq#9555 (`nonPropType` interface,
`simpl_rel` that simplifies with `inE`).

2 files changed, 14 insertions, 12 deletions

diff --git a/mathcomp/field/algC.v b/mathcomp/field/algC.v
index 86e9e30..e1fd4d1 100644
--- a/mathcomp/field/algC.v
+++ b/mathcomp/field/algC.v
@@ -554,13 +554,13 @@ Notation algCnumClosedField := numClosedFieldType.
 Notation Creal := (@Num.Def.Rreal numDomainType).
 
 Definition getCrat := let: GetCrat_spec CtoQ _ := getCrat_subproof in CtoQ.
-Definition Crat : pred_class := fun x : algC => ratr (getCrat x) == x.
+Definition Crat : {pred algC} := fun x => ratr (getCrat x) == x.
 
 Definition floorC x := sval (floorC_subproof x).
-Definition Cint : pred_class := fun x : algC => (floorC x)%:~R == x.
+Definition Cint : {pred algC} := fun x => (floorC x)%:~R == x.
 
 Definition truncC x := if x >= 0 then `|floorC x|%N else 0%N.
-Definition Cnat : pred_class := fun x : algC => (truncC x)%:R == x.
+Definition Cnat : {pred algC} := fun x => (truncC x)%:R == x.
 
 Definition minCpoly x : {poly algC} :=
   let: exist2 p _ _ := minCpoly_subproof x in map_poly ratr p.
@@ -573,8 +573,8 @@ Lemma nCdivE (p : nat) : p = p%:R :> divisor. Proof. by []. Qed.
 Lemma zCdivE (p : int) : p = p%:~R :> divisor. Proof. by []. Qed.
 Definition CdivE := (nCdivE, zCdivE).
 
-Definition dvdC (x : divisor) : pred_class :=
-   fun y : algC => if x == 0 then y == 0 else y / x \in Cint.
+Definition dvdC (x : divisor) : {pred algC} :=
+   fun y => if x == 0 then y == 0 else y / x \in Cint.
 Notation "x %| y" := (y \in dvdC x) : C_expanded_scope.
 Notation "x %| y" := (@in_mem divisor y (mem (dvdC x))) : C_scope.
 
@@ -715,7 +715,8 @@ Proof. by move=> _ _ /CintP[m1 ->] /CintP[m2 ->]; rewrite -rmorphM !intCK. Qed.
 Lemma floorCX n : {in Cint, {morph floorC : x / x ^+ n}}.
 Proof. by move=> _ /CintP[m ->]; rewrite -rmorphX !intCK. Qed.
 
-Lemma rpred_Cint S (ringS : subringPred S) (kS : keyed_pred ringS) x :
+Lemma rpred_Cint
+        (S : {pred algC}) (ringS : subringPred S) (kS : keyed_pred ringS) x :
   x \in Cint -> x \in kS.
 Proof. by case/CintP=> m ->; apply: rpred_int. Qed.
 
@@ -805,7 +806,8 @@ Proof. by move=> _ _ /CnatP[n1 ->] /CnatP[n2 ->]; rewrite -natrM !natCK. Qed.
 Lemma truncCX n : {in Cnat, {morph truncC : x / x ^+ n >-> (x ^ n)%N}}.
 Proof. by move=> _ /CnatP[n1 ->]; rewrite -natrX !natCK. Qed.
 
-Lemma rpred_Cnat S (ringS : semiringPred S) (kS : keyed_pred ringS) x :
+Lemma rpred_Cnat
+        (S : {pred algC}) (ringS : semiringPred S) (kS : keyed_pred ringS) x :
   x \in Cnat -> x \in kS.
 Proof. by case/CnatP=> n ->; apply: rpred_nat. Qed.
 
@@ -1110,7 +1112,8 @@ Canonical Crat_subringPred := SubringPred Crat_divring_closed.
 Canonical Crat_sdivrPred := SdivrPred Crat_divring_closed.
 Canonical Crat_divringPred := DivringPred Crat_divring_closed.
 
-Lemma rpred_Crat S (ringS : divringPred S) (kS : keyed_pred ringS) :
+Lemma rpred_Crat
+        (S : {pred algC}) (ringS : divringPred S) (kS : keyed_pred ringS) :
   {subset Crat <= kS}.
 Proof. by move=> _ /CratP[a ->]; apply: rpred_rat. Qed.
 
diff --git a/mathcomp/field/algnum.v b/mathcomp/field/algnum.v
index 144a82e..3f25ae6 100644
--- a/mathcomp/field/algnum.v
+++ b/mathcomp/field/algnum.v
@@ -505,8 +505,7 @@ Qed.
 
 (* Algebraic integers. *)
 
-Definition Aint : pred_class :=
-  fun x : algC => minCpoly x \is a polyOver Cint.
+Definition Aint : {pred algC} := fun x => minCpoly x \is a polyOver Cint.
 Fact Aint_key : pred_key Aint. Proof. by []. Qed.
 Canonical Aint_keyed := KeyedPred Aint_key.
 
@@ -673,8 +672,8 @@ Lemma Aint_aut (nu : {rmorphism algC -> algC}) x :
   (nu x \in Aint) = (x \in Aint).
 Proof. by rewrite !unfold_in minCpoly_aut. Qed.
 
-Definition dvdA (e : Algebraics.divisor) : pred_class :=
-  fun z : algC => if e == 0 then z == 0 else z / e \in Aint.
+Definition dvdA (e : Algebraics.divisor) : {pred algC} :=
+  fun z => if e == 0 then z == 0 else z / e \in Aint.
 Fact dvdA_key e : pred_key (dvdA e). Proof. by []. Qed.
 Canonical dvdA_keyed e := KeyedPred (dvdA_key e).
 Delimit Scope algC_scope with A.