diff options
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 15 | ||||
| -rw-r--r-- | mathcomp/algebra/matrix.v | 16 | ||||
| -rw-r--r-- | mathcomp/field/falgebra.v | 11 | ||||
| -rw-r--r-- | mathcomp/field/separable.v | 13 | ||||
| -rw-r--r-- | mathcomp/ssreflect/path.v | 32 | ||||
| -rw-r--r-- | mathcomp/ssreflect/seq.v | 124 |
6 files changed, 140 insertions, 71 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 9ea88fd..a61116b 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -90,11 +90,16 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). - in `seq.v`, new lemma `mkseqP` to abstract a sequence `s` with `mkseq f n`, where `f` and `n` are fresh variables. -- in `seq.v`, new high-order predicate `allrel r s` which - asserts that a relation `r` holds on all pairs of elements of `s`, and - + lemmas `allrel_map`, `allrelP` and `allrel0`. - + lemmas `allrel1`, `allrel2` and `allrel_cons`, - under assumptions of reflexivity and symmetry of `r`. +- in `seq.v`, new high-order relation `allrel r xs ys` which asserts that + `r x y` holds whenever `x` is in `xs` and `y` is in `ys`, new notation + `all2rel r xs (:= allrel r xs xs)` which asserts that `r` holds on all + pairs of elements of `xs`, and + + lemmas `allrel0(l|r)`, `allrel_cons(l|r|2)`, `allrel1(l|r)`, + `allrel_cat(l|r)`, `allrel_allpairsE`, `eq_in_allrel`, `eq_allrel`, + `allrelC`, `allrel_map(l|r)`, `allrelP`, + + lemmas `all2rel1`, `all2rel2`, and `all2rel_cons` + under assumptions of symmetry of `r`. + - in `mxpoly.v`, new lemmas `mxminpoly_minP` and `dvd_mxminpoly`. - in `mxalgebra.v` new lemmas `row_base0`, `sub_kermx`, `kermx0` and `mulmx_free_eq0`. diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index 2bca0b2..e7e0e35 100644 --- a/mathcomp/algebra/matrix.v +++ b/mathcomp/algebra/matrix.v @@ -110,9 +110,9 @@ From mathcomp Require Import div prime binomial ssralg finalg zmodp countalg. (* A \in unitmx == A is invertible (R must be a comUnitRingType). *) (* invmx A == the inverse matrix of A if A \in unitmx A, otherwise A. *) (* A \is a mxOver S == the matrix A has its coefficients in S. *) -(* comm_mx A B := A *m B = B *m A *) -(* comm_mxb A B := A *m B == B *m A *) -(* all_comm_mx As := allrel comm_mxb *) +(* comm_mx A B := A *m B = B *m A *) +(* comm_mxb A B := A *m B == B *m A *) +(* all_comm_mx As fs := all2rel comm_mxb fs *) (* The following operations provide a correspondence between linear functions *) (* and matrices: *) (* lin1_mx f == the m x n matrix that emulates via right product *) @@ -2772,23 +2772,21 @@ Proof. by move=> comm_mxfF; elim/big_ind: _ => // g h; apply: comm_mxD. Qed. Lemma comm_mxP f g : reflect (comm_mx f g) (comm_mxb f g). Proof. exact: eqP. Qed. -Notation all_comm_mx := (allrel comm_mxb). +Notation all_comm_mx fs := (all2rel comm_mxb fs). Lemma all_comm_mxP fs : reflect {in fs &, forall f g, f *m g = g *m f} (all_comm_mx fs). Proof. by apply: (iffP allrelP) => fsP ? ? ? ?; apply/eqP/fsP. Qed. Lemma all_comm_mx1 f : all_comm_mx [:: f]. -Proof. by rewrite /comm_mxb allrel1. Qed. +Proof. by rewrite /comm_mxb all2rel1. Qed. Lemma all_comm_mx2P f g : reflect (f *m g = g *m f) (all_comm_mx [:: f; g]). -Proof. -by rewrite /comm_mxb; apply: (iffP and4P) => [[_/eqP//]|->]; rewrite ?eqxx. -Qed. +Proof. by rewrite /comm_mxb /= all2rel2 ?eqxx //; exact: eqP. Qed. Lemma all_comm_mx_cons f fs : all_comm_mx (f :: fs) = all (comm_mxb f) fs && all_comm_mx fs. -Proof. by rewrite /comm_mxb [LHS]allrel_cons. Qed. +Proof. by rewrite /comm_mxb /= all2rel_cons //= eqxx. Qed. End CommMx. Notation all_comm_mx := (allrel comm_mxb). diff --git a/mathcomp/field/falgebra.v b/mathcomp/field/falgebra.v index 9069818..8fb123e 100644 --- a/mathcomp/field/falgebra.v +++ b/mathcomp/field/falgebra.v @@ -1078,21 +1078,20 @@ Section Class_Def. Variables aT rT : FalgType K. Definition ahom_in (U : {vspace aT}) (f : 'Hom(aT, rT)) := - let fM_at x y := f (x * y) == f x * f y in - all (fun x => all (fM_at x) (vbasis U)) (vbasis U) && (f 1 == 1). + all2rel (fun x y : aT => f (x * y) == f x * f y) (vbasis U) && (f 1 == 1). Lemma ahom_inP {f : 'Hom(aT, rT)} {U : {vspace aT}} : reflect ({in U &, {morph f : x y / x * y >-> x * y}} * (f 1 = 1)) (ahom_in U f). Proof. -apply: (iffP andP) => [[/allP fM /eqP f1] | [fM f1]]; last first. - rewrite f1; split=> //; apply/allP=> x Ax; apply/allP=> y Ay. +apply: (iffP andP) => [[/allrelP fM /eqP f1] | [fM f1]]; last first. + rewrite f1; split=> //; apply/allrelP => x y Ax Ay. by rewrite fM // vbasis_mem. -split=> // x y /coord_vbasis -> /coord_vbasis ->. +split=> // x y /coord_vbasis -> /coord_vbasis ->. rewrite !mulr_suml ![f _]linear_sum mulr_suml; apply: eq_bigr => i _ /=. rewrite !mulr_sumr linear_sum; apply: eq_bigr => j _ /=. rewrite !linearZ -!scalerAr -!scalerAl 2!linearZ /=; congr (_ *: (_ *: _)). -by apply/eqP/(allP (fM _ _)); apply: memt_nth. +by apply/eqP/fM; apply: memt_nth. Qed. Lemma ahomP {f : 'Hom(aT, rT)} : reflect (lrmorphism f) (ahom_in {:aT} f). diff --git a/mathcomp/field/separable.v b/mathcomp/field/separable.v index 6320343..d07839c 100644 --- a/mathcomp/field/separable.v +++ b/mathcomp/field/separable.v @@ -288,8 +288,8 @@ Variables (K : {vspace L}) (D : 'End(L)). (* A deriviation only needs to be additive and satify Lebniz's law, but all *) (* the deriviations used here are going to be linear, so we only define *) (* the Derivation predicate for linear endomorphisms. *) -Definition Derivation (s := vbasis K) : bool := - all (fun u => all (fun v => D (u * v) == D u * v + u * D v) s) s. +Definition Derivation : bool := + all2rel (fun u v => D (u * v) == D u * v + u * D v) (vbasis K). Hypothesis derD : Derivation. @@ -299,7 +299,7 @@ move=> u v /coord_vbasis-> /coord_vbasis->. rewrite !(mulr_sumr, linear_sum) -big_split; apply: eq_bigr => /= j _. rewrite !mulr_suml linear_sum -big_split; apply: eq_bigr => /= i _. rewrite !(=^~ scalerAl, linearZZ) -!scalerAr linearZZ -!scalerDr !scalerA /=. -by congr (_ *: _); apply/eqP; rewrite (allP (allP derD _ _)) ?memt_nth. +by congr (_ *: _); apply/eqP/(allrelP derD); exact: memt_nth. Qed. Lemma Derivation_mul_poly (Dp := map_poly D) : @@ -314,7 +314,7 @@ End Derivation. Lemma DerivationS E K D : (K <= E)%VS -> Derivation E D -> Derivation K D. Proof. -move/subvP=> sKE derD; apply/allP=> x Kx; apply/allP=> y Ky; apply/eqP. +move/subvP=> sKE derD; apply/allrelP=> x y Kx Ky; apply/eqP. by rewrite (Derivation_mul derD) ?sKE // vbasis_mem. Qed. @@ -492,8 +492,7 @@ Qed. Lemma extendDerivationP : separable_element K x -> Derivation <<K; x>> (extendDerivation K). Proof. -move=> sep; apply/allP=> u /vbasis_mem Hu; apply/allP=> v /vbasis_mem Hv. -apply/eqP. +move=> sep; apply/allrelP=> u v /vbasis_mem Hu /vbasis_mem Hv; apply/eqP. rewrite -(Fadjoin_poly_eq Hu) -(Fadjoin_poly_eq Hv) -hornerM. rewrite !{1}extendDerivation_horner ?{1}rpredM ?Fadjoin_polyOver //. rewrite (Derivation_mul_poly derD) ?Fadjoin_polyOver //. @@ -528,7 +527,7 @@ have DK_0: (K <= lker D)%VS. apply/subvP=> v Kv; rewrite memv_ker lfunE /= Fadjoin_polyC //. by rewrite derivC horner0. have Dder: Derivation <<K; x>> D. - apply/allP=> u /vbasis_mem Kx_u; apply/allP=> v /vbasis_mem Kx_v; apply/eqP. + apply/allrelP=> u v /vbasis_mem Kx_u /vbasis_mem Kx_v; apply/eqP. rewrite !lfunE /=; set Px := Fadjoin_poly K x. set Px_u := Px u; rewrite -(Fadjoin_poly_eq Kx_u) -/Px -/Px_u. set Px_v := Px v; rewrite -(Fadjoin_poly_eq Kx_v) -/Px -/Px_v. diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v index e9143fe..8ee8bea 100644 --- a/mathcomp/ssreflect/path.v +++ b/mathcomp/ssreflect/path.v @@ -1097,24 +1097,24 @@ Hypothesis (leT_total : total leT) (leT'_tr : transitive leT'). Let leT_lex := [rel x y | leT x y && (leT y x ==> leT' x y)]. Lemma merge_stable_path x s1 s2 : - all (fun y => all (leT' y) s2) s1 -> - path leT_lex x s1 -> path leT_lex x s2 -> path leT_lex x (merge leT s1 s2). + allrel leT' s1 s2 -> path leT_lex x s1 -> path leT_lex x s2 -> + path leT_lex x (merge leT s1 s2). Proof. elim: s1 s2 x => //= x s1 ih1; elim => //= y s2 ih2 h. -rewrite all_predI -andbA => /and4P [xy' xs2 ys1 s1s2]. -case/andP => hx xs1 /andP [] hy ys2; case: ifP => xy /=; rewrite (hx, hy) /=. -- by apply: ih1; rewrite ?all_predI ?ys1 //= xy xy' implybT. -- by apply: ih2; have:= leT_total x y; rewrite ?xs2 //= xy => /= ->. +rewrite allrel_cons2 => /and4P [xy' xs2 ys1 s1s2] /andP [hx xs1] /andP [hy ys2]. +case: ifP => xy /=; rewrite (hx, hy) /=. +- by apply: ih1; rewrite ?allrel_consr ?ys1 //= xy xy' implybT. +- by apply: ih2; have:= leT_total x y; rewrite ?allrel_consl ?xs2 ?xy //= => ->. Qed. Lemma merge_stable_sorted s1 s2 : - all (fun x => all (leT' x) s2) s1 -> - sorted leT_lex s1 -> sorted leT_lex s2 -> sorted leT_lex (merge leT s1 s2). + allrel leT' s1 s2 -> sorted leT_lex s1 -> sorted leT_lex s2 -> + sorted leT_lex (merge leT s1 s2). Proof. -case: s1 s2 => [|x s1] [|y s2] //=; rewrite all_predI -andbA. +case: s1 s2 => [|x s1] [|y s2] //=; rewrite allrel_consl allrel_consr /= -andbA. case/and4P => [xy' xs2 ys1 s1s2] xs1 ys2; rewrite -/(merge _ (_ :: _)). by case: ifP (leT_total x y) => /= xy yx; apply/merge_stable_path; - rewrite /= ?(all_predI, xs2, ys1, xy, yx, xy', implybT). + rewrite /= ?(allrel_consl, allrel_consr, xs2, ys1, xy, yx, xy', implybT). Qed. End Stability_merge. @@ -1142,9 +1142,9 @@ Proof. elim: ss s1 => [] // [] //= m s2 ss ihss s1; rewrite -2!andbA. move=> /and5P [sorted_s1 perm_s1 sorted_s2 perm_s2 hss]; apply: ihss. rewrite hss size_merge size_cat iotaD addnC -size_cat perm_merge perm_cat //. -rewrite merge_stable_sorted // (perm_all _ perm_s2); apply/allP => n. -rewrite mem_iota (perm_all _ perm_s1) => /andP [_ n_lt]; apply/allP => p. -by rewrite mem_iota size_cat addnC => /andP [] /(leq_trans n_lt). +rewrite merge_stable_sorted //; apply/allrelP => n p. +rewrite (perm_mem perm_s1) (perm_mem perm_s2) !mem_iota size_cat addnC. +by move=> /andP [_ n_lt] /andP [] /(leq_trans n_lt). Qed. Let pop_stable s1 ss : @@ -1153,9 +1153,9 @@ Proof. elim: ss s1 => [s1 /andP [] /andP [] //|s2 ss ihss s1]; rewrite /= -2!andbA. move=> /and5P [sorted_s1 perm_s1 sorted_s2 perm_s2 hss]; apply: ihss. rewrite /= hss size_merge size_cat iotaD addnC -size_cat perm_merge perm_cat //. -rewrite merge_stable_sorted // (perm_all _ perm_s2); apply/allP => n. -rewrite mem_iota (perm_all _ perm_s1) => /andP [_ n_lt]; apply/allP => p. -by rewrite mem_iota size_cat addnC => /andP [] /(leq_trans n_lt). +rewrite merge_stable_sorted //; apply/allrelP => n p. +rewrite (perm_mem perm_s1) (perm_mem perm_s2) !mem_iota size_cat addnC. +by move=> /andP [_ n_lt] /andP [] /(leq_trans n_lt). Qed. Lemma sort_iota_stable n : sorted lt_lex (sort leN (iota 0 n)). diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index 48a59ee..abca0d9 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -132,8 +132,10 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat. (* i.e. self expanding definition for *) (* [seq f x y | x <- s, y <- t] *) (* := [:: f x_1 y_1; ...; f x_1 y_m; f x_2 y_1; ...; f x_n y_m] *) -(* allrel r s := all id [seq r x y | x <- xs, y <- xs] *) -(* == the proposition r x y holds for all possible x, y in xs *) +(* allrel r xs ys := all [pred x | all (r x) ys] xs *) +(* == r x y holds whenever x is in xs and y is in ys *) +(* all2rel r xs := allrel r xs xs *) +(* == the proposition r x y holds for all possible x, y in xs. *) (* map f s == the sequence [:: f x_1, ..., f x_n]. *) (* pmap pf s == the sequence [:: y_i1, ..., y_ik] where i1 < ... < ik, *) (* pf x_i = Some y_i, and pf x_j = None iff j is not in *) @@ -3484,45 +3486,111 @@ Arguments perm_consP {T x s t}. Section AllRel. -Definition allrel {T : Type} (r : rel T) xs := - all id [seq r x y | x <- xs, y <- xs]. +Variables (T S : Type) (r : T -> S -> bool). +Implicit Types (x : T) (y : S) (xs : seq T) (ys : seq S). -Lemma allrel0 (T : Type) (r : rel T) : allrel r [::]. +Definition allrel xs ys := all [pred x | all (r x) ys] xs. + +Lemma allrel0l ys : allrel [::] ys. Proof. by []. Qed. + +Lemma allrel0r xs : allrel xs [::]. Proof. by elim: xs. Qed. + +Lemma allrel_consl x xs ys : allrel (x :: xs) ys = all (r x) ys && allrel xs ys. Proof. by []. Qed. -Lemma allrel_map (T T' : Type) (f : T' -> T) (r : rel T) xs : - allrel r (map f xs) = allrel (relpre f r) xs. -Proof. by rewrite /allrel allpairs_mapl allpairs_mapr. Qed. +Lemma allrel_consr xs y ys : + allrel xs (y :: ys) = all (r^~ y) xs && allrel xs ys. +Proof. exact: all_predI. Qed. -Lemma allrelP {T : eqType} {r : rel T} {xs : seq T} : - reflect {in xs &, forall x y, r x y} (allrel r xs). -Proof. exact: all_allpairsP. Qed. +Lemma allrel_cons2 x y xs ys : + allrel (x :: xs) (y :: ys) = + [&& r x y, all (r x) ys, all (r^~ y) xs & allrel xs ys]. +Proof. by rewrite /= allrel_consr -andbA. Qed. -Variable (T : nonPropType) (r : rel T). -Implicit Types (xs : seq T) (x y z : T). -Hypothesis (rxx : reflexive r) (rsym : symmetric r). +Lemma allrel1l x ys : allrel [:: x] ys = all (r x) ys. Proof. exact: andbT. Qed. -Lemma allrel1 x : allrel r [:: x]. -Proof. by rewrite /allrel/= rxx. Qed. +Lemma allrel1r xs y : allrel xs [:: y] = all (r^~ y) xs. +Proof. by rewrite allrel_consr allrel0r andbT. Qed. -Lemma allrel2 x y : allrel r [:: x; y] = r x y. -Proof. by rewrite /allrel/= !rxx [r y x]rsym !(andbT, andbb). Qed. +Lemma allrel_catl xs xs' ys : + allrel (xs ++ xs') ys = allrel xs ys && allrel xs' ys. +Proof. exact: all_cat. Qed. -Lemma allrel_cons x xs : - allrel r (x :: xs) = all (r x) xs && allrel r xs. +Lemma allrel_catr xs ys ys' : + allrel xs (ys ++ ys') = allrel xs ys && allrel xs ys'. Proof. -case: (mkseqP x (_ :: _)) => -[//|n] f [-> ->]. -rewrite !allrel_map all_map; apply/allrelP/andP => /= [rf|]. - split; first by apply/allP => i iP /=; rewrite rf// in_cons iP orbT. - by apply/allrelP => i j iP jP /=; rewrite rf// in_cons (iP, jP) orbT. -move=> [/allP/= rf0 /allrelP/= rf] i j; rewrite !in_cons. -by move=> /predU1P[->|iP] /predU1P[->|jP]//=; rewrite 2?(rf0, rsym)//= rf. +elim: ys => /= [|y ys ihys]; first by rewrite allrel0r. +by rewrite !allrel_consr ihys andbA. Qed. +Lemma allrel_allpairsE xs ys : + allrel xs ys = all id [seq r x y | x <- xs, y <- ys]. +Proof. by elim: xs => //= x xs ->; rewrite all_cat all_map. Qed. + End AllRel. -Arguments allrel {T} r xs. -Arguments allrelP {T r xs}. +Arguments allrel {T S} r xs ys : simpl never. +Arguments allrel0l {T S} r ys. +Arguments allrel0r {T S} r xs. +Arguments allrel_consl {T S} r x xs ys. +Arguments allrel_consr {T S} r xs y ys. +Arguments allrel1l {T S} r x ys. +Arguments allrel1r {T S} r xs y. +Arguments allrel_catl {T S} r xs xs' ys. +Arguments allrel_catr {T S} r xs ys ys'. +Arguments allrel_allpairsE {T S} r xs ys. + +Notation all2rel r xs := (allrel r xs xs). + +Lemma eq_in_allrel {T S : Type} (P : {pred T}) (Q : {pred S}) r r' : + {in P & Q, r =2 r'} -> + forall xs ys, all P xs -> all Q ys -> allrel r xs ys = allrel r' xs ys. +Proof. +move=> rr' + ys; elim=> //= x xs IH /andP [Px Pxs] Qys. +congr andb => /=; last exact: IH. +by elim: ys Qys {IH} => //= y ys IH /andP [Qy Qys]; rewrite rr' // IH. +Qed. + +Lemma eq_allrel {T S : Type} (r r': T -> S -> bool) : + r =2 r' -> allrel r =2 allrel r'. +Proof. by move=> rr' xs ys; apply/eq_in_allrel/all_predT/all_predT. Qed. + +Lemma allrelC {T S : Type} (r : T -> S -> bool) xs ys : + allrel r xs ys = allrel (fun y => r^~ y) ys xs. +Proof. by elim: xs => [|x xs ih]; [elim: ys | rewrite allrel_consr -ih]. Qed. + +Lemma allrel_mapl {T T' S : Type} (f : T' -> T) (r : T -> S -> bool) xs ys : + allrel r (map f xs) ys = allrel (fun x => r (f x)) xs ys. +Proof. exact: all_map. Qed. + +Lemma allrel_mapr {T S S' : Type} (f : S' -> S) (r : T -> S -> bool) xs ys : + allrel r xs (map f ys) = allrel (fun x y => r x (f y)) xs ys. +Proof. by rewrite allrelC allrel_mapl allrelC. Qed. + +Lemma allrelP {T S : eqType} {r : T -> S -> bool} {xs ys} : + reflect {in xs & ys, forall x y, r x y} (allrel r xs ys). +Proof. by rewrite allrel_allpairsE; exact: all_allpairsP. Qed. + +Section All2Rel. + +Variable (T : nonPropType) (r : rel T). +Implicit Types (x y z : T) (xs : seq T). +Hypothesis (rsym : symmetric r). + +Lemma all2rel1 x : all2rel r [:: x] = r x x. +Proof. by rewrite /allrel /= !andbT. Qed. + +Lemma all2rel2 x y : all2rel r [:: x; y] = r x x && r y y && r x y. +Proof. by rewrite /allrel /= rsym; do 3 case: r. Qed. + +Lemma all2rel_cons x xs : + all2rel r (x :: xs) = [&& r x x, all (r x) xs & all2rel r xs]. +Proof. +rewrite allrel_cons2; congr andb; rewrite andbA -all_predI; congr andb. +by elim: xs => //= y xs ->; rewrite rsym andbb. +Qed. + +End All2Rel. Section Permutations. |