aboutsummaryrefslogtreecommitdiff
path: root/mathcomp
diff options
context:
space:
mode:
Diffstat (limited to 'mathcomp')
-rw-r--r--mathcomp/algebra/interval.v2
-rw-r--r--mathcomp/algebra/poly.v15
-rw-r--r--mathcomp/algebra/rat.v3
-rw-r--r--mathcomp/algebra/ring_quotient.v41
-rw-r--r--mathcomp/algebra/ssralg.v43
-rw-r--r--mathcomp/algebra/ssrnum.v19
-rw-r--r--mathcomp/algebra/vector.v6
-rw-r--r--mathcomp/character/character.v4
-rw-r--r--mathcomp/character/classfun.v4
-rw-r--r--mathcomp/character/vcharacter.v6
-rw-r--r--mathcomp/field/algC.v19
-rw-r--r--mathcomp/field/algnum.v7
-rw-r--r--mathcomp/fingroup/fingroup.v28
-rw-r--r--mathcomp/solvable/gfunctor.v4
-rw-r--r--mathcomp/ssreflect/finfun.v4
-rw-r--r--mathcomp/ssreflect/fingraph.v15
-rw-r--r--mathcomp/ssreflect/finset.v45
-rw-r--r--mathcomp/ssreflect/fintype.v70
-rw-r--r--mathcomp/ssreflect/prime.v72
-rw-r--r--mathcomp/ssreflect/seq.v21
-rw-r--r--mathcomp/ssreflect/ssrbool.v41
-rw-r--r--mathcomp/ssreflect/ssreflect.v28
-rw-r--r--mathcomp/ssreflect/ssrfun.v3
-rw-r--r--mathcomp/ssreflect/ssrnat.v6
-rw-r--r--mathcomp/ssreflect/tuple.v7
25 files changed, 283 insertions, 230 deletions
diff --git a/mathcomp/algebra/interval.v b/mathcomp/algebra/interval.v
index 7c1ab8f..eb0785f 100644
--- a/mathcomp/algebra/interval.v
+++ b/mathcomp/algebra/interval.v
@@ -331,7 +331,7 @@ Definition pred_of_itv (i : interval R) : pred R :=
| BOpen_if b ub => x <= ub ?< if b
| BInfty => true
end].
-Canonical Structure itvPredType := Eval hnf in mkPredType pred_of_itv.
+Canonical Structure itvPredType := PredType pred_of_itv.
(* we compute a set of rewrite rules associated to an interval *)
Definition itv_rewrite (i : interval R) x : Type :=
diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v
index e0a8e5d..d898774 100644
--- a/mathcomp/algebra/poly.v
+++ b/mathcomp/algebra/poly.v
@@ -1298,13 +1298,14 @@ Qed.
(* Lifting a ring predicate to polynomials. *)
-Definition polyOver (S : pred_class) :=
- [qualify a p : {poly R} | all (mem S) p].
+Implicit Type S : {pred R}.
+
+Definition polyOver S := [qualify a p : {poly R} | all (mem S) p].
Fact polyOver_key S : pred_key (polyOver S). Proof. by []. Qed.
Canonical polyOver_keyed S := KeyedQualifier (polyOver_key S).
-Lemma polyOverS (S1 S2 : pred_class) :
+Lemma polyOverS (S1 S2 : {pred R}) :
{subset S1 <= S2} -> {subset polyOver S1 <= polyOver S2}.
Proof.
by move=> sS12 p /(all_nthP 0)S1p; apply/(all_nthP 0)=> i /S1p; apply: sS12.
@@ -1313,7 +1314,7 @@ Qed.
Lemma polyOver0 S : 0 \is a polyOver S.
Proof. by rewrite qualifE polyseq0. Qed.
-Lemma polyOver_poly (S : pred_class) n E :
+Lemma polyOver_poly S n E :
(forall i, i < n -> E i \in S) -> \poly_(i < n) E i \is a polyOver S.
Proof.
move=> S_E; apply/(all_nthP 0)=> i lt_i_p /=; rewrite coef_poly.
@@ -1322,7 +1323,7 @@ Qed.
Section PolyOverAdd.
-Variables (S : predPredType R) (addS : addrPred S) (kS : keyed_pred addS).
+Variables (S : {pred R}) (addS : addrPred S) (kS : keyed_pred addS).
Lemma polyOverP {p} : reflect (forall i, p`_i \in kS) (p \in polyOver kS).
Proof.
@@ -1354,7 +1355,7 @@ Canonical polyOver_zmodPred S addS kS := ZmodPred (@polyOverNr S addS kS).
Section PolyOverSemiring.
-Context (S : pred_class) (ringS : @semiringPred R S) (kS : keyed_pred ringS).
+Variables (S : {pred R}) (ringS : semiringPred S) (kS : keyed_pred ringS).
Fact polyOver_mulr_closed : mulr_closed (polyOver kS).
Proof.
@@ -1382,7 +1383,7 @@ End PolyOverSemiring.
Section PolyOverRing.
-Context (S : pred_class) (ringS : @subringPred R S) (kS : keyed_pred ringS).
+Variables (S : {pred R}) (ringS : subringPred S) (kS : keyed_pred ringS).
Canonical polyOver_smulrPred := SmulrPred (polyOver_mulr_closed kS).
Canonical polyOver_subringPred := SubringPred (polyOver_mulr_closed kS).
diff --git a/mathcomp/algebra/rat.v b/mathcomp/algebra/rat.v
index 8654fd1..228a824 100644
--- a/mathcomp/algebra/rat.v
+++ b/mathcomp/algebra/rat.v
@@ -689,7 +689,8 @@ Proof. by rewrite /ratr numq_int denq_int divr1. Qed.
Lemma ratr_nat n : ratr n%:R = n%:R.
Proof. exact: (ratr_int n). Qed.
-Lemma rpred_rat S (ringS : @divringPred R S) (kS : keyed_pred ringS) a :
+Lemma rpred_rat (S : {pred R}) (ringS : divringPred S) (kS : keyed_pred ringS)
+ a :
ratr a \in kS.
Proof. by rewrite rpred_div ?rpred_int. Qed.
diff --git a/mathcomp/algebra/ring_quotient.v b/mathcomp/algebra/ring_quotient.v
index 7e6bbf3..22aa279 100644
--- a/mathcomp/algebra/ring_quotient.v
+++ b/mathcomp/algebra/ring_quotient.v
@@ -38,9 +38,9 @@ From mathcomp Require Import ssrfun seq ssralg generic_quotient.
(* unitRingQuotType ... u i == As in the previous cases, instance of unit *)
(* ring whose unit predicate is obtained from *)
(* u and the inverse from i. *)
-(* idealr R S == (S : pred R) is a non-trivial, decidable, *)
+(* idealr R S == S : {pred R} is a non-trivial, decidable, *)
(* right ideal of the ring R. *)
-(* prime_idealr R S == (S : pred R) is a non-trivial, decidable, *)
+(* prime_idealr R S == S : {pred R} is a non-trivial, decidable, *)
(* right, prime ideal of the ring R. *)
(* *)
(* The formalization of ideals features the following constructions: *)
@@ -52,22 +52,21 @@ From mathcomp Require Import ssrfun seq ssralg generic_quotient.
(* ring R represents a (right) ideal. This *)
(* implies its being a proper_ideal. *)
(* *)
-(* MkIdeal idealS == packs idealS : proper_ideal S into an *)
-(* idealr S interface structure associating the *)
+(* MkIdeal idealS == packs idealS : proper_ideal S into an idealr S *)
+(* interface structure associating the *)
(* idealr_closed property to the canonical *)
(* pred_key S (see ssrbool), which must already *)
-(* be an zmodPred (see ssralg). *)
+(* be a zmodPred (see ssralg). *)
(* MkPrimeIdeal pidealS == packs pidealS : prime_idealr_closed S into a *)
(* prime_idealr S interface structure associating *)
(* the prime_idealr_closed property to the *)
(* canonical pred_key S (see ssrbool), which must *)
(* already be an idealr (see above). *)
(* {ideal_quot kI} == quotient by the keyed (right) ideal predicate *)
-(* kI of a commutative ring R. Note that we indeed*)
-(* only provide canonical structures of ring *)
-(* quotients for the case of commutative rings, *)
-(* for which a right ideal is obviously a *)
-(* two-sided ideal. *)
+(* kI of a commutative ring R. Note that we only *)
+(* provide canonical structures of ring quotients *)
+(* for commutative rings, in which a right ideal *)
+(* is obviously a two-sided ideal. *)
(* *)
(* Note : *)
(* if (I : pred R) is a predicate over a ring R and (ideal : idealr I) is an *)
@@ -425,13 +424,13 @@ Notation UnitRingQuotMixin Q mU mV :=
Section IdealDef.
-Definition proper_ideal (R : ringType) (S : predPredType R) : Prop :=
+Definition proper_ideal (R : ringType) (S : {pred R}) : Prop :=
1 \notin S /\ forall a, {in S, forall u, a * u \in S}.
-Definition prime_idealr_closed (R : ringType) (S : predPredType R) : Prop :=
+Definition prime_idealr_closed (R : ringType) (S : {pred R}) : Prop :=
forall u v, u * v \in S -> (u \in S) || (v \in S).
-Definition idealr_closed (R : ringType) (S : predPredType R) :=
+Definition idealr_closed (R : ringType) (S : {pred R}) :=
[/\ 0 \in S, 1 \notin S & forall a, {in S &, forall u v, a * u + v \in S}].
Lemma idealr_closed_nontrivial R S : @idealr_closed R S -> proper_ideal S.
@@ -443,22 +442,22 @@ Proof. by case=> S0 _ hS; split=> // x y xS yS; rewrite -mulN1r addrC hS. Qed.
Coercion idealr_closedB : idealr_closed >-> zmod_closed.
Coercion idealr_closed_nontrivial : idealr_closed >-> proper_ideal.
-Structure idealr (R : ringType) (S : predPredType R) := MkIdeal {
+Structure idealr (R : ringType) (S : {pred R}) := MkIdeal {
idealr_zmod :> zmodPred S;
_ : proper_ideal S
}.
-Structure prime_idealr (R : ringType) (S : predPredType R) := MkPrimeIdeal {
+Structure prime_idealr (R : ringType) (S : {pred R}) := MkPrimeIdeal {
prime_idealr_zmod :> idealr S;
_ : prime_idealr_closed S
}.
-Definition Idealr (R : ringType) (I : predPredType R) (zmodI : zmodPred I)
+Definition Idealr (R : ringType) (I : {pred R}) (zmodI : zmodPred I)
(kI : keyed_pred zmodI) : proper_ideal I -> idealr I.
Proof. by move=> kI1; split => //. Qed.
Section IdealTheory.
-Variables (R : ringType) (I : predPredType R)
+Variables (R : ringType) (I : {pred R})
(idealrI : idealr I) (kI : keyed_pred idealrI).
Lemma idealr1 : 1 \in kI = false.
@@ -475,7 +474,7 @@ End IdealTheory.
Section PrimeIdealTheory.
-Variables (R : comRingType) (I : predPredType R)
+Variables (R : comRingType) (I : {pred R})
(pidealrI : prime_idealr I) (kI : keyed_pred pidealrI).
Lemma prime_idealrM u v : (u * v \in kI) = (u \in kI) || (v \in kI).
@@ -490,7 +489,7 @@ End IdealDef.
Module Quotient.
Section ZmodQuotient.
-Variables (R : zmodType) (I : predPredType R)
+Variables (R : zmodType) (I : {pred R})
(zmodI : zmodPred I) (kI : keyed_pred zmodI).
Definition equiv (x y : R) := (x - y) \in kI.
@@ -567,7 +566,7 @@ Notation "{quot I }" := (@type_of _ _ _ I (Phant _)).
Section RingQuotient.
-Variables (R : comRingType) (I : predPredType R)
+Variables (R : comRingType) (I : {pred R})
(idealI : idealr I) (kI : keyed_pred idealI).
Local Notation type := {quot kI}.
@@ -618,7 +617,7 @@ End RingQuotient.
Section IDomainQuotient.
-Variables (R : comRingType) (I : predPredType R)
+Variables (R : comRingType) (I : {pred R})
(pidealI : prime_idealr I) (kI : keyed_pred pidealI).
Lemma rquot_IdomainAxiom (x y : {quot kI}): x * y = 0 -> (x == 0) || (y == 0).
diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v
index 7c74468..d35253c 100644
--- a/mathcomp/algebra/ssralg.v
+++ b/mathcomp/algebra/ssralg.v
@@ -851,7 +851,7 @@ Qed.
Section ClosedPredicates.
-Variable S : predPredType V.
+Variable S : {pred V}.
Definition addr_closed := 0 \in S /\ {in S &, forall u v, u + v \in S}.
Definition oppr_closed := {in S, forall u, - u \in S}.
@@ -1418,7 +1418,7 @@ Canonical converse_ringType := RingType R^c converse_ringMixin.
Section ClosedPredicates.
-Variable S : predPredType R.
+Variable S : {pred R}.
Definition mulr_2closed := {in S &, forall u v, u * v \in S}.
Definition mulr_closed := 1 \in S /\ mulr_2closed.
@@ -1626,7 +1626,7 @@ Proof. exact: big_endo (scalerDr a) (scaler0 a) I r P F. Qed.
Section ClosedPredicates.
-Variable S : predPredType V.
+Variable S : {pred V}.
Definition scaler_closed := forall a, {in S, forall v, a *: v \in S}.
Definition linear_closed := forall a, {in S &, forall u v, a *: u + v \in S}.
@@ -1746,7 +1746,7 @@ Canonical regular_lalgType := LalgType R R^o (@mulrA regular_ringType).
Section ClosedPredicates.
-Variable S : predPredType A.
+Variable S : {pred A}.
Definition subalg_closed := [/\ 1 \in S, linear_closed S & mulr_2closed S].
@@ -2985,14 +2985,13 @@ Lemma rev_unitrP (x y : R^c) : y * x = 1 /\ x * y = 1 -> x \is a unit.
Proof. by case=> [yx1 xy1]; apply/unitrP; exists y. Qed.
Definition converse_unitRingMixin :=
- @UnitRing.Mixin _ ((unit : pred_class) : pred R^c) _
- mulrV mulVr rev_unitrP invr_out.
+ @UnitRing.Mixin _ (unit : {pred R^c}) _ mulrV mulVr rev_unitrP invr_out.
Canonical converse_unitRingType := UnitRingType R^c converse_unitRingMixin.
Canonical regular_unitRingType := [unitRingType of R^o].
Section ClosedPredicates.
-Variables S : predPredType R.
+Variables S : {pred R}.
Definition invr_closed := {in S, forall x, x^-1 \in S}.
Definition divr_2closed := {in S &, forall x y, x / y \in S}.
@@ -3266,7 +3265,7 @@ Qed.
Section ClosedPredicates.
-Variables S : predPredType A.
+Variables S : {pred A}.
Definition divalg_closed := [/\ 1 \in S, linear_closed S & divr_2closed S].
@@ -3511,7 +3510,7 @@ End DefaultPred.
Section ZmodulePred.
-Variables (V : zmodType) (S : predPredType V).
+Variables (V : zmodType) (S : {pred V}).
Section Add.
@@ -3580,7 +3579,7 @@ End ZmodulePred.
Section RingPred.
-Variables (R : ringType) (S : predPredType R).
+Variables (R : ringType) (S : {pred R}).
Lemma rpredMsign (oppS : opprPred S) (kS : keyed_pred oppS) n x :
((-1) ^+ n * x \in kS) = (x \in kS).
@@ -3624,7 +3623,7 @@ End RingPred.
Section LmodPred.
-Variables (R : ringType) (V : lmodType R) (S : predPredType V).
+Variables (R : ringType) (V : lmodType R) (S : {pred V}).
Lemma rpredZsign (oppS : opprPred S) (kS : keyed_pred oppS) n u :
((-1) ^+ n *: u \in kS) = (u \in kS).
@@ -3645,7 +3644,7 @@ Variable R : unitRingType.
Section Div.
-Variables (S : predPredType R) (divS : divrPred S) (kS : keyed_pred divS).
+Variables (S : {pred R}) (divS : divrPred S) (kS : keyed_pred divS).
Lemma rpredVr x : x \in kS -> x^-1 \in kS.
Proof. by rewrite !keyed_predE; case: divS x. Qed.
@@ -4792,7 +4791,7 @@ Proof. by move=> p; rewrite inE -scaler_nat scaler_eq0 oner_eq0 orbF. Qed.
Section Predicates.
-Context (S : pred_class) (divS : @divrPred F S) (kS : keyed_pred divS).
+Context (S : {pred F}) (divS : @divrPred F S) (kS : keyed_pred divS).
Lemma fpredMl x y : x \in kS -> x != 0 -> (x * y \in kS) = (y \in kS).
Proof. by rewrite -!unitfE; apply: rpredMl. Qed.
@@ -5150,7 +5149,7 @@ Module SubType.
Section Zmodule.
-Variables (V : zmodType) (S : predPredType V).
+Variables (V : zmodType) (S : {pred V}).
Variables (subS : zmodPred S) (kS : keyed_pred subS).
Variable U : subType (mem kS).
@@ -5175,7 +5174,7 @@ End Zmodule.
Section Ring.
-Variables (R : ringType) (S : predPredType R).
+Variables (R : ringType) (S : {pred R}).
Variables (ringS : subringPred S) (kS : keyed_pred ringS).
Definition cast_zmodType (V : zmodType) T (VeqT : V = T :> Type) :=
@@ -5219,7 +5218,7 @@ End Ring.
Section Lmodule.
-Variables (R : ringType) (V : lmodType R) (S : predPredType V).
+Variables (R : ringType) (V : lmodType R) (S : {pred V}).
Variables (linS : submodPred S) (kS : keyed_pred linS).
Variables (W : subType (mem kS)) (Z : zmodType) (ZeqW : Z = W :> Type).
@@ -5265,7 +5264,7 @@ Definition cast_ringType (Q : ringType) T (QeqT : Q = T :> Type) :=
let cast rQ := let: erefl in _ = T := QeqT return Ring.class_of T in rQ in
Ring.Pack (cast (Ring.class Q)).
-Variables (R : unitRingType) (S : predPredType R).
+Variables (R : unitRingType) (S : {pred R}).
Variables (ringS : divringPred S) (kS : keyed_pred ringS).
Variables (T : subType (mem kS)) (Q : ringType) (QeqT : Q = T :> Type).
@@ -5279,7 +5278,7 @@ Hypothesis val1 : val (1 : T') = 1.
Hypothesis valM : {morph (val : T' -> R) : x y / x * y}.
Fact mulVr :
- {in (unitT : predPredType T'), left_inverse (1 : T') invT (@mul T')}.
+ {in (unitT : {pred T'}), left_inverse (1 : T') invT (@mul T')}.
Proof. by move=> u Uu; apply: val_inj; rewrite val1 valM SubK mulVr. Qed.
Fact mulrV : {in unitT, right_inverse (1 : T') invT (@mul T')}.
@@ -6249,7 +6248,7 @@ Canonical pair_unitAlgType (R : comUnitRingType) (A1 A2 : unitAlgType R) :=
(* Testing subtype hierarchy
Section Test0.
-Variables (T : choiceType) (S : predPredType T).
+Variables (T : choiceType) (S : {pred T}).
Inductive B := mkB x & x \in S.
Definition vB u := let: mkB x _ := u in x.
@@ -6264,7 +6263,7 @@ End Test0.
Section Test1.
-Variables (R : unitRingType) (S : pred R).
+Variables (R : unitRingType) (S : {pred R}).
Variables (ringS : divringPred S) (kS : keyed_pred ringS).
Definition B_zmodMixin := [zmodMixin of B kS by <:].
@@ -6278,7 +6277,7 @@ End Test1.
Section Test2.
-Variables (R : comUnitRingType) (A : unitAlgType R) (S : pred A).
+Variables (R : comUnitRingType) (A : unitAlgType R) (S : {pred A}).
Variables (algS : divalgPred S) (kS : keyed_pred algS).
Definition B_lmodMixin := [lmodMixin of B kS by <:].
@@ -6293,7 +6292,7 @@ End Test2.
Section Test3.
-Variables (F : fieldType) (S : pred F).
+Variables (F : fieldType) (S : {pred F}).
Variables (ringS : divringPred S) (kS : keyed_pred ringS).
Definition B_comRingMixin := [comRingMixin of B kS by <:].
diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v
index 6b2a40a..97afdfb 100644
--- a/mathcomp/algebra/ssrnum.v
+++ b/mathcomp/algebra/ssrnum.v
@@ -1314,8 +1314,7 @@ Proof. by move=> m n; apply: leq_total. Qed.
Section AcrossTypes.
-Variable D D' : pred R.
-Variable (f : R -> R').
+Variables (D D' : {pred R}) (f : R -> R').
Lemma ltrW_homo : {homo f : x y / x < y} -> {homo f : x y / x <= y}.
Proof. exact: homoW. Qed.
@@ -1382,8 +1381,7 @@ End AcrossTypes.
Section NatToR.
-Variable D D' : pred nat.
-Variable (f : nat -> R).
+Variables (D D' : {pred nat}) (f : nat -> R).
Lemma ltnrW_homo : {homo f : m n / (m < n)%N >-> m < n} ->
{homo f : m n / (m <= n)%N >-> m <= n}.
@@ -1471,8 +1469,7 @@ End NatToR.
Section RToNat.
-Variable D D' : pred R.
-Variable (f : R -> nat).
+Variables (D D' : {pred R}) (f : R -> nat).
Lemma ltrnW_homo : {homo f : m n / m < n >-> (m < n)%N} ->
{homo f : m n / m <= n >-> (m <= n)%N}.
@@ -3070,7 +3067,7 @@ Proof. by move=> le_xy; rewrite ltr_neqAle !le_xy andbT. Qed.
Lemma lerif_nat m n C : (m%:R <= n%:R ?= iff C :> R) = (m <= n ?= iff C)%N.
Proof. by rewrite /lerif !ler_nat eqr_nat. Qed.
-Lemma mono_in_lerif (A : pred R) (f : R -> R) C :
+Lemma mono_in_lerif (A : {pred R}) (f : R -> R) C :
{in A &, {mono f : x y / x <= y}} ->
{in A &, forall x y, (f x <= f y ?= iff C) = (x <= y ?= iff C)}.
Proof.
@@ -3082,7 +3079,7 @@ Lemma mono_lerif (f : R -> R) C :
forall x y, (f x <= f y ?= iff C) = (x <= y ?= iff C).
Proof. by move=> mf x y; rewrite /lerif mf (inj_eq (incr_inj _)). Qed.
-Lemma nmono_in_lerif (A : pred R) (f : R -> R) C :
+Lemma nmono_in_lerif (A : {pred R}) (f : R -> R) C :
{in A &, {mono f : x y /~ x <= y}} ->
{in A &, forall x y, (f x <= f y ?= iff C) = (y <= x ?= iff C)}.
Proof.
@@ -3183,7 +3180,7 @@ move=> Rx Ry; rewrite sqrrD addrAC (mulrnDr _ 2) -lerif_subLR addrK.
exact: real_lerif_mean_square_scaled.
Qed.
-Lemma lerif_AGM_scaled (I : finType) (A : pred I) (E : I -> R) (n := #|A|) :
+Lemma lerif_AGM_scaled (I : finType) (A : {pred I}) (E : I -> R) (n := #|A|) :
{in A, forall i, 0 <= E i *+ n} ->
\prod_(i in A) (E i *+ n) <= (\sum_(i in A) E i) ^+ n
?= iff [forall i in A, forall j in A, E i == E j].
@@ -3515,7 +3512,7 @@ rewrite mulr_natr (natrX F 2 2) -exprMn divfK ?pnatr_eq0 //.
exact: real_lerif_AGM2_scaled.
Qed.
-Lemma lerif_AGM (I : finType) (A : pred I) (E : I -> F) :
+Lemma lerif_AGM (I : finType) (A : {pred I}) (E : I -> F) :
let n := #|A| in let mu := (\sum_(i in A) E i) / n%:R in
{in A, forall i, 0 <= E i} ->
\prod_(i in A) E i <= mu ^+ n
@@ -4855,7 +4852,7 @@ Qed.
(* The proper form of the Arithmetic - Geometric Mean inequality. *)
-Lemma lerif_rootC_AGM (I : finType) (A : pred I) (n := #|A|) E :
+Lemma lerif_rootC_AGM (I : finType) (A : {pred I}) (n := #|A|) E :
{in A, forall i, 0 <= E i} ->
n.-root (\prod_(i in A) E i) <= (\sum_(i in A) E i) / n%:R
?= iff [forall i in A, forall j in A, E i == E j].
diff --git a/mathcomp/algebra/vector.v b/mathcomp/algebra/vector.v
index 48d7d3e..e73ca33 100644
--- a/mathcomp/algebra/vector.v
+++ b/mathcomp/algebra/vector.v
@@ -267,10 +267,10 @@ Definition subsetv U V := (vs2mx U <= vs2mx V)%MS.
Definition vline u := mx2vs (v2r u).
(* Vspace membership is defined as line inclusion. *)
-Definition pred_of_vspace phV (U : Vector.space phV) : pred_class :=
+Definition pred_of_vspace phV (U : Vector.space phV) : {pred vT} :=
fun v => (vs2mx (vline v) <= vs2mx U)%MS.
Canonical vspace_predType :=
- @mkPredType _ (unkeyed {vspace vT}) (@pred_of_vspace _).
+ @PredType _ (unkeyed {vspace vT}) (@pred_of_vspace _).
Definition fullv : {vspace vT} := mx2vs 1%:M.
Definition addv U V := mx2vs (vs2mx U + vs2mx V).
@@ -294,7 +294,7 @@ Definition basis_of U X := (span X == U) && free X.
End VspaceDefs.
-Coercion pred_of_vspace : Vector.space >-> pred_class.
+Coercion pred_of_vspace : Vector.space >-> pred_sort.
Notation "\dim U" := (dimv U) : nat_scope.
Notation "U <= V" := (subsetv U V) : vspace_scope.
Notation "U <= V <= W" := (subsetv U V && subsetv V W) : vspace_scope.
diff --git a/mathcomp/character/character.v b/mathcomp/character/character.v
index 862e1ba..c2a7ef4 100644
--- a/mathcomp/character/character.v
+++ b/mathcomp/character/character.v
@@ -572,10 +572,10 @@ Lemma irr_of_socleK : cancel irr_of_socle W.
Proof. by move=> Wi; rewrite /W subrK cast_ordKV enum_rankK. Qed.
Hint Resolve socle_of_IirrK irr_of_socleK : core.
-Lemma irr_of_socle_bij (A : pred (Iirr G)) : {on A, bijective irr_of_socle}.
+Lemma irr_of_socle_bij (A : {pred (Iirr G)}) : {on A, bijective irr_of_socle}.
Proof. by apply: onW_bij; exists W. Qed.
-Lemma socle_of_Iirr_bij (A : pred sG) : {on A, bijective W}.
+Lemma socle_of_Iirr_bij (A : {pred sG}) : {on A, bijective W}.
Proof. by apply: onW_bij; exists irr_of_socle. Qed.
End IrrClassDef.
diff --git a/mathcomp/character/classfun.v b/mathcomp/character/classfun.v
index 2cf17aa..468aa66 100644
--- a/mathcomp/character/classfun.v
+++ b/mathcomp/character/classfun.v
@@ -1066,7 +1066,7 @@ have [-> | nzV] := eqVneq V 0; first by rewrite cfdot0r !mul0r subrr.
by rewrite divfK ?cfnorm_eq0 ?subrr.
Qed.
-Lemma map_orthogonal M (nu : 'CF(G) -> 'CF(M)) S R (A : pred 'CF(G)) :
+Lemma map_orthogonal M (nu : 'CF(G) -> 'CF(M)) S R (A : {pred 'CF(G)}) :
{in A &, isometry nu} -> {subset S <= A} -> {subset R <= A} ->
orthogonal (map nu S) (map nu R) = orthogonal S R.
Proof.
@@ -1290,7 +1290,7 @@ Section BuildIsometries.
Variable (gT : finGroupType) (L G : {group gT}).
Implicit Types (phi psi xi : 'CF(L)) (R S : seq 'CF(L)).
-Implicit Types (U : pred 'CF(L)) (W : pred 'CF(G)).
+Implicit Types (U : {pred 'CF(L)}) (W : {pred 'CF(G)}).
Lemma sub_iso_to U1 U2 W1 W2 tau :
{subset U2 <= U1} -> {subset W1 <= W2} ->
diff --git a/mathcomp/character/vcharacter.v b/mathcomp/character/vcharacter.v
index 8d7d7e9..4212fbe 100644
--- a/mathcomp/character/vcharacter.v
+++ b/mathcomp/character/vcharacter.v
@@ -47,7 +47,7 @@ Section Basics.
Variables (gT : finGroupType) (B : {set gT}) (S : seq 'CF(B)) (A : {set gT}).
-Definition Zchar : pred_class :=
+Definition Zchar : {pred 'CF(B)} :=
[pred phi in 'CF(B, A) | dec_Cint_span (in_tuple S) phi].
Fact Zchar_key : pred_key Zchar. Proof. by []. Qed.
Canonical Zchar_keyed := KeyedPred Zchar_key.
@@ -701,8 +701,8 @@ Qed.
End MoreVchar.
-Definition dirr (gT : finGroupType) (B : {set gT}) : pred_class :=
- [pred f : 'CF(B) | (f \in irr B) || (- f \in irr B)].
+Definition dirr (gT : finGroupType) (B : {set gT}) : {pred 'CF(B)} :=
+ [pred f | (f \in irr B) || (- f \in irr B)].
Arguments dirr {gT}.
Section Norm1vchar.
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.
diff --git a/mathcomp/fingroup/fingroup.v b/mathcomp/fingroup/fingroup.v
index 65af825..9399035 100644
--- a/mathcomp/fingroup/fingroup.v
+++ b/mathcomp/fingroup/fingroup.v
@@ -1357,17 +1357,6 @@ Lemma valG : val G = G. Proof. by []. Qed.
Lemma group1 : 1 \in G. Proof. by case/group_setP: (valP G). Qed.
Hint Resolve group1 : core.
-(* Loads of silly variants to placate the incompleteness of trivial. *)
-(* An alternative would be to upgrade done, pending better support *)
-(* in the ssreflect ML code. *)
-Notation gTr := (FinGroup.sort gT).
-Notation Gcl := (pred_of_set G : pred gTr).
-Lemma group1_class1 : (1 : gTr) \in G. Proof. by []. Qed.
-Lemma group1_class2 : 1 \in Gcl. Proof. by []. Qed.
-Lemma group1_class12 : (1 : gTr) \in Gcl. Proof. by []. Qed.
-Lemma group1_eqType : (1 : gT : eqType) \in G. Proof. by []. Qed.
-Lemma group1_finType : (1 : gT : finType) \in G. Proof. by []. Qed.
-
Lemma group1_contra x : x \notin G -> x != 1.
Proof. by apply: contraNneq => ->. Qed.
@@ -1385,14 +1374,6 @@ Lemma repr_group : repr G = 1. Proof. by rewrite /repr group1. Qed.
Lemma cardG_gt0 : 0 < #|G|.
Proof. by rewrite lt0n; apply/existsP; exists (1 : gT). Qed.
-(* Workaround for the fact that the simple matching used by Trivial does not *)
-(* always allow conversion. In particular cardG_gt0 always fails to apply to *)
-(* subgoals that have been simplified (by /=) because type inference in the *)
-(* notation #|G| introduces redexes of the form *)
-(* Finite.sort (arg_finGroupType (FinGroup.base gT)) *)
-(* which get collapsed to Fingroup.arg_sort (FinGroup.base gT). *)
-Definition cardG_gt0_reduced : 0 < card (@mem gT (predPredType gT) G)
- := cardG_gt0.
Lemma indexg_gt0 A : 0 < #|G : A|.
Proof.
@@ -1839,9 +1820,9 @@ Qed.
End GroupProp.
-Hint Resolve group1 group1_class1 group1_class12 group1_class12 : core.
-Hint Resolve group1_eqType group1_finType : core.
-Hint Resolve cardG_gt0 cardG_gt0_reduced indexg_gt0 : core.
+Hint Extern 0 (is_true (1%g \in _)) => apply: group1 : core.
+Hint Extern 0 (is_true (0 < #|_|)) => apply: cardG_gt0 : core.
+Hint Extern 0 (is_true (0 < #|_ : _|)) => apply: indexg_gt0 : core.
Notation "G :^ x" := (conjG_group G x) : Group_scope.
@@ -3005,7 +2986,8 @@ Notation "''C_' G [ x ]" := (setI_group G 'C[x]) : Group_scope.
Notation "''C_' ( G ) [ x ]" := (setI_group G 'C[x])
(only parsing) : Group_scope.
-Hint Resolve normG normal_refl : core.
+Hint Extern 0 (is_true (_ \subset _)) => apply: normG : core.
+Hint Extern 0 (is_true (_ <| _)) => apply: normal_refl : core.
Section MinMaxGroup.
diff --git a/mathcomp/solvable/gfunctor.v b/mathcomp/solvable/gfunctor.v
index 31ffded..3417d84 100644
--- a/mathcomp/solvable/gfunctor.v
+++ b/mathcomp/solvable/gfunctor.v
@@ -266,7 +266,7 @@ Variable F : GFunctor.iso_map.
Lemma gFsub gT (G : {group gT}) : F gT G \subset G.
Proof. by case: F gT G. Qed.
-Lemma gFsub_trans gT (G : {group gT}) (A : pred_class) :
+Lemma gFsub_trans gT (G : {group gT}) (A : {pred gT}) :
G \subset A -> F gT G \subset A.
Proof. exact/subset_trans/gFsub. Qed.
@@ -297,7 +297,7 @@ Proof. exact/char_trans/gFchar. Qed.
Lemma gFnormal_trans gT (G H : {group gT}) : H <| G -> F gT H <| G.
Proof. exact/char_normal_trans/gFchar. Qed.
-Lemma gFnorm_trans gT (A : pred_class) (G : {group gT}) :
+Lemma gFnorm_trans gT (A : {pred gT}) (G : {group gT}) :
A \subset 'N(G) -> A \subset 'N(F gT G).
Proof. by move/subset_trans/(_ (gFnorms G)). Qed.
diff --git a/mathcomp/ssreflect/finfun.v b/mathcomp/ssreflect/finfun.v
index 127bd48..075ebfa 100644
--- a/mathcomp/ssreflect/finfun.v
+++ b/mathcomp/ssreflect/finfun.v
@@ -348,7 +348,7 @@ Section EqTheory.
Variables (aT : finType) (rT : eqType).
Notation fT := {ffun aT -> rT}.
-Implicit Types (y : rT) (D : pred aT) (R : pred rT) (f : fT).
+Implicit Types (y : rT) (D : {pred aT}) (R : {pred rT}) (f : fT).
Lemma supportP y D g :
reflect (forall x, x \notin D -> g x = y) (y.-support g \subset D).
@@ -440,7 +440,7 @@ Section FinFunTheory.
Variables aT rT : finType.
Notation fT := {ffun aT -> rT}.
-Implicit Types (D : pred aT) (R : pred rT) (F : aT -> pred rT).
+Implicit Types (D : {pred aT}) (R : {pred rT}) (F : aT -> pred rT).
Lemma card_pfamily y0 D F :
#|pfamily y0 D F| = foldr muln 1 [seq #|F x| | x in D].
diff --git a/mathcomp/ssreflect/fingraph.v b/mathcomp/ssreflect/fingraph.v
index 42346e2..70536dc 100644
--- a/mathcomp/ssreflect/fingraph.v
+++ b/mathcomp/ssreflect/fingraph.v
@@ -238,7 +238,7 @@ Notation fclosure f a := (closure (coerced_frel f) a).
Section EqConnect.
Variable T : finType.
-Implicit Types (e : rel T) (a : pred T).
+Implicit Types (e : rel T) (a : {pred T}).
Lemma connect_sub e e' :
subrel e (connect e') -> subrel (connect e) (connect e').
@@ -289,7 +289,7 @@ Section Closure.
Variables (T : finType) (e : rel T).
Hypothesis sym_e : connect_sym e.
-Implicit Type a : pred T.
+Implicit Type a : {pred T}.
Lemma same_connect_rev : connect e =2 connect (fun x y => e y x).
Proof.
@@ -465,7 +465,7 @@ End Loop.
Section orbit_in.
-Variable S : pred_sort (predPredType T).
+Variable S : {pred T}.
Hypothesis f_in : {in S, forall x, f x \in S}.
Hypothesis injf : {in S &, injective f}.
@@ -579,7 +579,7 @@ Proof. exact: eq_n_comp same_fconnect_finv. Qed.
Definition order_set n : pred T := [pred x | order x == n].
-Lemma fcard_order_set n (a : pred T) :
+Lemma fcard_order_set n (a : {pred T}) :
a \subset order_set n -> fclosed f a -> fcard f a * n = #|a|.
Proof.
move=> a_n cl_a; rewrite /n_comp_mem; set b := [predI froots f & a].
@@ -598,7 +598,8 @@ rewrite -(cardID (fconnect f x)); congr (_ + _); apply: eq_card => y.
by congr (~~ _ && _); rewrite /= /in_mem /= symf -(root_connect symf) r_x.
Qed.
-Lemma fclosed1 (a : pred T) : fclosed f a -> forall x, (x \in a) = (f x \in a).
+Lemma fclosed1 (a : {pred T}) :
+ fclosed f a -> forall x, (x \in a) = (f x \in a).
Proof. by move=> cl_a x; apply: cl_a (eqxx _). Qed.
Lemma same_fconnect1 x : fconnect f x =1 fconnect f (f x).
@@ -630,7 +631,7 @@ Proof. by rewrite /roots -fconnect_id connect_root. Qed.
Lemma froot_id (x : T) : froot id x = x.
Proof. by apply/eqP; apply: froots_id. Qed.
-Lemma fcard_id (a : pred T) : fcard id a = #|a|.
+Lemma fcard_id (a : {pred T}) : fcard id a = #|a|.
Proof. by apply: eq_card => x; rewrite inE froots_id. Qed.
End FconnectId.
@@ -694,7 +695,7 @@ Record rel_adjunction_mem m_a := RelAdjunction {
in_mem (h x') m_a -> connect e' x' y' = connect e (h x') (h y')
}.
-Variable a : pred T.
+Variable a : {pred T}.
Hypothesis cl_a : closed e a.
Local Notation rel_adjunction := (rel_adjunction_mem (mem a)).
diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v
index 98abdf2..204843a 100644
--- a/mathcomp/ssreflect/finset.v
+++ b/mathcomp/ssreflect/finset.v
@@ -203,8 +203,7 @@ Coercion pred_of_set: set_type >-> fin_pred_sort.
(* Declare pred_of_set as a canonical instance of topred, but use the *)
(* coercion to resolve mem A to @mem (predPredType T) (pred_of_set A). *)
-Canonical set_predType T :=
- Eval hnf in @mkPredType _ (unkeyed (set_type T)) (@pred_of_set T).
+Canonical set_predType T := @PredType _ (unkeyed (set_type T)) (@pred_of_set T).
Section BasicSetTheory.
@@ -1085,7 +1084,7 @@ Notation "[ 'set' E | x : T 'in' A , y : U 'in' B & P ]" :=
(at level 0, E, x, y at level 99, only parsing) : set_scope.
(* Comprehensions over a type. *)
-Local Notation predOfType T := (sort_of_simpl_pred (@pred_of_argType T)).
+Local Notation predOfType T := (pred_of_simpl (@pred_of_argType T)).
Notation "[ 'set' E | x : T ]" := [set E | x : T in predOfType T]
(at level 0, E, x at level 99,
format "[ '[hv' 'set' E '/ ' | x : T ] ']'") : set_scope.
@@ -1205,7 +1204,7 @@ apply: (iffP imageP) => [[[x1 x2] Dx12] | [x1 x2 Dx1 Dx2]] -> {y}.
by exists (x1, x2); rewrite //= !inE Dx1.
Qed.
-Lemma mem_imset (D : pred aT) x : x \in D -> f x \in f @: D.
+Lemma mem_imset (D : {pred aT}) x : x \in D -> f x \in f @: D.
Proof. by move=> Dx; apply/imsetP; exists x. Qed.
Lemma imset0 : f @: set0 = set0.
@@ -1223,12 +1222,12 @@ apply/setP => y.
by apply/imsetP/set1P=> [[x' /set1P-> //]| ->]; exists x; rewrite ?set11.
Qed.
-Lemma mem_imset2 (D : pred aT) (D2 : aT -> pred aT2) x x2 :
+Lemma mem_imset2 (D : {pred aT}) (D2 : aT -> {pred aT2}) x x2 :
x \in D -> x2 \in D2 x ->
f2 x x2 \in imset2 f2 (mem D) (fun x1 => mem (D2 x1)).
Proof. by move=> Dx Dx2; apply/imset2P; exists x x2. Qed.
-Lemma sub_imset_pre (A : pred aT) (B : pred rT) :
+Lemma sub_imset_pre (A : {pred aT}) (B : {pred rT}) :
(f @: A \subset B) = (A \subset f @^-1: B).
Proof.
apply/subsetP/subsetP=> [sfAB x Ax | sAf'B fx].
@@ -1236,7 +1235,7 @@ apply/subsetP/subsetP=> [sfAB x Ax | sAf'B fx].
by case/imsetP=> x Ax ->; move/sAf'B: Ax; rewrite inE.
Qed.
-Lemma preimsetS (A B : pred rT) :
+Lemma preimsetS (A B : {pred rT}) :
A \subset B -> (f @^-1: A) \subset (f @^-1: B).
Proof. by move=> sAB; apply/subsetP=> y; rewrite !inE; apply: subsetP. Qed.
@@ -1261,7 +1260,7 @@ Proof. by apply/setP=> y; rewrite !inE. Qed.
Lemma preimsetC (A : {set rT}) : f @^-1: (~: A) = ~: f @^-1: A.
Proof. by apply/setP=> y; rewrite !inE. Qed.
-Lemma imsetS (A B : pred aT) : A \subset B -> f @: A \subset f @: B.
+Lemma imsetS (A B : {pred aT}) : A \subset B -> f @: A \subset f @: B.
Proof.
move=> sAB; apply/subsetP=> _ /imsetP[x Ax ->].
by apply/imsetP; exists x; rewrite ?(subsetP sAB).
@@ -1303,27 +1302,27 @@ apply/subsetP=> _ /setIP[/imsetP[x Ax ->] /imsetP[z Bz /injf eqxz]].
by rewrite mem_imset // inE Ax eqxz.
Qed.
-Lemma imset2Sl (A B : pred aT) (C : pred aT2) :
+Lemma imset2Sl (A B : {pred aT}) (C : {pred aT2}) :
A \subset B -> f2 @2: (A, C) \subset f2 @2: (B, C).
Proof.
move=> sAB; apply/subsetP=> _ /imset2P[x y Ax Cy ->].
by apply/imset2P; exists x y; rewrite ?(subsetP sAB).
Qed.
-Lemma imset2Sr (A B : pred aT2) (C : pred aT) :
+Lemma imset2Sr (A B : {pred aT2}) (C : {pred aT}) :
A \subset B -> f2 @2: (C, A) \subset f2 @2: (C, B).
Proof.
move=> sAB; apply/subsetP=> _ /imset2P[x y Ax Cy ->].
by apply/imset2P; exists x y; rewrite ?(subsetP sAB).
Qed.
-Lemma imset2S (A B : pred aT) (A2 B2 : pred aT2) :
+Lemma imset2S (A B : {pred aT}) (A2 B2 : {pred aT2}) :
A \subset B -> A2 \subset B2 -> f2 @2: (A, A2) \subset f2 @2: (B, B2).
Proof. by move=> /(imset2Sl B2) sBA /(imset2Sr A)/subset_trans->. Qed.
End ImsetProp.
-Implicit Types (f g : aT -> rT) (D : {set aT}) (R : pred rT).
+Implicit Types (f g : aT -> rT) (D : {set aT}) (R : {pred rT}).
Lemma eq_preimset f g R : f =1 g -> f @^-1: R = g @^-1: R.
Proof. by move=> eqfg; apply/setP => y; rewrite !inE eqfg. Qed.
@@ -1340,7 +1339,7 @@ move=> eqfg; apply/setP => y.
by apply/imsetP/imsetP=> [] [x Dx ->]; exists x; rewrite ?eqfg.
Qed.
-Lemma eq_in_imset2 (f g : aT -> aT2 -> rT) (D : pred aT) (D2 : pred aT2) :
+Lemma eq_in_imset2 (f g : aT -> aT2 -> rT) (D : {pred aT}) (D2 : {pred aT2}) :
{in D & D2, f =2 g} -> f @2: (D, D2) = g @2: (D, D2).
Proof.
move=> eqfg; apply/setP => y.
@@ -1407,7 +1406,7 @@ Lemma big_setU1 a A F : a \notin A ->
\big[aop/idx]_(i in a |: A) F i = aop (F a) (\big[aop/idx]_(i in A) F i).
Proof. by move=> notAa; rewrite (@big_setD1 a) ?setU11 //= setU1K. Qed.
-Lemma big_imset h (A : pred I) G : {in A &, injective h} ->
+Lemma big_imset h (A : {pred I}) G : {in A &, injective h} ->
\big[aop/idx]_(j in h @: A) G j = \big[aop/idx]_(i in A) G (h i).
Proof.
move=> injh; pose hA := mem (image h A).
@@ -1424,12 +1423,12 @@ symmetry; rewrite (negbTE nhAhi); apply/idP=> Ai.
by case/imageP: nhAhi; exists i.
Qed.
-Lemma big_imset_cond h (A : pred I) (P : pred J) G : {in A &, injective h} ->
+Lemma big_imset_cond h (A : {pred I}) (P : pred J) G : {in A &, injective h} ->
\big[aop/idx]_(j in h @: A | P j) G j =
\big[aop/idx]_(i in A | P (h i)) G (h i).
Proof. by move=> h_inj; rewrite 2!big_mkcondr big_imset. Qed.
-Lemma partition_big_imset h (A : pred I) F :
+Lemma partition_big_imset h (A : {pred I}) F :
\big[aop/idx]_(i in A) F i =
\big[aop/idx]_(j in h @: A) \big[aop/idx]_(i in A | h i == j) F i.
Proof. by apply: partition_big => i Ai; apply/imsetP; exists i. Qed.
@@ -1447,14 +1446,14 @@ Section Fun2Set1.
Variables aT1 aT2 rT : finType.
Variables (f : aT1 -> aT2 -> rT).
-Lemma imset2_set1l x1 (D2 : pred aT2) : f @2: ([set x1], D2) = f x1 @: D2.
+Lemma imset2_set1l x1 (D2 : {pred aT2}) : f @2: ([set x1], D2) = f x1 @: D2.
Proof.
apply/setP=> y; apply/imset2P/imsetP=> [[x x2 /set1P->]| [x2 Dx2 ->]].
by exists x2.
by exists x1 x2; rewrite ?set11.
Qed.
-Lemma imset2_set1r x2 (D1 : pred aT1) : f @2: (D1, [set x2]) = f^~ x2 @: D1.
+Lemma imset2_set1r x2 (D1 : {pred aT1}) : f @2: (D1, [set x2]) = f^~ x2 @: D1.
Proof.
apply/setP=> y; apply/imset2P/imsetP=> [[x1 x Dx1 /set1P->]| [x1 Dx1 ->]].
by exists x1.
@@ -1467,7 +1466,7 @@ Section CardFunImage.
Variables aT aT2 rT : finType.
Variables (f : aT -> rT) (g : rT -> aT) (f2 : aT -> aT2 -> rT).
-Variables (D : pred aT) (D2 : pred aT).
+Variables (D : {pred aT}) (D2 : {pred aT}).
Lemma imset_card : #|f @: D| = #|image f D|.
Proof. by rewrite [@imset]unlock cardsE. Qed.
@@ -1498,7 +1497,7 @@ End CardFunImage.
Arguments imset_injP {aT rT f D}.
-Lemma on_card_preimset (aT rT : finType) (f : aT -> rT) (R : pred rT) :
+Lemma on_card_preimset (aT rT : finType) (f : aT -> rT) (R : {pred rT}) :
{on R, bijective f} -> #|f @^-1: R| = #|R|.
Proof.
case=> g fK gK; rewrite -(can2_in_imset_pre gK) // card_in_imset //.
@@ -1539,7 +1538,7 @@ Section FunImageComp.
Variables T T' U : finType.
-Lemma imset_comp (f : T' -> U) (g : T -> T') (H : pred T) :
+Lemma imset_comp (f : T' -> U) (g : T -> T') (H : {pred T}) :
(f \o g) @: H = f @: (g @: H).
Proof.
apply/setP/subset_eqP/andP.
@@ -1603,7 +1602,7 @@ Notation "\bigcap_ ( i 'in' A ) F" :=
Section BigSetOps.
Variables T I : finType.
-Implicit Types (U : pred T) (P : pred I) (A B : {set I}) (F : I -> {set T}).
+Implicit Types (U : {pred T}) (P : pred I) (A B : {set I}) (F : I -> {set T}).
(* It is very hard to use this lemma, because the unification fails to *)
(* defer the F j pattern (even though it's a Miller pattern!). *)
@@ -1714,7 +1713,7 @@ Variables (aT1 aT2 rT : finType) (f : aT1 -> aT2 -> rT).
Section Curry.
Variables (A1 : {set aT1}) (A2 : {set aT2}).
-Variables (D1 : pred aT1) (D2 : pred aT2).
+Variables (D1 : {pred aT1}) (D2 : {pred aT2}).
Lemma curry_imset2X : f @2: (A1, A2) = prod_curry f @: (setX A1 A2).
Proof.
diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v
index 04c1732..e58ae61 100644
--- a/mathcomp/ssreflect/fintype.v
+++ b/mathcomp/ssreflect/fintype.v
@@ -461,9 +461,7 @@ Section OpsTheory.
Variable T : finType.
-Implicit Types A B C P Q : pred T.
-Implicit Types x y : T.
-Implicit Type s : seq T.
+Implicit Types (A B C : {pred T}) (P Q : pred T) (x y : T) (s : seq T).
Lemma enumP : Finite.axiom (Finite.enum T).
Proof. by rewrite unlock; case T => ? [? []]. Qed.
@@ -478,7 +476,7 @@ Proof. exact: filter_predT. Qed.
Lemma mem_enum A : enum A =i A.
Proof. by move=> x; rewrite mem_filter andbC -has_pred1 has_count enumP. Qed.
-Lemma enum_uniq : uniq (enum P).
+Lemma enum_uniq A : uniq (enum A).
Proof.
by apply/filter_uniq/count_mem_uniq => x; rewrite enumP -enumT mem_enum.
Qed.
@@ -504,8 +502,8 @@ Qed.
End EnumPick.
-Lemma eq_enum P Q : P =i Q -> enum P = enum Q.
-Proof. by move=> eqPQ; apply: eq_filter. Qed.
+Lemma eq_enum A B : A =i B -> enum A = enum B.
+Proof. by move=> eqAB; apply: eq_filter. Qed.
Lemma eq_pick P Q : P =1 Q -> pick P = pick Q.
Proof. by move=> eqPQ; rewrite /pick (eq_enum eqPQ). Qed.
@@ -640,17 +638,17 @@ Hint Resolve subxx_hint : core.
Lemma subxx (pT : predType T) (pA : pT) : pA \subset pA.
Proof. by []. Qed.
-Lemma eq_subset A1 A2 : A1 =i A2 -> subset (mem A1) =1 subset (mem A2).
+Lemma eq_subset A B : A =i B -> subset (mem A) =1 subset (mem B).
Proof.
-move=> eqA12 [B]; rewrite !unlock; congr (_ == 0).
-by apply: eq_card => x; rewrite inE /= eqA12.
+move=> eqAB [C]; rewrite !unlock; congr (_ == 0).
+by apply: eq_card => x; rewrite inE /= eqAB.
Qed.
-Lemma eq_subset_r B1 B2 : B1 =i B2 ->
- (@subset T)^~ (mem B1) =1 (@subset T)^~ (mem B2).
+Lemma eq_subset_r A B :
+ A =i B -> (@subset T)^~ (mem A) =1 (@subset T)^~ (mem B).
Proof.
-move=> eqB12 [A]; rewrite !unlock; congr (_ == 0).
-by apply: eq_card => x; rewrite !inE /= eqB12.
+move=> eqAB [C]; rewrite !unlock; congr (_ == 0).
+by apply: eq_card => x; rewrite !inE /= eqAB.
Qed.
Lemma eq_subxx A B : A =i B -> A \subset B.
@@ -746,8 +744,8 @@ move=> eAB [C]; congr (_ && _); first exact: (eq_subset eAB).
by rewrite (eq_subset_r eAB).
Qed.
-Lemma eq_proper_r A B : A =i B ->
- (@proper T)^~ (mem A) =1 (@proper T)^~ (mem B).
+Lemma eq_proper_r A B :
+ A =i B -> (@proper T)^~ (mem A) =1 (@proper T)^~ (mem B).
Proof.
move=> eAB [C]; congr (_ && _); first exact: (eq_subset_r eAB).
by rewrite (eq_subset eAB).
@@ -756,15 +754,15 @@ Qed.
Lemma disjoint_sym A B : [disjoint A & B] = [disjoint B & A].
Proof. by congr (_ == 0); apply: eq_card => x; apply: andbC. Qed.
-Lemma eq_disjoint A1 A2 : A1 =i A2 -> disjoint (mem A1) =1 disjoint (mem A2).
+Lemma eq_disjoint A B : A =i B -> disjoint (mem A) =1 disjoint (mem B).
Proof.
-by move=> eqA12 [B]; congr (_ == 0); apply: eq_card => x; rewrite !inE eqA12.
+by move=> eqAB [C]; congr (_ == 0); apply: eq_card => x; rewrite !inE eqAB.
Qed.
-Lemma eq_disjoint_r B1 B2 : B1 =i B2 ->
- (@disjoint T)^~ (mem B1) =1 (@disjoint T)^~ (mem B2).
+Lemma eq_disjoint_r A B : A =i B ->
+ (@disjoint T)^~ (mem A) =1 (@disjoint T)^~ (mem B).
Proof.
-by move=> eqB12 [A]; congr (_ == 0); apply: eq_card => x; rewrite !inE eqB12.
+by move=> eqAB [C]; congr (_ == 0); apply: eq_card => x; rewrite !inE eqAB.
Qed.
Lemma subset_disjoint A B : (A \subset B) = [disjoint A & [predC B]].
@@ -787,9 +785,9 @@ Proof. by move/eq_disjoint->; apply: disjoint0. Qed.
Lemma disjoint1 x A : [disjoint pred1 x & A] = (x \notin A).
Proof.
-apply/negbRL/(sameP (pred0Pn _)).
+apply/negbRL/(sameP (pred0Pn _))=> /=.
apply: introP => [Ax | notAx [_ /andP[/eqP->]]]; last exact: negP.
-by exists x; rewrite !inE eqxx.
+by exists x; rewrite inE eqxx.
Qed.
Lemma eq_disjoint1 x A B :
@@ -863,7 +861,7 @@ Notation "'forall_ view" := (forallPP (fun _ => view))
Section Quantifiers.
Variables (T : finType) (rT : T -> eqType).
-Implicit Type (D P : pred T) (f : forall x, rT x).
+Implicit Types (D P : pred T) (f : forall x, rT x).
Lemma forallP P : reflect (forall x, P x) [forall x, P x].
Proof. exact: 'forall_idP. Qed.
@@ -1059,7 +1057,7 @@ Notation "[ 'arg' 'max_' ( i > i0 ) F ]" := [arg max_(i > i0 | true) F]
Section Injectiveb.
Variables (aT : finType) (rT : eqType) (f : aT -> rT).
-Implicit Type D : pred aT.
+Implicit Type D : {pred aT}.
Definition dinjectiveb D := uniq (map f (enum D)).
@@ -1113,7 +1111,7 @@ Notation "[ 'seq' F | x 'in' A ]" := (image (fun x => F) A)
Notation "[ 'seq' F | x : T 'in' A ]" := (image (fun x : T => F) A)
(at level 0, F at level 99, x ident, only parsing) : seq_scope.
Notation "[ 'seq' F | x : T ]" :=
- [seq F | x : T in sort_of_simpl_pred (@pred_of_argType T)]
+ [seq F | x : T in pred_of_simpl (@pred_of_argType T)]
(at level 0, F at level 99, x ident,
format "'[hv' [ 'seq' F '/ ' | x : T ] ']'") : seq_scope.
Notation "[ 'seq' F , x ]" := [seq F | x : _ ]
@@ -1124,7 +1122,7 @@ Definition codom T T' f := @image_mem T T' f (mem T).
Section Image.
Variable T : finType.
-Implicit Type A : pred T.
+Implicit Type A : {pred T}.
Section SizeImage.
@@ -1236,7 +1234,8 @@ Prenex Implicits codom iinv.
Arguments imageP {T T' f A y}.
Arguments codomP {T T' f y}.
-Lemma flatten_imageP (aT : finType) (rT : eqType) A (P : pred aT) (y : rT) :
+Lemma flatten_imageP (aT : finType) (rT : eqType)
+ (A : aT -> seq rT) (P : {pred aT}) (y : rT) :
reflect (exists2 x, x \in P & y \in A x) (y \in flatten [seq A x | x in P]).
Proof.
by apply: (iffP flatten_mapP) => [][x Px]; exists x; rewrite ?mem_enum in Px *.
@@ -1246,7 +1245,7 @@ Arguments flatten_imageP {aT rT A P y}.
Section CardFunImage.
Variables (T T' : finType) (f : T -> T').
-Implicit Type A : pred T.
+Implicit Type A : {pred T}.
Lemma leq_image_card A : #|image f A| <= #|A|.
Proof. by rewrite (cardE A) -(size_map f) card_size. Qed.
@@ -1271,7 +1270,7 @@ Proof. by apply: card_in_image; apply: in2W. Qed.
Lemma card_codom : #|codom f| = #|T|.
Proof. exact: card_image. Qed.
-Lemma card_preim (B : pred T') : #|[preim f of B]| = #|[predI codom f & B]|.
+Lemma card_preim (B : {pred T'}) : #|[preim f of B]| = #|[predI codom f & B]|.
Proof.
rewrite -card_image /=; apply: eq_card => y.
by rewrite [y \in _]image_pre !inE andbC.
@@ -1330,7 +1329,7 @@ Section EqImage.
Variables (T : finType) (T' : Type).
-Lemma eq_image (A B : pred T) (f g : T -> T') :
+Lemma eq_image (A B : {pred T}) (f g : T -> T') :
A =i B -> f =1 g -> image f A = image g B.
Proof.
by move=> eqAB eqfg; rewrite /image_mem (eq_enum eqAB) (eq_map eqfg).
@@ -1461,7 +1460,7 @@ Variable sfT : subFinType P.
Lemma card_sub : #|sfT| = #|[pred x | P x]|.
Proof. by rewrite -(eq_card (codom_val sfT)) (card_image val_inj). Qed.
-Lemma eq_card_sub (A : pred sfT) : A =i predT -> #|A| = #|[pred x | P x]|.
+Lemma eq_card_sub (A : {pred sfT}) : A =i predT -> #|A| = #|[pred x | P x]|.
Proof. exact: eq_card_trans card_sub. Qed.
End FinTypeForSub.
@@ -1695,7 +1694,7 @@ Proof. exact: inv_inj rev_ordK. Qed.
Section EnumRank.
Variable T : finType.
-Implicit Type A : pred T.
+Implicit Type A : {pred T}.
Lemma enum_rank_subproof x0 A : x0 \in A -> 0 < #|A|.
Proof. by move=> Ax0; rewrite (cardD1 x0) Ax0. Qed.
@@ -2026,7 +2025,7 @@ Variable T1 T2 : finType.
Definition prod_enum := [seq (x1, x2) | x1 <- enum T1, x2 <- enum T2].
-Lemma predX_prod_enum (A1 : pred T1) (A2 : pred T2) :
+Lemma predX_prod_enum (A1 : {pred T1}) (A2 : {pred T2}) :
count [predX A1 & A2] prod_enum = #|A1| * #|A2|.
Proof.
rewrite !cardE !size_filter -!enumT /prod_enum.
@@ -2042,13 +2041,14 @@ Qed.
Definition prod_finMixin := Eval hnf in FinMixin prod_enumP.
Canonical prod_finType := Eval hnf in FinType (T1 * T2) prod_finMixin.
-Lemma cardX (A1 : pred T1) (A2 : pred T2) : #|[predX A1 & A2]| = #|A1| * #|A2|.
+Lemma cardX (A1 : {pred T1}) (A2 : {pred T2}) :
+ #|[predX A1 & A2]| = #|A1| * #|A2|.
Proof. by rewrite -predX_prod_enum unlock size_filter unlock. Qed.
Lemma card_prod : #|{: T1 * T2}| = #|T1| * #|T2|.
Proof. by rewrite -cardX; apply: eq_card; case. Qed.
-Lemma eq_card_prod (A : pred (T1 * T2)) : A =i predT -> #|A| = #|T1| * #|T2|.
+Lemma eq_card_prod (A : {pred (T1 * T2)}) : A =i predT -> #|A| = #|T1| * #|T2|.
Proof. exact: eq_card_trans card_prod. Qed.
End ProdFinType.
diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v
index 9a01ed1..bfecfa9 100644
--- a/mathcomp/ssreflect/prime.v
+++ b/mathcomp/ssreflect/prime.v
@@ -7,7 +7,9 @@ From mathcomp Require Import fintype div bigop.
(* This file contains the definitions of: *)
(* prime p <=> p is a prime. *)
(* primes m == the sorted list of prime divisors of m > 1, else [::]. *)
-(* pfactor == the type of prime factors, syntax (p ^ e)%pfactor. *)
+(* pfactor p e == the value p ^ e of a prime factor (p, e). *)
+(* NumFactor f == print version of a prime factor, converting the prime *)
+(* component to a Num (which can print large values). *)
(* prime_decomp m == the list of prime factors of m > 1, sorted by primes. *)
(* logn p m == the e such that (p ^ e) \in prime_decomp n, else 0. *)
(* trunc_log p m == the largest e such that p ^ e <= m, or 0 if p or m is 0. *)
@@ -26,16 +28,15 @@ From mathcomp Require Import fintype div bigop.
(* that (p \in \pi(n)) = (p \in primes n). *)
(* \pi(A) == the set of primes of #|A|, with A a collective predicate *)
(* over a finite Type. *)
-(* -> The notation \pi(A) is implemented with a collapsible Coercion, so *)
-(* the type of A must coerce to finpred_class (e.g., by coercing to *)
-(* {set T}), not merely implement the predType interface (as seq T *)
-(* does). *)
-(* -> The expression #|A| will only appear in \pi(A) after simplification *)
-(* collapses the coercion stack, so it is advisable to do so early on. *)
+(* -> The notation \pi(A) is implemented with a collapsible Coercion. The *)
+(* type of A must coerce to finpred_sort (e.g., by coercing to {set T}) *)
+(* and not merely implement the predType interface (as seq T does). *)
+(* -> The expression #|A| will only appear in \pi(A) after simplification *)
+(* collapses the coercion, so it is advisable to do so early on. *)
(* pi.-nat n <=> n > 0 and all prime divisors of n are in pi. *)
(* n`_pi == the pi-part of n -- the largest pi.-nat divisor of n. *)
(* := \prod_(0 <= p < n.+1 | p \in pi) p ^ logn p n. *)
-(* -> The nat >-> nat_pred coercion lets us write p.-nat n and n`_p. *)
+(* -> The nat >-> nat_pred coercion lets us write p.-nat n and n`_p. *)
(* In addition to the lemmas relevant to these definitions, this file also *)
(* contains the dvdn_sum lemma, so that bigop.v doesn't depend on div.v. *)
(******************************************************************************)
@@ -56,7 +57,9 @@ Unset Printing Implicit Defensive.
(* which can then be used casually in proofs with moderately-sized numeric *)
(* values (indeed, the code here performs well for up to 6-digit numbers). *)
-(* We start with faster mod-2 functions. *)
+Module Import PrimeDecompAux.
+
+(* We start with faster mod-2 and 2-valuation functions. *)
Fixpoint edivn2 q r := if r is r'.+2 then edivn2 q.+1 r' else (q, r).
@@ -95,21 +98,35 @@ Variant ifnz_spec T n (x y : T) : T -> Type :=
Lemma ifnzP T n (x y : T) : ifnz_spec n x y (ifnz n x y).
Proof. by case: n => [|n]; [right | left]. Qed.
-(* For pretty-printing. *)
-Definition NumFactor (f : nat * nat) := ([Num of f.1], f.2).
+(* The list of divisors and the Euler function are computed directly from *)
+(* the decomposition, using a merge_sort variant sort of the divisor list. *)
-Definition pfactor p e := p ^ e.
+Definition add_divisors f divs :=
+ let: (p, e) := f in
+ let add1 divs' := merge leq (map (NatTrec.mul p) divs') divs in
+ iter e add1 divs.
+
+Import NatTrec.
+
+Definition add_totient_factor f m := let: (p, e) := f in p.-1 * p ^ e.-1 * m.
Definition cons_pfactor (p e : nat) pd := ifnz e ((p, e) :: pd) pd.
-Local Notation "p ^? e :: pd" := (cons_pfactor p e pd)
+Notation "p ^? e :: pd" := (cons_pfactor p e pd)
(at level 30, e at level 30, pd at level 60) : nat_scope.
+End PrimeDecompAux.
+
+(* For pretty-printing. *)
+Definition NumFactor (f : nat * nat) := ([Num of f.1], f.2).
+
+Definition pfactor p e := p ^ e.
+
Section prime_decomp.
Import NatTrec.
-Fixpoint prime_decomp_rec m k a b c e :=
+Local Fixpoint prime_decomp_rec m k a b c e :=
let p := k.*2.+1 in
if a is a'.+1 then
if b - (ifnz e 1 k - c) is b'.+1 then
@@ -128,16 +145,6 @@ Definition prime_decomp n :=
let: (b, c) := edivn (2 - bc) 2 in
2 ^? e2 :: [rec m2.*2.+1, 1, a, b, c, 0].
-(* The list of divisors and the Euler function are computed directly from *)
-(* the decomposition, using a merge_sort variant sort the divisor list. *)
-
-Definition add_divisors f divs :=
- let: (p, e) := f in
- let add1 divs' := merge leq (map (NatTrec.mul p) divs') divs in
- iter e add1 divs.
-
-Definition add_totient_factor f m := let: (p, e) := f in p.-1 * p ^ e.-1 * m.
-
End prime_decomp.
Definition primes n := unzip1 (prime_decomp n).
@@ -146,19 +153,16 @@ Definition prime p := if prime_decomp p is [:: (_ , 1)] then true else false.
Definition nat_pred := simpl_pred nat.
-Definition pi_unwrapped_arg := nat.
-Definition pi_wrapped_arg := wrapped nat.
-Coercion unwrap_pi_arg (wa : pi_wrapped_arg) : pi_unwrapped_arg := unwrap wa.
-Coercion pi_arg_of_nat (n : nat) := Wrap n : pi_wrapped_arg.
-Coercion pi_arg_of_fin_pred T pT (A : @fin_pred_sort T pT) : pi_wrapped_arg :=
- Wrap #|A|.
-
-Definition pi_of (n : pi_unwrapped_arg) : nat_pred := [pred p in primes n].
+Definition pi_arg := nat.
+Coercion pi_arg_of_nat (n : nat) : pi_arg := n.
+Coercion pi_arg_of_fin_pred T pT (A : @fin_pred_sort T pT) : pi_arg := #|A|.
+Arguments pi_arg_of_nat n /.
+Arguments pi_arg_of_fin_pred {T pT} A /.
+Definition pi_of (n : pi_arg) : nat_pred := [pred p in primes n].
Notation "\pi ( n )" := (pi_of n)
(at level 2, format "\pi ( n )") : nat_scope.
-Notation "\p 'i' ( A )" := \pi(#|A|)
- (at level 2, format "\p 'i' ( A )") : nat_scope.
+Notation "\pi ( A )" := \pi(#|A|) (only printing) : nat_scope.
Definition pdiv n := head 1 (primes n).
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v
index 1c8e150..5576355 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/mathcomp/ssreflect/seq.v
@@ -928,14 +928,13 @@ Proof. by rewrite -size_eq0 size_filter has_count lt0n. Qed.
Fixpoint mem_seq (s : seq T) :=
if s is y :: s' then xpredU1 y (mem_seq s') else xpred0.
-Definition eqseq_class := seq T.
-Identity Coercion seq_of_eqseq : eqseq_class >-> seq.
+Definition seq_eqclass := seq T.
+Identity Coercion seq_of_eqclass : seq_eqclass >-> seq.
+Coercion pred_of_seq (s : seq_eqclass) : {pred T} := mem_seq s.
-Coercion pred_of_eq_seq (s : eqseq_class) : pred_class := [eta mem_seq s].
-
-Canonical seq_predType := @mkPredType T (seq T) pred_of_eq_seq.
+Canonical seq_predType := PredType (pred_of_seq : seq T -> pred T).
(* The line below makes mem_seq a canonical instance of topred. *)
-Canonical mem_seq_predType := mkPredType mem_seq.
+Canonical mem_seq_predType := PredType mem_seq.
Lemma in_cons y s x : (x \in y :: s) = (x == y) || (x \in s).
Proof. by []. Qed.
@@ -949,14 +948,13 @@ Proof. by rewrite in_cons orbF. Qed.
(* to be repeated after the Section discharge. *)
Let inE := (mem_seq1, in_cons, inE).
-Lemma mem_seq2 x y1 y2 : (x \in [:: y1; y2]) = xpred2 y1 y2 x.
+Lemma mem_seq2 x y z : (x \in [:: y; z]) = xpred2 y z x.
Proof. by rewrite !inE. Qed.
-Lemma mem_seq3 x y1 y2 y3 : (x \in [:: y1; y2; y3]) = xpred3 y1 y2 y3 x.
+Lemma mem_seq3 x y z t : (x \in [:: y; z; t]) = xpred3 y z t x.
Proof. by rewrite !inE. Qed.
-Lemma mem_seq4 x y1 y2 y3 y4 :
- (x \in [:: y1; y2; y3; y4]) = xpred4 y1 y2 y3 y4 x.
+Lemma mem_seq4 x y z t u : (x \in [:: y; z; t; u]) = xpred4 y z t u x.
Proof. by rewrite !inE. Qed.
Lemma mem_cat x s1 s2 : (x \in s1 ++ s2) = (x \in s1) || (x \in s2).
@@ -1285,6 +1283,7 @@ Definition inE := (mem_seq1, in_cons, inE).
Prenex Implicits mem_seq1 constant uniq undup index.
Arguments eqseq {T} !_ !_.
+Arguments pred_of_seq {T} s x /.
Arguments eqseqP {T x y}.
Arguments hasP {T a s}.
Arguments hasPn {T a s}.
@@ -2253,7 +2252,7 @@ Qed.
Lemma perm_pmap s t : perm_eq s t -> perm_eq (pmap f s) (pmap f t).
Proof.
-move=> eq_st; apply/(perm_map_inj (@Some_inj _)); rewrite !pmapS_filter.
+move=> eq_st; apply/(perm_map_inj Some_inj); rewrite !pmapS_filter.
exact/perm_map/perm_filter.
Qed.
diff --git a/mathcomp/ssreflect/ssrbool.v b/mathcomp/ssreflect/ssrbool.v
index c96ca6a..7eb7fd9 100644
--- a/mathcomp/ssreflect/ssrbool.v
+++ b/mathcomp/ssreflect/ssrbool.v
@@ -1 +1,40 @@
-From Coq Require Export ssrbool. \ No newline at end of file
+From mathcomp Require Import ssreflect ssrfun.
+From Coq Require Export ssrbool.
+
+Notation "{ 'pred' T }" := (pred_sort (predPredType T)) (at level 0,
+ format "{ 'pred' T }") : type_scope.
+
+Lemma simpl_pred_sortE T (p : pred T) : (SimplPred p : {pred T}) =1 p.
+Proof. by []. Qed.
+Definition inE := (inE, simpl_pred_sortE).
+
+Definition PredType : forall T pT, (pT -> pred T) -> predType T.
+exact PredType || exact mkPredType.
+Defined.
+Arguments PredType [T pT] toP.
+
+Definition simpl_rel T := T -> simpl_pred T.
+Definition SimplRel {T} (r : rel T) : simpl_rel T := fun x => SimplPred (r x).
+Coercion rel_of_simpl_rel T (sr : simpl_rel T) : rel T := sr.
+Arguments rel_of_simpl_rel {T} sr x / y : rename.
+
+Notation "[ 'rel' x y | E ]" := (SimplRel (fun x y => E%B)) (at level 0,
+ x ident, y ident, format "'[hv' [ 'rel' x y | '/ ' E ] ']'") : fun_scope.
+Notation "[ 'rel' x y : T | E ]" := (SimplRel (fun x y : T => E%B)) (at level 0,
+ x ident, y ident, only parsing) : fun_scope.
+Notation "[ 'rel' x y 'in' A & B | E ]" :=
+ [rel x y | (x \in A) && (y \in B) && E] (at level 0, x ident, y ident,
+ format "'[hv' [ 'rel' x y 'in' A & B | '/ ' E ] ']'") : fun_scope.
+Notation "[ 'rel' x y 'in' A & B ]" := [rel x y | (x \in A) && (y \in B)]
+ (at level 0, x ident, y ident,
+ format "'[hv' [ 'rel' x y 'in' A & B ] ']'") : fun_scope.
+Notation "[ 'rel' x y 'in' A | E ]" := [rel x y in A & A | E]
+ (at level 0, x ident, y ident,
+ format "'[hv' [ 'rel' x y 'in' A | '/ ' E ] ']'") : fun_scope.
+Notation "[ 'rel' x y 'in' A ]" := [rel x y in A & A] (at level 0,
+ x ident, y ident, format "'[hv' [ 'rel' x y 'in' A ] ']'") : fun_scope.
+
+Notation xrelpre := (fun f (r : rel _) x y => r (f x) (f y)).
+Definition relpre {T rT} (f : T -> rT) (r : rel rT) :=
+ [rel x y | r (f x) (f y)].
+
diff --git a/mathcomp/ssreflect/ssreflect.v b/mathcomp/ssreflect/ssreflect.v
index a7b5ef8..fe06c0d 100644
--- a/mathcomp/ssreflect/ssreflect.v
+++ b/mathcomp/ssreflect/ssreflect.v
@@ -5,3 +5,31 @@ Global Set SsrOldRewriteGoalsOrder.
Global Set Asymmetric Patterns.
Global Set Bullet Behavior "None".
+Module NonPropType.
+
+Structure call_of (condition : unit) (result : bool) := Call {callee : Type}.
+Definition maybeProp (T : Type) := tt.
+Definition call T := Call (maybeProp T) false T.
+
+Structure test_of (result : bool) := Test {condition :> unit}.
+Definition test_Prop (P : Prop) := Test true (maybeProp P).
+Definition test_negative := Test false tt.
+
+Structure type :=
+ Check {result : bool; test : test_of result; frame : call_of test result}.
+Definition check result test frame := @Check result test frame.
+
+Module Exports.
+Canonical call.
+Canonical test_Prop.
+Canonical test_negative.
+Canonical check.
+Notation nonPropType := type.
+Coercion callee : call_of >-> Sortclass.
+Coercion frame : type >-> call_of.
+Notation notProp T := (@check false test_negative (call T)).
+End Exports.
+
+End NonPropType.
+Export NonPropType.Exports.
+
diff --git a/mathcomp/ssreflect/ssrfun.v b/mathcomp/ssreflect/ssrfun.v
index 2dd7103..ed18941 100644
--- a/mathcomp/ssreflect/ssrfun.v
+++ b/mathcomp/ssreflect/ssrfun.v
@@ -1,2 +1,5 @@
+From mathcomp Require Import ssreflect.
From Coq Require Export ssrfun.
From mathcomp Require Export ssrnotations.
+
+Definition Some_inj {T : nonPropType} := @Some_inj T.
diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v
index 9222124..86f8fb2 100644
--- a/mathcomp/ssreflect/ssrnat.v
+++ b/mathcomp/ssreflect/ssrnat.v
@@ -1382,7 +1382,7 @@ Qed.
Section Monotonicity.
Variable T : Type.
-Lemma homo_ltn_in (D : pred nat) (f : nat -> T) (r : T -> T -> Prop) :
+Lemma homo_ltn_in (D : {pred nat}) (f : nat -> T) (r : T -> T -> Prop) :
(forall y x z, r x y -> r y z -> r x z) ->
{in D &, forall i j k, i < k < j -> k \in D} ->
{in D, forall i, i.+1 \in D -> r (f i) (f i.+1)} ->
@@ -1400,7 +1400,7 @@ Lemma homo_ltn (f : nat -> T) (r : T -> T -> Prop) :
(forall i, r (f i) (f i.+1)) -> {homo f : i j / i < j >-> r i j}.
Proof. by move=> /(@homo_ltn_in predT f) fr fS i j; apply: fr. Qed.
-Lemma homo_leq_in (D : pred nat) (f : nat -> T) (r : T -> T -> Prop) :
+Lemma homo_leq_in (D : {pred nat}) (f : nat -> T) (r : T -> T -> Prop) :
(forall x, r x x) -> (forall y x z, r x y -> r y z -> r x z) ->
{in D &, forall i j k, i < k < j -> k \in D} ->
{in D, forall i, i.+1 \in D -> r (f i) (f i.+1)} ->
@@ -1464,7 +1464,7 @@ Proof. exact: total_homo_mono. Qed.
Lemma leq_nmono : {homo f : m n /~ m < n} -> {mono f : m n /~ m <= n}.
Proof. exact: total_homo_mono. Qed.
-Variable (D D' : pred nat).
+Variables (D D' : {pred nat}).
Lemma ltnW_homo_in : {in D & D', {homo f : m n / m < n}} ->
{in D & D', {homo f : m n / m <= n}}.
diff --git a/mathcomp/ssreflect/tuple.v b/mathcomp/ssreflect/tuple.v
index 77e9dc0..dd73664 100644
--- a/mathcomp/ssreflect/tuple.v
+++ b/mathcomp/ssreflect/tuple.v
@@ -275,8 +275,7 @@ Variables (n : nat) (T : eqType).
Definition tuple_eqMixin := Eval hnf in [eqMixin of n.-tuple T by <:].
Canonical tuple_eqType := Eval hnf in EqType (n.-tuple T) tuple_eqMixin.
-Canonical tuple_predType :=
- Eval hnf in mkPredType (fun t : n.-tuple T => mem_seq t).
+Canonical tuple_predType := PredType (pred_of_seq : n.-tuple T -> pred T).
Lemma memtE (t : n.-tuple T) : mem t = mem (tval t).
Proof. by []. Qed.
@@ -371,7 +370,7 @@ Canonical tuple_subFinType := Eval hnf in [subFinType of n.-tuple T].
Lemma card_tuple : #|{:n.-tuple T}| = #|T| ^ n.
Proof. by rewrite [#|_|]cardT enumT unlock FinTuple.size_enum. Qed.
-Lemma enum_tupleP (A : pred T) : size (enum A) == #|A|.
+Lemma enum_tupleP (A : {pred T}) : size (enum A) == #|A|.
Proof. by rewrite -cardE. Qed.
Canonical enum_tuple A := Tuple (enum_tupleP A).
@@ -389,7 +388,7 @@ Qed.
Section ImageTuple.
-Variables (T' : Type) (f : T -> T') (A : pred T).
+Variables (T' : Type) (f : T -> T') (A : {pred T}).
Canonical image_tuple : #|A|.-tuple T' := [tuple of image f A].
Canonical codom_tuple : #|T|.-tuple T' := [tuple of codom f].
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:15:12 +0000