diff options
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 15 | ||||
| -rw-r--r-- | mathcomp/algebra/matrix.v | 10 | ||||
| -rw-r--r-- | mathcomp/field/falgebra.v | 2 | ||||
| -rw-r--r-- | mathcomp/field/separable.v | 2 | ||||
| -rw-r--r-- | 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. |