From 10171942883948c8144ec076ef48eb73f8e49cdd Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Thu, 12 Jul 2018 20:19:55 +0900 Subject: Replace all the CoInductives with Variants --- mathcomp/algebra/fraction.v | 2 +- mathcomp/algebra/intdiv.v | 2 +- mathcomp/algebra/interval.v | 4 ++-- mathcomp/algebra/matrix.v | 2 +- mathcomp/algebra/mxalgebra.v | 4 ++-- mathcomp/algebra/polydiv.v | 12 ++++++------ mathcomp/algebra/rat.v | 6 +++--- mathcomp/algebra/ssrint.v | 10 +++++----- mathcomp/algebra/ssrnum.v | 22 +++++++++++----------- mathcomp/character/mxrepresentation.v | 8 ++++---- mathcomp/field/algC.v | 2 +- mathcomp/fingroup/fingroup.v | 2 +- mathcomp/fingroup/gproduct.v | 2 +- mathcomp/fingroup/morphism.v | 2 +- mathcomp/fingroup/perm.v | 2 +- mathcomp/fingroup/quotient.v | 2 +- mathcomp/solvable/frobenius.v | 2 +- mathcomp/ssreflect/bigop.v | 2 +- mathcomp/ssreflect/div.v | 4 ++-- mathcomp/ssreflect/eqtype.v | 6 +++--- mathcomp/ssreflect/finset.v | 2 +- mathcomp/ssreflect/fintype.v | 10 +++++----- mathcomp/ssreflect/generic_quotient.v | 6 +++--- mathcomp/ssreflect/path.v | 12 ++++++------ mathcomp/ssreflect/plugin/v8.6/ssrbool.v | 12 ++++++------ mathcomp/ssreflect/plugin/v8.6/ssreflect.v | 6 +++--- mathcomp/ssreflect/plugin/v8.6/ssrfun.v | 4 ++-- mathcomp/ssreflect/prime.v | 4 ++-- mathcomp/ssreflect/seq.v | 4 ++-- mathcomp/ssreflect/ssrnat.v | 10 +++++----- mathcomp/ssreflect/tuple.v | 2 +- 31 files changed, 85 insertions(+), 85 deletions(-) (limited to 'mathcomp') diff --git a/mathcomp/algebra/fraction.v b/mathcomp/algebra/fraction.v index 98eb9f1..28dd82b 100644 --- a/mathcomp/algebra/fraction.v +++ b/mathcomp/algebra/fraction.v @@ -53,7 +53,7 @@ Proof. by move=> ny0; rewrite /Ratio /insubd insubT. Qed. Definition numden_Ratio := (numer_Ratio, denom_Ratio). -CoInductive Ratio_spec (n d : R) : {ratio R} -> R -> R -> Type := +Variant Ratio_spec (n d : R) : {ratio R} -> R -> R -> Type := | RatioNull of d = 0 : Ratio_spec n d ratio0 n 0 | RatioNonNull (d_neq0 : d != 0) : Ratio_spec n d (@mkRatio (n, d) d_neq0) n d. diff --git a/mathcomp/algebra/intdiv.v b/mathcomp/algebra/intdiv.v index e043561..4c5ad4d 100644 --- a/mathcomp/algebra/intdiv.v +++ b/mathcomp/algebra/intdiv.v @@ -560,7 +560,7 @@ Proof. by rewrite coprimezE abszN. Qed. Lemma coprimezN m n : coprimez m (- n) = coprimez m n. Proof. by rewrite coprimezE abszN. Qed. -CoInductive egcdz_spec m n : int * int -> Type := +Variant egcdz_spec m n : int * int -> Type := EgcdzSpec u v of u * m + v * n = gcdz m n & coprimez u v : egcdz_spec m n (u, v). diff --git a/mathcomp/algebra/interval.v b/mathcomp/algebra/interval.v index b699da1..80f1b5d 100644 --- a/mathcomp/algebra/interval.v +++ b/mathcomp/algebra/interval.v @@ -48,10 +48,10 @@ Local Notation mid x y := ((x + y) / 2%:R). Section IntervalPo. -CoInductive itv_bound (T : Type) : Type := BOpen_if of bool & T | BInfty. +Variant itv_bound (T : Type) : Type := BOpen_if of bool & T | BInfty. Notation BOpen := (BOpen_if true). Notation BClose := (BOpen_if false). -CoInductive interval (T : Type) := Interval of itv_bound T & itv_bound T. +Variant interval (T : Type) := Interval of itv_bound T & itv_bound T. Variable (R : numDomainType). diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index ec9fcc5..fca25a9 100644 --- a/mathcomp/algebra/matrix.v +++ b/mathcomp/algebra/matrix.v @@ -870,7 +870,7 @@ Proof. by rewrite card_prod !card_ord. Qed. Definition mxvec_index (i : 'I_m) (j : 'I_n) := cast_ord mxvec_cast (enum_rank (i, j)). -CoInductive is_mxvec_index : 'I_(m * n) -> Type := +Variant is_mxvec_index : 'I_(m * n) -> Type := IsMxvecIndex i j : is_mxvec_index (mxvec_index i j). Lemma mxvec_indexP k : is_mxvec_index k. diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v index d77bfb1..ed8e6c0 100644 --- a/mathcomp/algebra/mxalgebra.v +++ b/mathcomp/algebra/mxalgebra.v @@ -1874,7 +1874,7 @@ Section SubDaddsmx. Variables m m1 m2 n : nat. Variables (A : 'M[F]_(m, n)) (B1 : 'M[F]_(m1, n)) (B2 : 'M[F]_(m2, n)). -CoInductive sub_daddsmx_spec : Prop := +Variant sub_daddsmx_spec : Prop := SubDaddsmxSpec A1 A2 of (A1 <= B1)%MS & (A2 <= B2)%MS & A = A1 + A2 & forall C1 C2, (C1 <= B1)%MS -> (C2 <= B2)%MS -> A = C1 + C2 -> C1 = A1 /\ C2 = A2. @@ -1896,7 +1896,7 @@ Section SubDsumsmx. Variables (P : pred I) (m n : nat) (A : 'M[F]_(m, n)) (B : I -> 'M[F]_n). -CoInductive sub_dsumsmx_spec : Prop := +Variant sub_dsumsmx_spec : Prop := SubDsumsmxSpec A_ of forall i, P i -> (A_ i <= B i)%MS & A = \sum_(i | P i) A_ i & forall C, (forall i, P i -> C i <= B i)%MS -> diff --git a/mathcomp/algebra/polydiv.v b/mathcomp/algebra/polydiv.v index a3b7ad6..34b6e7b 100644 --- a/mathcomp/algebra/polydiv.v +++ b/mathcomp/algebra/polydiv.v @@ -384,7 +384,7 @@ apply: Irec => //; last by rewrite ltn_rmodp. by rewrite ltnW // ltn_rmodp. Qed. -CoInductive comm_redivp_spec m d : nat * {poly R} * {poly R} -> Type := +Variant comm_redivp_spec m d : nat * {poly R} * {poly R} -> Type := ComEdivnSpec k (q r : {poly R}) of (GRing.comm d (lead_coef d)%:P -> m * (lead_coef d ^+ k)%:P = q * d + r) & (d != 0 -> size r < size d) : comm_redivp_spec m d (k, q, r). @@ -510,7 +510,7 @@ rewrite -/v -!exprD addnC subnK ?leq_maxl //. by rewrite addnC subnK ?subrr ?leq_maxr. Qed. -CoInductive rdvdp_spec p q : {poly R} -> bool -> Type := +Variant rdvdp_spec p q : {poly R} -> bool -> Type := | Rdvdp k q1 & p * ((lead_coef q)^+ k)%:P = q1 * q : rdvdp_spec p q 0 true | RdvdpN & rmodp p q != 0 : rdvdp_spec p q (rmodp p q) false. @@ -727,7 +727,7 @@ Variable R : comRingType. Implicit Types d p q m n r : {poly R}. -CoInductive redivp_spec (m d : {poly R}) : nat * {poly R} * {poly R} -> Type := +Variant redivp_spec (m d : {poly R}) : nat * {poly R} * {poly R} -> Type := EdivnSpec k (q r: {poly R}) of (lead_coef d ^+ k) *: m = q * d + r & (d != 0 -> size r < size d) : redivp_spec m d (k, q, r). @@ -870,7 +870,7 @@ Qed. Hint Resolve lc_expn_scalp_neq0. -CoInductive edivp_spec (m d : {poly R}) : +Variant edivp_spec (m d : {poly R}) : nat * {poly R} * {poly R} -> bool -> Type := |Redivp_spec k (q r: {poly R}) of (lead_coef d ^+ k) *: m = q * d + r & lead_coef d \notin GRing.unit & @@ -2340,7 +2340,7 @@ Fixpoint gdcop_rec q p k := Definition gdcop q p := gdcop_rec q p (size p). -CoInductive gdcop_spec q p : {poly R} -> Type := +Variant gdcop_spec q p : {poly R} -> Type := GdcopSpec r of (dvdp r p) & ((coprimep r q) || (p == 0)) & (forall d, dvdp d p -> coprimep d q -> dvdp d r) : gdcop_spec q p r. @@ -3194,7 +3194,7 @@ Qed. (* Just to have it without importing the weak theory *) Lemma dvdpE p q : p %| q = rdvdp p q. Proof. exact: Idomain.dvdpE. Qed. -CoInductive edivp_spec m d : nat * {poly F} * {poly F} -> Type := +Variant edivp_spec m d : nat * {poly F} * {poly F} -> Type := EdivpSpec n q r of m = q * d + r & (d != 0) ==> (size r < size d) : edivp_spec m d (n, q, r). diff --git a/mathcomp/algebra/rat.v b/mathcomp/algebra/rat.v index cd7d306..27f59f5 100644 --- a/mathcomp/algebra/rat.v +++ b/mathcomp/algebra/rat.v @@ -150,7 +150,7 @@ Qed. Fact fracq0 x : fracq (x, 0) = zeroq. Proof. exact/eqP. Qed. -CoInductive fracq_spec (x : int * int) : int * int -> rat -> Type := +Variant fracq_spec (x : int * int) : int * int -> rat -> Type := | FracqSpecN of x.2 = 0 : fracq_spec x (x.1, 0) zeroq | FracqSpecP k fx of k != 0 : fracq_spec x (k * numq fx, k * denq fx) fx. @@ -418,7 +418,7 @@ Qed. Lemma divq_num_den x : (numq x)%:Q / (denq x)%:Q = x. Proof. by rewrite -{3}[x]valqK [valq _]surjective_pairing /= fracqE. Qed. -CoInductive divq_spec (n d : int) : int -> int -> rat -> Type := +Variant divq_spec (n d : int) : int -> int -> rat -> Type := | DivqSpecN of d = 0 : divq_spec n d n 0 0 | DivqSpecP k x of k != 0 : divq_spec n d (k * numq x) (k * denq x) x. @@ -436,7 +436,7 @@ move=> dx_neq0 dy_neq0; rewrite -(inj_eq (@mulIf _ (dx * dy) _)) ?mulf_neq0 //. by rewrite mulrA divfK // mulrCA divfK // [dx * _ ]mulrC. Qed. -CoInductive rat_spec (* (x : rat) *) : rat -> int -> int -> Type := +Variant rat_spec (* (x : rat) *) : rat -> int -> int -> Type := Rat_spec (n : int) (d : nat) & coprime `|n| d.+1 : rat_spec (* x *) (n%:Q / d.+1%:Q) n d.+1. diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v index cbfd593..f12784b 100644 --- a/mathcomp/algebra/ssrint.v +++ b/mathcomp/algebra/ssrint.v @@ -48,7 +48,7 @@ Delimit Scope int_scope with Z. Local Open Scope int_scope. (* Defining int *) -CoInductive int : Set := Posz of nat | Negz of nat. +Variant int : Set := Posz of nat | Negz of nat. (* This must be deferred to module DistInt to work around the design flaws of *) (* the Coq module system. *) (* Coercion Posz : nat >-> int. *) @@ -126,7 +126,7 @@ Qed. Definition int_rec := int_rect. Definition int_ind := int_rect. -CoInductive int_spec (x : int) : int -> Type := +Variant int_spec (x : int) : int -> Type := | ZintNull of x = 0 : int_spec x 0 | ZintPos n of x = n.+1 : int_spec x n.+1 | ZintNeg n of x = - (n.+1)%:Z : int_spec x (- n.+1). @@ -216,7 +216,7 @@ Qed. Definition int_rec := int_rect. Definition int_ind := int_rect. -CoInductive int_spec (x : int) : int -> Type := +Variant int_spec (x : int) : int -> Type := | ZintNull : int_spec x 0 | ZintPos n : int_spec x n.+1 | ZintNeg n : int_spec x (- (n.+1)%:Z). @@ -1438,7 +1438,7 @@ Lemma sgz_cp0 x : ((sgz x == 0) = (x == 0)). Proof. by rewrite /sgz; case: ltrgtP. Qed. -CoInductive sgz_val x : bool -> bool -> bool -> bool -> bool -> bool +Variant sgz_val x : bool -> bool -> bool -> bool -> bool -> bool -> bool -> bool -> bool -> bool -> bool -> bool -> bool -> bool -> bool -> bool -> bool -> bool -> R -> R -> int -> Set := @@ -1783,4 +1783,4 @@ Lemma rpredXsign R S (divS : @divrPred R S) (kS : keyed_pred divS) n x : (x ^ ((-1) ^+ n) \in kS) = (x \in kS). Proof. by rewrite -signr_odd; case: (odd n); rewrite ?rpredV. Qed. -End rpred. \ No newline at end of file +End rpred. diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index 0d9d135..8d4d3e7 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -1550,15 +1550,15 @@ Proof. exact: rpredD. Qed. (* dichotomy and trichotomy *) -CoInductive ler_xor_gt (x y : R) : R -> R -> bool -> bool -> Set := +Variant ler_xor_gt (x y : R) : R -> R -> bool -> bool -> Set := | LerNotGt of x <= y : ler_xor_gt x y (y - x) (y - x) true false | GtrNotLe of y < x : ler_xor_gt x y (x - y) (x - y) false true. -CoInductive ltr_xor_ge (x y : R) : R -> R -> bool -> bool -> Set := +Variant ltr_xor_ge (x y : R) : R -> R -> bool -> bool -> Set := | LtrNotGe of x < y : ltr_xor_ge x y (y - x) (y - x) false true | GerNotLt of y <= x : ltr_xor_ge x y (x - y) (x - y) true false. -CoInductive comparer x y : R -> R -> +Variant comparer x y : R -> R -> bool -> bool -> bool -> bool -> bool -> bool -> Set := | ComparerLt of x < y : comparer x y (y - x) (y - x) false false true false true false @@ -1603,15 +1603,15 @@ have /eqP ->: x == y by rewrite eqr_le le_yx le_xy. by rewrite subrr eqxx; constructor. Qed. -CoInductive ger0_xor_lt0 (x : R) : R -> bool -> bool -> Set := +Variant ger0_xor_lt0 (x : R) : R -> bool -> bool -> Set := | Ger0NotLt0 of 0 <= x : ger0_xor_lt0 x x false true | Ltr0NotGe0 of x < 0 : ger0_xor_lt0 x (- x) true false. -CoInductive ler0_xor_gt0 (x : R) : R -> bool -> bool -> Set := +Variant ler0_xor_gt0 (x : R) : R -> bool -> bool -> Set := | Ler0NotLe0 of x <= 0 : ler0_xor_gt0 x (- x) false true | Gtr0NotGt0 of 0 < x : ler0_xor_gt0 x x true false. -CoInductive comparer0 x : +Variant comparer0 x : R -> bool -> bool -> bool -> bool -> bool -> bool -> Set := | ComparerGt0 of 0 < x : comparer0 x x false false false true false true | ComparerLt0 of x < 0 : comparer0 x (- x) false false true false true false @@ -3574,7 +3574,7 @@ case: (x =P 0) => [-> | _]; first by rewrite !(eq_sym 0) !signr_eq0 ltrr eqxx. by rewrite !(inj_eq signr_inj) eqb_id eqbF_neg signr_eq0 //. Qed. -CoInductive sgr_val x : R -> bool -> bool -> bool -> bool -> bool -> bool +Variant sgr_val x : R -> bool -> bool -> bool -> bool -> bool -> bool -> bool -> bool -> bool -> bool -> bool -> bool -> R -> Set := | SgrNull of x = 0 : sgr_val x 0 true true true true false false true false false true false false 0 @@ -3760,7 +3760,7 @@ Proof. by move=> x y z; rewrite !minrA [minr x y]minrC. Qed. Lemma minrAC : @right_commutative R R min. Proof. by move=> x y z; rewrite -!minrA [minr y z]minrC. Qed. -CoInductive minr_spec x y : bool -> bool -> R -> Type := +Variant minr_spec x y : bool -> bool -> R -> Type := | Minr_r of x <= y : minr_spec x y true false x | Minr_l of y < x : minr_spec x y false true y. @@ -3788,7 +3788,7 @@ Proof. by move=> x y z; rewrite !maxrA [maxr x y]maxrC. Qed. Lemma maxrAC : @right_commutative R R max. Proof. by move=> x y z; rewrite -!maxrA [maxr y z]maxrC. Qed. -CoInductive maxr_spec x y : bool -> bool -> R -> Type := +Variant maxr_spec x y : bool -> bool -> R -> Type := | Maxr_r of y <= x : maxr_spec x y true false x | Maxr_l of x < y : maxr_spec x y false true y. @@ -4041,7 +4041,7 @@ Qed. Lemma ltr0_sqrtr a : a < 0 -> sqrt a = 0. Proof. by move=> /ltrW; apply: ler0_sqrtr. Qed. -CoInductive sqrtr_spec a : R -> bool -> bool -> R -> Type := +Variant sqrtr_spec a : R -> bool -> bool -> R -> Type := | IsNoSqrtr of a < 0 : sqrtr_spec a a false true 0 | IsSqrtr b of 0 <= b : sqrtr_spec a (b ^+ 2) true false b. @@ -4154,7 +4154,7 @@ Let Re2 z := z + z^*. Definition nnegIm z := (0 <= imaginaryC * (z^* - z)). Definition argCle y z := nnegIm z ==> nnegIm y && (Re2 z <= Re2 y). -CoInductive rootC_spec n (x : C) : Type := +Variant rootC_spec n (x : C) : Type := RootCspec (y : C) of if (n > 0)%N then y ^+ n = x else y = 0 & forall z, (n > 0)%N -> z ^+ n = x -> argCle y z. diff --git a/mathcomp/character/mxrepresentation.v b/mathcomp/character/mxrepresentation.v index 4558b3d..c8d7ab1 100644 --- a/mathcomp/character/mxrepresentation.v +++ b/mathcomp/character/mxrepresentation.v @@ -1513,7 +1513,7 @@ Qed. (* Module isomorphism is an intentional property in general, but it can be *) (* decided when one of the two modules is known to be simple. *) -CoInductive mx_iso (U V : 'M_n) : Prop := +Variant mx_iso (U V : 'M_n) : Prop := MxIso f of f \in unitmx & (U <= dom_hom_mx f)%MS & (U *m f :=: V)%MS. Lemma eqmx_iso U V : (U :=: V)%MS -> mx_iso U V. @@ -1692,7 +1692,7 @@ Qed. Implicit Type I : finType. -CoInductive mxsemisimple (V : 'M_n) := +Variant mxsemisimple (V : 'M_n) := MxSemisimple I U (W := (\sum_(i : I) U i)%MS) of forall i, mxsimple (U i) & (W :=: V)%MS & mxdirect W. @@ -1812,7 +1812,7 @@ Qed. (* Completely reducible modules, and Maeschke's Theorem. *) -CoInductive mxsplits (V U : 'M_n) := +Variant mxsplits (V U : 'M_n) := MxSplits (W : 'M_n) of mxmodule W & (U + W :=: V)%MS & mxdirect (U + W). Definition mx_completely_reducible V := @@ -2969,7 +2969,7 @@ Section Similarity. Variables (gT : finGroupType) (G : {group gT}). Local Notation reprG := (mx_representation F G). -CoInductive mx_rsim n1 (rG1 : reprG n1) n2 (rG2 : reprG n2) : Prop := +Variant mx_rsim n1 (rG1 : reprG n1) n2 (rG2 : reprG n2) : Prop := MxReprSim B of n1 = n2 & row_free B & forall x, x \in G -> rG1 x *m B = B *m rG2 x. diff --git a/mathcomp/field/algC.v b/mathcomp/field/algC.v index b045c07..f7cb614 100644 --- a/mathcomp/field/algC.v +++ b/mathcomp/field/algC.v @@ -470,7 +470,7 @@ Local Notation Creal := (Num.real : qualifier 0 algC). Fact algCi_subproof : {i : algC | i ^+ 2 = -1}. Proof. exact: GRing.imaginary_exists. Qed. -CoInductive getCrat_spec : Type := GetCrat_spec CtoQ of cancel QtoC CtoQ. +Variant getCrat_spec : Type := GetCrat_spec CtoQ of cancel QtoC CtoQ. Fact getCrat_subproof : getCrat_spec. Proof. diff --git a/mathcomp/fingroup/fingroup.v b/mathcomp/fingroup/fingroup.v index b43036b..959eea1 100644 --- a/mathcomp/fingroup/fingroup.v +++ b/mathcomp/fingroup/fingroup.v @@ -1589,7 +1589,7 @@ Proof. by move=> Gx; rewrite (rcoset_eqP (_ : x \in G :* 1)) mulg1. Qed. (* Elimination form. *) -CoInductive rcoset_repr_spec x : gT -> Type := +Variant rcoset_repr_spec x : gT -> Type := RcosetReprSpec g : g \in G -> rcoset_repr_spec x (g * x). Lemma mem_repr_rcoset x : repr (G :* x) \in G :* x. diff --git a/mathcomp/fingroup/gproduct.v b/mathcomp/fingroup/gproduct.v index 9498de7..986489b 100644 --- a/mathcomp/fingroup/gproduct.v +++ b/mathcomp/fingroup/gproduct.v @@ -132,7 +132,7 @@ Proof. by move=> A; rewrite /pprod eqxx. Qed. Lemma pprodg1 : right_id 1 pprod. Proof. by move=> A; rewrite /pprod eqxx; case: eqP. Qed. -CoInductive are_groups A B : Prop := AreGroups K H of A = K & B = H. +Variant are_groups A B : Prop := AreGroups K H of A = K & B = H. Lemma group_not0 G : set0 <> G. Proof. by move/setP/(_ 1); rewrite inE group1. Qed. diff --git a/mathcomp/fingroup/morphism.v b/mathcomp/fingroup/morphism.v index 32c01d3..3c23921 100644 --- a/mathcomp/fingroup/morphism.v +++ b/mathcomp/fingroup/morphism.v @@ -97,7 +97,7 @@ Definition clone_morphism D f := Variables (D A : {set aT}) (R : {set rT}) (x : aT) (y : rT) (f : aT -> rT). -CoInductive morphim_spec : Prop := MorphimSpec z & z \in D & z \in A & y = f z. +Variant morphim_spec : Prop := MorphimSpec z & z \in D & z \in A & y = f z. Lemma morphimP : reflect morphim_spec (y \in f @: (D :&: A)). Proof. diff --git a/mathcomp/fingroup/perm.v b/mathcomp/fingroup/perm.v index ed5d25b..3edcfed 100644 --- a/mathcomp/fingroup/perm.v +++ b/mathcomp/fingroup/perm.v @@ -220,7 +220,7 @@ Qed. Definition tperm x y := perm (can_inj (tperm_proof x y)). -CoInductive tperm_spec x y z : T -> Type := +Variant tperm_spec x y z : T -> Type := | TpermFirst of z = x : tperm_spec x y z y | TpermSecond of z = y : tperm_spec x y z x | TpermNone of z <> x & z <> y : tperm_spec x y z z. diff --git a/mathcomp/fingroup/quotient.v b/mathcomp/fingroup/quotient.v index 06feab2..03c55b3 100644 --- a/mathcomp/fingroup/quotient.v +++ b/mathcomp/fingroup/quotient.v @@ -569,7 +569,7 @@ Variables (G : {group gT}) (Kbar : {group coset_of H}). Hypothesis nHG : H <| G. -CoInductive inv_quotient_spec (P : pred {group gT}) : Prop := +Variant inv_quotient_spec (P : pred {group gT}) : Prop := InvQuotientSpec K of Kbar :=: K / H & H \subset K & P K. Lemma inv_quotientS : diff --git a/mathcomp/solvable/frobenius.v b/mathcomp/solvable/frobenius.v index eb7ceab..98657b4 100644 --- a/mathcomp/solvable/frobenius.v +++ b/mathcomp/solvable/frobenius.v @@ -93,7 +93,7 @@ Definition Frobenius_action := End FrobeniusAction. -CoInductive has_Frobenius_action G H : Prop := +Variant has_Frobenius_action G H : Prop := HasFrobeniusAction sT S to of @Frobenius_action G H sT S to. End Definitions. diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v index 64e8927..2db8927 100644 --- a/mathcomp/ssreflect/bigop.v +++ b/mathcomp/ssreflect/bigop.v @@ -525,7 +525,7 @@ Open Scope big_scope. (* packages both in in a term in which i occurs; it also depends on the *) (* iterated , as this can give more information on the expected type of *) (* the , thus allowing for the insertion of coercions. *) -CoInductive bigbody R I := BigBody of I & (R -> R -> R) & bool & R. +Variant bigbody R I := BigBody of I & (R -> R -> R) & bool & R. Definition applybig {R I} (body : bigbody R I) x := let: BigBody _ op b v := body in if b then op v x else x. diff --git a/mathcomp/ssreflect/div.v b/mathcomp/ssreflect/div.v index 59c19ce..6565ddf 100644 --- a/mathcomp/ssreflect/div.v +++ b/mathcomp/ssreflect/div.v @@ -37,7 +37,7 @@ Definition edivn_rec d := Definition edivn m d := if d > 0 then edivn_rec d.-1 m 0 else (0, m). -CoInductive edivn_spec m d : nat * nat -> Type := +Variant edivn_spec m d : nat * nat -> Type := EdivnSpec q r of m = q * d + r & (d > 0) ==> (r < d) : edivn_spec m d (q, r). Lemma edivnP m d : edivn_spec m d (edivn m d). @@ -581,7 +581,7 @@ Fixpoint egcdn_rec m n s qs := Definition egcdn m n := Bezout_rec 0 1 (egcdn_rec m n n [::]). -CoInductive egcdn_spec m n : nat * nat -> Type := +Variant egcdn_spec m n : nat * nat -> Type := EgcdnSpec km kn of km * m = kn * n + gcdn m n & kn * gcdn m n < m : egcdn_spec m n (km, kn). diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v index 159c00e..01ce7a9 100644 --- a/mathcomp/ssreflect/eqtype.v +++ b/mathcomp/ssreflect/eqtype.v @@ -420,7 +420,7 @@ Section FunWith. Variables (aT : eqType) (rT : Type). -CoInductive fun_delta : Type := FunDelta of aT & rT. +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]. @@ -501,7 +501,7 @@ Definition clone_subType U v := Variable sT : subType. -CoInductive Sub_spec : sT -> Type := SubSpec x Px : Sub_spec (Sub x Px). +Variant Sub_spec : sT -> Type := SubSpec x Px : Sub_spec (Sub x Px). Lemma SubP u : Sub_spec u. Proof. by case: sT Sub_spec SubSpec u => T' _ C rec /= _. Qed. @@ -514,7 +514,7 @@ Definition insub x := Definition insubd u0 x := odflt u0 (insub x). -CoInductive insub_spec x : option sT -> Type := +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. diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v index 4ff769e..6cff46e 100644 --- a/mathcomp/ssreflect/finset.v +++ b/mathcomp/ssreflect/finset.v @@ -1197,7 +1197,7 @@ Variables (f : aT -> rT) (f2 : aT -> aT2 -> rT). Lemma imsetP D y : reflect (exists2 x, in_mem x D & y = f x) (y \in imset f D). Proof. by rewrite [@imset]unlock inE; apply: imageP. Qed. -CoInductive imset2_spec D1 D2 y : Prop := +Variant imset2_spec D1 D2 y : Prop := Imset2spec x1 x2 of in_mem x1 D1 & in_mem x2 (D2 x1) & y = f2 x1 x2. Lemma imset2P D1 D2 y : reflect (imset2_spec D1 D2 y) (y \in imset2 f2 D1 D2). diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v index 1446fbd..fec2e35 100644 --- a/mathcomp/ssreflect/fintype.v +++ b/mathcomp/ssreflect/fintype.v @@ -325,7 +325,7 @@ Prenex Implicits pred0b. Module FiniteQuant. -CoInductive quantified := Quantified of bool. +Variant quantified := Quantified of bool. Delimit Scope fin_quant_scope with Q. (* Bogus, only used to declare scope. *) Bind Scope fin_quant_scope with quantified. @@ -483,7 +483,7 @@ rewrite [enum _](all_pred1P x _ _); first by rewrite size_filter enumP. by apply/allP=> y; rewrite mem_enum. Qed. -CoInductive pick_spec : option T -> Type := +Variant pick_spec : option T -> Type := | Pick x of P x : pick_spec (Some x) | Nopick of P =1 xpred0 : pick_spec None. @@ -938,7 +938,7 @@ Definition arg_min := odflt i0 (pick (arg_pred leq)). Definition arg_max := odflt i0 (pick (arg_pred geq)). -CoInductive extremum_spec (ord : rel nat) : I -> Type := +Variant extremum_spec (ord : rel nat) : I -> Type := ExtremumSpec i of P i & (forall j, P j -> ord (F i) (F j)) : extremum_spec ord i. @@ -1845,7 +1845,7 @@ Qed. Definition unlift n (h i : 'I_n) := omap (fun u : {j | j != h} => Ordinal (unlift_subproof u)) (insub i). -CoInductive unlift_spec n h i : option 'I_n.-1 -> Type := +Variant unlift_spec n h i : option 'I_n.-1 -> Type := | UnliftSome j of i = lift h j : unlift_spec h i (Some j) | UnliftNone of i = h : unlift_spec h i None. @@ -1900,7 +1900,7 @@ Definition split m n (i : 'I_(m + n)) : 'I_m + 'I_n := | GeqNotLtn ge_i_m => inr _ (Ordinal (split_subproof ge_i_m)) end. -CoInductive split_spec m n (i : 'I_(m + n)) : 'I_m + 'I_n -> bool -> Type := +Variant split_spec m n (i : 'I_(m + n)) : 'I_m + 'I_n -> bool -> Type := | SplitLo (j : 'I_m) of i = j :> nat : split_spec i (inl _ j) true | SplitHi (k : 'I_n) of i = m + k :> nat : split_spec i (inr _ k) false. diff --git a/mathcomp/ssreflect/generic_quotient.v b/mathcomp/ssreflect/generic_quotient.v index a3e6cac..16709ee 100644 --- a/mathcomp/ssreflect/generic_quotient.v +++ b/mathcomp/ssreflect/generic_quotient.v @@ -213,7 +213,7 @@ Variable qT : quotType T. Lemma reprK : cancel repr \pi_qT. Proof. by move=> x; rewrite !unlock repr_ofK. Qed. -CoInductive pi_spec (x : T) : T -> Type := +Variant pi_spec (x : T) : T -> Type := PiSpec y of x = y %[mod qT] : pi_spec x y. Lemma piP (x : T) : pi_spec x (repr (\pi_qT x)). @@ -466,7 +466,7 @@ Lemma right_trans (e : rel T) : symmetric e -> transitive e -> right_transitive e. Proof. by move=> s t ? * x; rewrite ![e x _]s; apply: left_trans. Qed. -CoInductive equiv_class_of (equiv : rel T) := +Variant equiv_class_of (equiv : rel T) := EquivClass of reflexive equiv & symmetric equiv & transitive equiv. Record equiv_rel := EquivRelPack { @@ -511,7 +511,7 @@ Section EncodingModuloRel. Variables (D E : Type) (ED : E -> D) (DE : D -> E) (e : rel D). -CoInductive encModRel_class_of (r : rel D) := +Variant encModRel_class_of (r : rel D) := EncModRelClassPack of (forall x, r x x -> r (ED (DE x)) x) & (r =2 e). Record encModRel := EncModRelPack { diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v index e649cbe..94873a8 100644 --- a/mathcomp/ssreflect/path.v +++ b/mathcomp/ssreflect/path.v @@ -167,7 +167,7 @@ Section EqPath. Variables (n0 : nat) (T : eqType) (x0_cycle : T) (e : rel T). Implicit Type p : seq T. -CoInductive split x : seq T -> seq T -> seq T -> Type := +Variant split x : seq T -> seq T -> seq T -> Type := Split p1 p2 : split x (rcons p1 x ++ p2) p1 p2. Lemma splitP p x (i := index x p) : @@ -177,7 +177,7 @@ move=> p_x; have lt_ip: i < size p by rewrite index_mem. by rewrite -{1}(cat_take_drop i p) (drop_nth x lt_ip) -cat_rcons nth_index. Qed. -CoInductive splitl x1 x : seq T -> Type := +Variant splitl x1 x : seq T -> Type := Splitl p1 p2 of last x1 p1 = x : splitl x1 x (p1 ++ p2). Lemma splitPl x1 p x : x \in x1 :: p -> splitl x1 x p. @@ -186,7 +186,7 @@ rewrite inE; case: eqP => [->| _ /splitP[]]; first by rewrite -(cat0s p). by split; apply: last_rcons. Qed. -CoInductive splitr x : seq T -> Type := +Variant splitr x : seq T -> Type := Splitr p1 p2 : splitr x (p1 ++ x :: p2). Lemma splitPr p x : x \in p -> splitr x p. @@ -341,7 +341,7 @@ move=> p2'x p2'y; rewrite catA !mem2_cat !mem_cat. by rewrite (negPf p2'x) (negPf p2'y) (mem2lf p2'x) andbF !orbF. Qed. -CoInductive split2r x y : seq T -> Type := +Variant split2r x y : seq T -> Type := Split2r p1 p2 of y \in x :: p2 : split2r x y (p1 ++ x :: p2). Lemma splitP2r p x y : mem2 p x y -> split2r x y p. @@ -356,7 +356,7 @@ Fixpoint shorten x p := if x \in p then shorten x p' else y :: shorten y p' else [::]. -CoInductive shorten_spec x p : T -> seq T -> Type := +Variant shorten_spec x p : T -> seq T -> Type := ShortenSpec p' of path e x p' & uniq (x :: p') & subpred (mem p') (mem p) : shorten_spec x p (last x p') p'. @@ -870,7 +870,7 @@ rewrite -[p]cat_cons -rot_size_cat rot_uniq => Up. by rewrite arc_rot ?left_arc ?mem_head. Qed. -CoInductive rot_to_arc_spec p x y := +Variant rot_to_arc_spec p x y := RotToArcSpec i p1 p2 of x :: p1 = arc p x y & y :: p2 = arc p y x & rot i p = x :: p1 ++ y :: p2 : diff --git a/mathcomp/ssreflect/plugin/v8.6/ssrbool.v b/mathcomp/ssreflect/plugin/v8.6/ssrbool.v index f81e16e..2342ec6 100644 --- a/mathcomp/ssreflect/plugin/v8.6/ssrbool.v +++ b/mathcomp/ssreflect/plugin/v8.6/ssrbool.v @@ -442,7 +442,7 @@ Section BoolIf. Variables (A B : Type) (x : A) (f : A -> B) (b : bool) (vT vF : A). -CoInductive if_spec (not_b : Prop) : bool -> A -> Set := +Variant if_spec (not_b : Prop) : bool -> A -> Set := | IfSpecTrue of b : if_spec not_b true vT | IfSpecFalse of not_b : if_spec not_b false vF. @@ -577,7 +577,7 @@ Lemma rwP2 : reflect Q b -> (P <-> Q). Proof. by move=> Qb; split=> ?; [apply: appP | apply: elimT; case: Qb]. Qed. (* Predicate family to reflect excluded middle in bool. *) -CoInductive alt_spec : bool -> Type := +Variant alt_spec : bool -> Type := | AltTrue of P : alt_spec true | AltFalse of ~~ b : alt_spec false. @@ -595,7 +595,7 @@ Hint View for apply// equivPif|3 xorPif|3 equivPifn|3 xorPifn|3. (* Allow the direct application of a reflection lemma to a boolean assertion. *) Coercion elimT : reflect >-> Funclass. -CoInductive implies P Q := Implies of P -> Q. +Variant implies P Q := Implies of P -> Q. Lemma impliesP P Q : implies P Q -> P -> Q. Proof. by case. Qed. Lemma impliesPn (P Q : Prop) : implies P Q -> ~ Q -> ~ P. Proof. by case=> iP ? /iP. Qed. @@ -1111,7 +1111,7 @@ Proof. by move=> *; apply/orP; left. Qed. Lemma subrelUr r1 r2 : subrel r2 (relU r1 r2). Proof. by move=> *; apply/orP; right. Qed. -CoInductive mem_pred := Mem of pred T. +Variant mem_pred := Mem of pred T. Definition isMem pT topred mem := mem = (fun p : pT => Mem [eta topred p]). @@ -1321,7 +1321,7 @@ End simpl_mem. (* Qualifiers and keyed predicates. *) -CoInductive qualifier (q : nat) T := Qualifier of predPredType T. +Variant qualifier (q : nat) T := Qualifier of predPredType T. Coercion has_quality n T (q : qualifier n T) : pred_class := fun x => let: Qualifier p := q in p x. @@ -1368,7 +1368,7 @@ Notation "[ 'qualify' 'an' x : T | P ]" := (Qualifier 2 (fun x : T => P%B)) Section KeyPred. Variable T : Type. -CoInductive pred_key (p : predPredType T) := DefaultPredKey. +Variant pred_key (p : predPredType T) := DefaultPredKey. Variable p : predPredType T. Structure keyed_pred (k : pred_key p) := diff --git a/mathcomp/ssreflect/plugin/v8.6/ssreflect.v b/mathcomp/ssreflect/plugin/v8.6/ssreflect.v index 860f0a1..e63b45b 100644 --- a/mathcomp/ssreflect/plugin/v8.6/ssreflect.v +++ b/mathcomp/ssreflect/plugin/v8.6/ssreflect.v @@ -174,7 +174,7 @@ Notation "T (* n *)" := (abstract T n abstract_key). Module TheCanonical. -CoInductive put vT sT (v1 v2 : vT) (s : sT) := Put. +Variant put vT sT (v1 v2 : vT) (s : sT) := Put. Definition get vT sT v s (p : @put vT sT v v s) := let: Put := p in s. @@ -265,10 +265,10 @@ Notation "{ 'type' 'of' c 'for' s }" := (dependentReturnType c s) (* We also define a simpler version ("phant" / "Phant") of phantom for the *) (* common case where p_type is Type. *) -CoInductive phantom T (p : T) := Phantom. +Variant phantom T (p : T) := Phantom. Implicit Arguments phantom []. Implicit Arguments Phantom []. -CoInductive phant (p : Type) := Phant. +Variant phant (p : Type) := Phant. (* Internal tagging used by the implementation of the ssreflect elim. *) diff --git a/mathcomp/ssreflect/plugin/v8.6/ssrfun.v b/mathcomp/ssreflect/plugin/v8.6/ssrfun.v index c517b92..7cb30ff 100644 --- a/mathcomp/ssreflect/plugin/v8.6/ssrfun.v +++ b/mathcomp/ssreflect/plugin/v8.6/ssrfun.v @@ -419,7 +419,7 @@ Section SimplFun. Variables aT rT : Type. -CoInductive simpl_fun := SimplFun of aT -> rT. +Variant simpl_fun := SimplFun of aT -> rT. Definition fun_of_simpl f := fun x => let: SimplFun lam := f in lam x. @@ -777,7 +777,7 @@ Section Bijections. Variables (A B : Type) (f : B -> A). -CoInductive bijective : Prop := Bijective g of cancel f g & cancel g f. +Variant bijective : Prop := Bijective g of cancel f g & cancel g f. Hypothesis bijf : bijective. diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v index 648737b..4bbea2a 100644 --- a/mathcomp/ssreflect/prime.v +++ b/mathcomp/ssreflect/prime.v @@ -77,7 +77,7 @@ Fixpoint elogn2 e q r {struct q} := | q'.+1, r'.+2 => elogn2 e q' r' end. -CoInductive elogn2_spec n : nat * nat -> Type := +Variant elogn2_spec n : nat * nat -> Type := Elogn2Spec e m of n = 2 ^ e * m.*2.+1 : elogn2_spec n (e, m). Lemma elogn2P n : elogn2_spec n.+1 (elogn2 0 n n). @@ -91,7 +91,7 @@ Qed. Definition ifnz T n (x y : T) := if n is 0 then y else x. -CoInductive ifnz_spec T n (x y : T) : T -> Type := +Variant ifnz_spec T n (x y : T) : T -> Type := | IfnzPos of n > 0 : ifnz_spec n x y x | IfnzZero of n = 0 : ifnz_spec n x y y. diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index 4347983..e9d29fb 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -305,7 +305,7 @@ Proof. by rewrite -cats1 -catA. Qed. Lemma rcons_cat x s1 s2 : rcons (s1 ++ s2) x = s1 ++ rcons s2 x. Proof. by rewrite -!cats1 catA. Qed. -CoInductive last_spec : seq T -> Type := +Variant last_spec : seq T -> Type := | LastNil : last_spec [::] | LastRcons s x : last_spec (rcons s x). @@ -1272,7 +1272,7 @@ Proof. by move=> x; rewrite -{2}(cat_take_drop n0 s) !mem_cat /= orbC. Qed. Lemma eqseq_rot s1 s2 : (rot n0 s1 == rot n0 s2) = (s1 == s2). Proof. by apply: inj_eq; apply: rot_inj. Qed. -CoInductive rot_to_spec s x := RotToSpec i s' of rot i s = x :: s'. +Variant rot_to_spec s x := RotToSpec i s' of rot i s = x :: s'. Lemma rot_to s x : x \in s -> rot_to_spec s x. Proof. diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v index cfe0fa3..4619db7 100644 --- a/mathcomp/ssreflect/ssrnat.v +++ b/mathcomp/ssreflect/ssrnat.v @@ -418,7 +418,7 @@ Proof. exact: (@le_irrelevance m.+1). Qed. (* Comparison predicates. *) -CoInductive leq_xor_gtn m n : bool -> bool -> Set := +Variant leq_xor_gtn m n : bool -> bool -> Set := | LeqNotGtn of m <= n : leq_xor_gtn m n true false | GtnNotLeq of n < m : leq_xor_gtn m n false true. @@ -427,21 +427,21 @@ Proof. by rewrite ltnNge; case le_mn: (m <= n); constructor; rewrite // ltnNge le_mn. Qed. -CoInductive ltn_xor_geq m n : bool -> bool -> Set := +Variant ltn_xor_geq m n : bool -> bool -> Set := | LtnNotGeq of m < n : ltn_xor_geq m n false true | GeqNotLtn of n <= m : ltn_xor_geq m n true false. Lemma ltnP m n : ltn_xor_geq m n (n <= m) (m < n). Proof. by rewrite -(ltnS n); case: leqP; constructor. Qed. -CoInductive eqn0_xor_gt0 n : bool -> bool -> Set := +Variant eqn0_xor_gt0 n : bool -> bool -> Set := | Eq0NotPos of n = 0 : eqn0_xor_gt0 n true false | PosNotEq0 of n > 0 : eqn0_xor_gt0 n false true. Lemma posnP n : eqn0_xor_gt0 n (n == 0) (0 < n). Proof. by case: n; constructor. Qed. -CoInductive compare_nat m n : +Variant compare_nat m n : bool -> bool -> bool -> bool -> bool -> bool -> Set := | CompareNatLt of m < n : compare_nat m n true false true false false false | CompareNatGt of m > n : compare_nat m n false true false true false false @@ -751,7 +751,7 @@ Proof. by case: exP => i Pi; exists (m - i); rewrite subKn ?ubP. Qed. Definition ex_maxn := m - ex_minn ex_maxn_subproof. -CoInductive ex_maxn_spec : nat -> Type := +Variant ex_maxn_spec : nat -> Type := ExMaxnSpec i of P i & (forall j, P j -> j <= i) : ex_maxn_spec i. Lemma ex_maxnP : ex_maxn_spec ex_maxn. diff --git a/mathcomp/ssreflect/tuple.v b/mathcomp/ssreflect/tuple.v index e06bd38..64585f6 100644 --- a/mathcomp/ssreflect/tuple.v +++ b/mathcomp/ssreflect/tuple.v @@ -220,7 +220,7 @@ Proof. by []. Qed. Lemma tuple0 : all_equal_to ([tuple] : 0.-tuple T). Proof. by move=> t; apply: val_inj; case: t => [[]]. Qed. -CoInductive tuple1_spec : n.+1.-tuple T -> Type := +Variant tuple1_spec : n.+1.-tuple T -> Type := Tuple1spec x t : tuple1_spec [tuple of x :: t]. Lemma tupleP u : tuple1_spec u. -- cgit v1.2.3