From 783631c771ec76baa4ff9d292c1eddfb58f67f4c Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Fri, 20 Nov 2020 16:52:52 +0900 Subject: Generalize `allrel` to take two lists as arguments --- mathcomp/algebra/matrix.v | 16 +++---- mathcomp/field/falgebra.v | 11 +++-- mathcomp/field/separable.v | 13 +++--- mathcomp/ssreflect/path.v | 33 +++++++------- mathcomp/ssreflect/seq.v | 110 +++++++++++++++++++++++++++++++++------------ 5 files changed, 116 insertions(+), 67 deletions(-) diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index 2bca0b2..5e42904 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 := all1rel 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 := (all1rel 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 all1rel1. 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 /= all1rel2 ?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 /= all1rel_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..97a5f22 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). + all1rel (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..7e208cd 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 := + all1rel (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 <> (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 <> 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..112f129 100644 --- a/mathcomp/ssreflect/path.v +++ b/mathcomp/ssreflect/path.v @@ -1097,24 +1097,25 @@ 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_consl allrel_consr /= -andbA. +move=> /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 +1143,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 +1154,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..c3936bb 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -132,8 +132,11 @@ 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 *) +(* == the proposition r x y holds for all x and y respectively *) +(* in xs and ys. *) +(* all1rel 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 +3487,94 @@ 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 [::]. -Proof. by []. Qed. +Definition allrel xs ys := all [pred x | all (r x) ys] xs. -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 allrel0s ys : allrel [::] ys. Proof. by []. 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 allrels0 xs : allrel xs [::]. Proof. by elim: xs. Qed. -Variable (T : nonPropType) (r : rel T). -Implicit Types (xs : seq T) (x y z : T). -Hypothesis (rxx : reflexive r) (rsym : symmetric r). +Lemma allrel_consl x xs ys : allrel (x :: xs) ys = all (r x) ys && allrel xs ys. +Proof. by []. Qed. + +Lemma allrel_consr xs y ys : + allrel xs (y :: ys) = all (r^~ y) xs && allrel xs ys. +Proof. exact: all_predI. Qed. + +Lemma allrel1s 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 allrels1 xs y : allrel xs [:: y] = all (r^~ y) xs. +Proof. by rewrite allrel_consr allrels0 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 allrels0. +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 allrel0s {T S} r ys. +Arguments allrels0 {T S} r xs. +Arguments allrel_consl {T S} r x xs ys. +Arguments allrel_consr {T S} r xs y ys. +Arguments allrel1s {T S} r x ys. +Arguments allrels1 {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 all1rel r xs := (allrel r xs xs). + +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 All1Rel. + +Variable (T : nonPropType) (r : rel T). +Implicit Types (x y z : T) (xs : seq T). +Hypothesis (rsym : symmetric r). + +Lemma all1rel1 x : all1rel r [:: x] = r x x. +Proof. by rewrite /allrel /= !andbT. Qed. + +Lemma all1rel2 x y : all1rel r [:: x; y] = r x x && r y y && r x y. +Proof. by rewrite /allrel /= rsym; do 3 case: r. Qed. + +Lemma all1rel_cons x xs : + all1rel r (x :: xs) = [&& r x x, all (r x) xs & all1rel r xs]. +Proof. +rewrite allrel_consl allrel_consr /= !andbA [r x x && _]andbC -andbA andbACA. +rewrite -[RHS]andbA; congr andb; rewrite -all_predI. +by elim: xs => //= y xs ->; rewrite rsym andbb. +Qed. + +End All1Rel. Section Permutations. -- cgit v1.2.3 From c2b2ea2dce5fa7b8d428a5072f2e86979eeb1d98 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Sat, 21 Nov 2020 13:30:45 +0900 Subject: Apply suggestions from code review Co-authored-by: Christian Doczkal --- mathcomp/ssreflect/seq.v | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index c3936bb..777041f 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -133,8 +133,7 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat. (* [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 xs ys := all [pred x | all (r x) ys] xs *) -(* == the proposition r x y holds for all x and y respectively *) -(* in xs and ys. *) +(* == r x y holds whenever x is in xs and y is in ys *) (* all1rel 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]. *) -- cgit v1.2.3 From 43796130c3e59c0651a283e6654a7d82acbfeed3 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Sat, 21 Nov 2020 13:32:03 +0900 Subject: Apply suggestions from code review Co-authored-by: Cyril Cohen --- mathcomp/ssreflect/path.v | 3 +-- mathcomp/ssreflect/seq.v | 41 +++++++++++++++++++++++++++++------------ 2 files changed, 30 insertions(+), 14 deletions(-) diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v index 112f129..8ee8bea 100644 --- a/mathcomp/ssreflect/path.v +++ b/mathcomp/ssreflect/path.v @@ -1101,8 +1101,7 @@ Lemma merge_stable_path x s1 s2 : path leT_lex x (merge leT s1 s2). Proof. elim: s1 s2 x => //= x s1 ih1; elim => //= y s2 ih2 h. -rewrite allrel_consl allrel_consr /= -andbA. -move=> /and4P [xy' xs2 ys1 s1s2] /andP [hx xs1] /andP [hy ys2]. +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 //= => ->. diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index 777041f..9747f73 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -3491,9 +3491,9 @@ Implicit Types (x : T) (y : S) (xs : seq T) (ys : seq S). Definition allrel xs ys := all [pred x | all (r x) ys] xs. -Lemma allrel0s ys : allrel [::] ys. Proof. by []. Qed. +Lemma allrel0l ys : allrel [::] ys. Proof. by []. Qed. -Lemma allrels0 xs : allrel xs [::]. Proof. by elim: xs. 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. @@ -3502,10 +3502,15 @@ Lemma allrel_consr xs y ys : allrel xs (y :: ys) = all (r^~ y) xs && allrel xs ys. Proof. exact: all_predI. Qed. -Lemma allrel1s x ys : allrel [:: x] ys = all (r x) ys. Proof. exact: andbT. 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. -Lemma allrels1 xs y : allrel xs [:: y] = all (r^~ y) xs. -Proof. by rewrite allrel_consr allrels0 andbT. Qed. +Lemma allrel1l x ys : allrel [:: x] ys = all (r x) ys. Proof. exact: andbT. Qed. + +Lemma allrel1r xs y : allrel xs [:: y] = all (r^~ y) xs. +Proof. by rewrite allrel_consr allrel0r andbT. Qed. Lemma allrel_catl xs xs' ys : allrel (xs ++ xs') ys = allrel xs ys && allrel xs' ys. @@ -3514,7 +3519,7 @@ Proof. exact: all_cat. Qed. Lemma allrel_catr xs ys ys' : allrel xs (ys ++ ys') = allrel xs ys && allrel xs ys'. Proof. -elim: ys => /= [|y ys ihys]; first by rewrite allrels0. +elim: ys => /= [|y ys ihys]; first by rewrite allrel0r. by rewrite !allrel_consr ihys andbA. Qed. @@ -3525,18 +3530,31 @@ Proof. by elim: xs => //= x xs ->; rewrite all_cat all_map. Qed. End AllRel. Arguments allrel {T S} r xs ys : simpl never. -Arguments allrel0s {T S} r ys. -Arguments allrels0 {T S} r xs. +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 allrel1s {T S} r x ys. -Arguments allrels1 {T S} r xs y. +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 all1rel 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) xs ys : + r =2 r' -> allrel r xs ys = allrel r' xs ys. +Proof. by move=> rr'; 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. @@ -3568,8 +3586,7 @@ Proof. by rewrite /allrel /= rsym; do 3 case: r. Qed. Lemma all1rel_cons x xs : all1rel r (x :: xs) = [&& r x x, all (r x) xs & all1rel r xs]. Proof. -rewrite allrel_consl allrel_consr /= !andbA [r x x && _]andbC -andbA andbACA. -rewrite -[RHS]andbA; congr andb; rewrite -all_predI. +rewrite allrel_cons2; congr andb; rewrite andbA -all_predI; congr andb. by elim: xs => //= y xs ->; rewrite rsym andbb. Qed. -- cgit v1.2.3 From d844896e6418bb00418964bb4ae4219e2bd6b69c Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Wed, 25 Nov 2020 22:14:58 +0900 Subject: Rename `all1rel` to `all2rel`, restate `eq_allrel`, and add CHANGELOG entries Co-authored-by: Cyril Cohen --- CHANGELOG_UNRELEASED.md | 15 ++++++++++----- mathcomp/algebra/matrix.v | 10 +++++----- mathcomp/field/falgebra.v | 2 +- mathcomp/field/separable.v | 2 +- mathcomp/ssreflect/seq.v | 22 +++++++++++----------- 5 files changed, 28 insertions(+), 23 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 5e42904..e7e0e35 100644 --- a/mathcomp/algebra/matrix.v +++ b/mathcomp/algebra/matrix.v @@ -112,7 +112,7 @@ From mathcomp Require Import div prime binomial ssralg finalg zmodp countalg. (* 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 fs := all1rel comm_mxb fs *) +(* 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,21 +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 fs := (all1rel comm_mxb fs). +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 all1rel1. 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 /= all1rel2 ?eqxx //; exact: eqP. 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 /= all1rel_cons //= eqxx. 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 97a5f22..8fb123e 100644 --- a/mathcomp/field/falgebra.v +++ b/mathcomp/field/falgebra.v @@ -1078,7 +1078,7 @@ Section Class_Def. Variables aT rT : FalgType K. Definition ahom_in (U : {vspace aT}) (f : 'Hom(aT, rT)) := - all1rel (fun x y : aT => f (x * y) == f x * f y) (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)) diff --git a/mathcomp/field/separable.v b/mathcomp/field/separable.v index 7e208cd..d07839c 100644 --- a/mathcomp/field/separable.v +++ b/mathcomp/field/separable.v @@ -289,7 +289,7 @@ Variables (K : {vspace L}) (D : 'End(L)). (* the deriviations used here are going to be linear, so we only define *) (* the Derivation predicate for linear endomorphisms. *) Definition Derivation : bool := - all1rel (fun u v => D (u * v) == D u * v + u * D v) (vbasis K). + all2rel (fun u v => D (u * v) == D u * v + u * D v) (vbasis K). Hypothesis derD : Derivation. diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index 9747f73..abca0d9 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -134,7 +134,7 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat. (* := [:: f x_1 y_1; ...; f x_1 y_m; f x_2 y_1; ...; f x_n y_m] *) (* 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 *) -(* all1rel r xs := allrel r xs xs *) +(* 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, *) @@ -3540,7 +3540,7 @@ 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 all1rel r xs := (allrel r xs xs). +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'} -> @@ -3551,9 +3551,9 @@ 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) xs ys : - r =2 r' -> allrel r xs ys = allrel r' xs ys. -Proof. by move=> rr'; apply/eq_in_allrel/all_predT/all_predT. 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. @@ -3571,26 +3571,26 @@ 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 All1Rel. +Section All2Rel. Variable (T : nonPropType) (r : rel T). Implicit Types (x y z : T) (xs : seq T). Hypothesis (rsym : symmetric r). -Lemma all1rel1 x : all1rel r [:: x] = r x x. +Lemma all2rel1 x : all2rel r [:: x] = r x x. Proof. by rewrite /allrel /= !andbT. Qed. -Lemma all1rel2 x y : all1rel r [:: x; y] = r x x && r y y && r x y. +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 all1rel_cons x xs : - all1rel r (x :: xs) = [&& r x x, all (r x) xs & all1rel r xs]. +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 All1Rel. +End All2Rel. Section Permutations. -- cgit v1.2.3