diff options
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 65 | ||||
| -rw-r--r-- | mathcomp/algebra/matrix.v | 313 | ||||
| -rw-r--r-- | mathcomp/algebra/mxalgebra.v | 20 | ||||
| -rw-r--r-- | mathcomp/algebra/mxpoly.v | 40 | ||||
| -rw-r--r-- | mathcomp/ssreflect/bigop.v | 22 | ||||
| -rw-r--r-- | mathcomp/ssreflect/eqtype.v | 14 | ||||
| -rw-r--r-- | mathcomp/ssreflect/order.v | 185 | ||||
| -rw-r--r-- | mathcomp/ssreflect/path.v | 5 | ||||
| -rw-r--r-- | mathcomp/ssreflect/seq.v | 59 | ||||
| -rw-r--r-- | mathcomp/ssreflect/ssrnat.v | 71 |
10 files changed, 729 insertions, 65 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 20809f3..95c0d63 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -10,7 +10,25 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). ### Added -- Added contrapostion lemmas involving propositions: `contra_not`, `contraPnot`, `contraTnot`, `contraNnot`, `contraPT`, `contra_notT`, `contra_notN`, `contraPN`, `contraFnot`, `contraPF` and `contra_notF` in ssrbool.v and `contraPeq`, `contra_not_eq`, `contraPneq`, and `contra_neq_not` in eqtype.v +- Added contraposition lemmas involving propositions: `contra_not`, `contraPnot`, `contraTnot`, `contraNnot`, `contraPT`, `contra_notT`, `contra_notN`, `contraPN`, `contraFnot`, `contraPF` and `contra_notF` in ssrbool.v and `contraPeq`, `contra_not_eq`, `contraPneq`, and `contra_neq_not` in eqtype.v +- Contraposition lemmas involving inequalities: + + in `order.v`: + `comparable_contraTle`, `comparable_contraTlt`, `comparable_contraNle`, `comparable_contraNlt`, `comparable_contraFle`, `comparable_contraFlt`, + `contra_leT`, `contra_ltT`, `contra_leN`, `contra_ltN`, `contra_leF`, `contra_ltF`, + `comparable_contra_leq_le`, `comparable_contra_leq_lt`, `comparable_contra_ltn_le`, `comparable_contra_ltn_lt`, + `contra_le_leq`, `contra_le_ltn`, `contra_lt_leq`, `contra_lt_ltn`, + `comparable_contra_le`, `comparable_contra_le_lt`, `comparable_contra_lt_le`, `comparable_contra_lt`, + `contraTle`, `contraTlt`, `contraNle`, `contraNlt`, `contraFle`, `contraFlt`, + `contra_leq_le`, `contra_leq_lt`, `contra_ltn_le`, `contra_ltn_lt`, + `contra_le`, `contra_le_lt`, `contra_lt_le`, `contra_lt`, + `contra_le_not`, `contra_lt_not`, + `comparable_contraPle`, `comparable_contraPlt`, `comparable_contra_not_le`, `comparable_contra_not_lt`, + `contraPle`, `contraPlt`, `contra_not_le`, `contra_not_lt` + + in `ssrnat.v`: + `contraTleq`, `contraTltn`, `contraNleq`, `contraNltn`, `contraFleq`, `contraFltn`, + `contra_leqT`, `contra_ltnT`, `contra_leqN`, `contra_ltnN`, `contra_leqF`, `contra_ltnF`, + `contra_leq`, `contra_ltn`, `contra_leq_ltn`, `contra_ltn_leq`, + `contraPleq`, `contraPltn`, `contra_not_leq`, `contra_not_ltn`, `contra_leq_not`, `contra_ltn_not` - in `ssralg.v`, new lemma `sumr_const_nat` and `iter_addr_0` - in `ssrnum.v`, new lemma `ler_sum_nat` @@ -83,6 +101,40 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). * `mxOver S` is a subring for square matrices if `S` is. - in `matrix.v` new lemmas about `map_mx`: `map_mx_id`, `map_mx_comp`, `eq_in_map_mx`, `eq_map_mx` and `map_mx_id_in`. +- in `matrix.v`, new lemmas `row_usubmx`, `row_dsubmx`, `col_lsubmx`, + and `col_rsubmx`. +- in `seq.v` new lemmas `find_ltn`, `has_take`, `has_take_leq`, + `index_ltn`, `in_take`, `in_take_leq`, `split_find_nth`, + `split_find` and `nth_rcons_cat_find`. + +- in `matrix.v` new lemma `mul_rVP`. + +- in `matrix.v`: + + new inductions lemmas: `row_ind`, `col_ind`, `mx_ind`, `sqmx_ind`, + `ringmx_ind`, `trigmx_ind`, `trigsqmx_ind`, `diagmx_ind`, + `diagsqmx_ind`. + + missing lemma `trmx_eq0` + + new lemmas about diagonal and triangular matrices: `mx11_is_diag`, + `mx11_is_trig`, `diag_mx_row`, `is_diag_mxEtrig`, `is_diag_trmx`, + `ursubmx_trig`, `dlsubmx_diag`, `ulsubmx_trig`, `drsubmx_trig`, + `ulsubmx_diag`, `drsubmx_diag`, `is_trig_block_mx`, + `is_diag_block_mx`, and `det_trig`. + +- in `mxpoly.v` new lemmas `horner_mx_diag`, `char_poly_trig`, + `root_mxminpoly`, and `mxminpoly_diag` +- in `mxalgebra.v`, new lemma `sub_sums_genmxP` (generalizes `sub_sumsmxP`). + +- in `bigop.v` new lemma `big_uncond`. The ideal name is `big_rmcond` + but it has just been deprecated from its previous meaning (see + Changed section) so as to reuse it in next mathcomp release. + +- in `bigop.v` new lemma `big_uncond_in` is a new alias of + `big_rmcond_in` for the sake of uniformity, but it is already + deprecated and will be removed two releases from now. + +- in `eqtype.v` new lemmas `contra_not_neq`, `contra_eq_not`. +- in `order.v`, new notations `0^d` and `1^d` for bottom and top elements of + dual lattices. ### Changed @@ -101,8 +153,19 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). - The `dual_*` notations such as `dual_le` in order.v are now qualified with the `Order` module. +- Lemma `big_rmcond` is deprecated and has been renamed + `big_rmcomd_in` (and aliased `big_uncond_in`, see Added). The + variant which does not require an `eqType` is currently named + `big_uncond` (cf Added) but it will be renamed `big_mkcond` in the + next release. + +- in `order.v`, `\join^d_` and `\meet^d_` notations are now properly specialized + for `dual_display`. + ### Renamed +- `big_rmcond` -> `big_rmcond_in` (cf Changed section) + ### Removed ### Infrastructure diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index 1730b0b..02097a4 100644 --- a/mathcomp/algebra/matrix.v +++ b/mathcomp/algebra/matrix.v @@ -82,6 +82,8 @@ From mathcomp Require Import div prime binomial ssralg finalg zmodp countalg. (* equal to 1%R when n is of the form n'.+1 (e.g., n >= 1). *) (* is_scalar_mx A <=> A is a scalar matrix (A = a%:M for some A). *) (* diag_mx d == the diagonal matrix whose main diagonal is d : 'rV_n. *) +(* is_diag_mx A <=> A is a diagonal matrix: forall i j, i != j -> A i j = 0 *) +(* is_trig_mx A <=> A is a triangular matrix: forall i j, i < j -> A i j = 0 *) (* delta_mx i j == the matrix with a 1 in row i, column j and 0 elsewhere. *) (* pid_mx r == the partial identity matrix with 1s only on the r first *) (* coefficients of the main diagonal; the dimensions of *) @@ -205,7 +207,7 @@ Variables m n : nat. (* We use dependent types (ordinals) for the indices so that ranges are *) (* mostly inferred automatically *) -Inductive matrix : predArgType := Matrix of {ffun 'I_m * 'I_n -> R}. +Variant matrix : predArgType := Matrix of {ffun 'I_m * 'I_n -> R}. Definition mx_val A := let: Matrix g := A in g. @@ -607,6 +609,18 @@ Proof. by split_mxE. Qed. Lemma col_mx_const a : col_mx (const_mx a) (const_mx a) = const_mx a. Proof. by split_mxE. Qed. +Lemma row_usubmx A i : row i (usubmx A) = row (lshift m2 i) A. +Proof. by apply/rowP=> j; rewrite !mxE; congr (A _ _); apply/val_inj. Qed. + +Lemma row_dsubmx A i : row i (dsubmx A) = row (rshift m1 i) A. +Proof. by apply/rowP=> j; rewrite !mxE; congr (A _ _); apply/val_inj. Qed. + +Lemma col_lsubmx A i : col i (lsubmx A) = col (lshift n2 i) A. +Proof. by apply/colP=> j; rewrite !mxE; congr (A _ _); apply/val_inj. Qed. + +Lemma col_rsubmx A i : col i (rsubmx A) = col (rshift n1 i) A. +Proof. by apply/colP=> j; rewrite !mxE; congr (A _ _); apply/val_inj. Qed. + End CutPaste. Lemma trmx_lsub m n1 n2 (A : 'M_(m, n1 + n2)) : (lsubmx A)^T = usubmx A^T. @@ -858,6 +872,58 @@ by rewrite castmx_comp etrans_id. Qed. Definition block_mxAx := block_mxA. (* Bypass Prenex Implicits *) +Section Induction. + +Lemma row_ind m (P : forall n, 'M[R]_(m, n) -> Type) : + (forall A, P 0%N A) -> + (forall n c A, P n A -> P (1 + n)%N (row_mx c A)) -> + forall n A, P n A. +Proof. +move=> P0 PS; elim=> [//|n IHn] A. +by rewrite -[n.+1]/(1 + n)%N in A *; rewrite -[A]hsubmxK; apply: PS. +Qed. + +Lemma col_ind n (P : forall m, 'M[R]_(m, n) -> Type) : + (forall A, P 0%N A) -> + (forall m r A, P m A -> P (1 + m)%N (col_mx r A)) -> + forall m A, P m A. +Proof. +move=> P0 PS; elim=> [//|m IHm] A. +by rewrite -[m.+1]/(1 + m)%N in A *; rewrite -[A]vsubmxK; apply: PS. +Qed. + +Lemma mx_ind (P : forall m n, 'M[R]_(m, n) -> Type) : + (forall m A, P m 0%N A) -> + (forall n A, P 0%N n A) -> + (forall m n x r c A, P m n A -> P (1 + m)%N (1 + n)%N (block_mx x r c A)) -> + forall m n A, P m n A. +Proof. +move=> P0l P0r PS; elim=> [|m IHm] [|n] A; do ?by [apply: P0l|apply: P0r]. +by rewrite -[A](@submxK 1 _ 1); apply: PS. +Qed. +Definition matrix_rect := mx_ind. +Definition matrix_rec := mx_ind. +Definition matrix_ind := mx_ind. + +Lemma sqmx_ind (P : forall n, 'M[R]_n -> Type) : + (forall A, P 0%N A) -> + (forall n x r c A, P n A -> P (1 + n)%N (block_mx x r c A)) -> + forall n A, P n A. +Proof. +by move=> P0 PS; elim=> [//|n IHn] A; rewrite -[A](@submxK 1 _ 1); apply: PS. +Qed. + +Lemma ringmx_ind (P : forall n, 'M[R]_n.+1 -> Type) : + (forall x, P 0%N x) -> + (forall n x (r : 'rV_n.+1) (c : 'cV_n.+1) A, + P n A -> P (1 + n)%N (block_mx x r c A)) -> + forall n A, P n A. +Proof. +by move=> P0 PS; elim=> [//|n IHn] A; rewrite -[A](@submxK 1 _ 1); apply: PS. +Qed. + +End Induction. + (* Bijections mxvec : 'M_(m, n) <----> 'rV_(m * n) : vec_mx *) Section VecMatrix. @@ -1213,6 +1279,9 @@ Lemma block_mx_eq0 m1 m2 n1 n2 (Aul : 'M_(m1, n1)) Aur Adl (Adr : 'M_(m2, n2)) : [&& Aul == 0, Aur == 0, Adl == 0 & Adr == 0]. Proof. by rewrite col_mx_eq0 !row_mx_eq0 !andbA. Qed. +Lemma trmx_eq0 m n (A : 'M_(m, n)) : (A^T == 0) = (A == 0). +Proof. by rewrite -trmx0 (inj_eq trmx_inj). Qed. + Lemma matrix_eq0 m n (A : 'M_(m, n)) : (A == 0) = [forall i, forall j, A i j == 0]. Proof. @@ -1247,8 +1316,177 @@ rewrite /nz_row; symmetry; case: pickP => [i /= nzAi | Ai0]. by rewrite eqxx; apply/eqP/row_matrixP=> i; move/eqP: (Ai0 i) ->; rewrite row0. Qed. +Definition is_diag_mx m n (A : 'M[V]_(m, n)) := + [forall i : 'I__, forall j : 'I__, (i != j :> nat) ==> (A i j == 0)]. + +Lemma is_diag_mxP m n (A : 'M[V]_(m, n)) : + reflect (forall i j : 'I__, i != j :> nat -> A i j = 0) (is_diag_mx A). +Proof. by apply: (iffP 'forall_'forall_implyP) => /(_ _ _ _)/eqP. Qed. + +Lemma mx0_is_diag m n : is_diag_mx (0 : 'M[V]_(m, n)). +Proof. by apply/is_diag_mxP => i j _; rewrite mxE. Qed. + +Lemma mx11_is_diag (M : 'M_1) : is_diag_mx M. +Proof. by apply/is_diag_mxP => i j; rewrite !ord1 eqxx. Qed. + +Definition is_trig_mx m n (A : 'M[V]_(m, n)) := + [forall i : 'I__, forall j : 'I__, (i < j)%N ==> (A i j == 0)]. + +Lemma is_trig_mxP m n (A : 'M[V]_(m, n)) : + reflect (forall i j : 'I__, (i < j)%N -> A i j = 0) (is_trig_mx A). +Proof. by apply: (iffP 'forall_'forall_implyP) => /(_ _ _ _)/eqP. Qed. + +Lemma is_diag_mx_is_trig m n (A : 'M[V]_(m, n)) : is_diag_mx A -> is_trig_mx A. +Proof. +by move=> /is_diag_mxP A_eq0; apply/is_trig_mxP=> i j lt_ij; rewrite A_eq0// ltn_eqF. +Qed. + +Lemma mx0_is_trig m n : is_trig_mx (0 : 'M[V]_(m, n)). +Proof. by apply/is_trig_mxP => i j _; rewrite mxE. Qed. + +Lemma mx11_is_trig (M : 'M_1) : is_trig_mx M. +Proof. by apply/is_trig_mxP => i j; rewrite !ord1 ltnn. Qed. + +Lemma is_diag_mxEtrig m n (A : 'M[V]_(m, n)) : + is_diag_mx A = is_trig_mx A && is_trig_mx A^T. +Proof. +apply/is_diag_mxP/andP => [Adiag|[/is_trig_mxP Atrig /is_trig_mxP ATtrig]]. + by split; apply/is_trig_mxP => i j lt_ij; rewrite ?mxE ?Adiag//; + [rewrite ltn_eqF|rewrite gtn_eqF]. +by move=> i j; case: ltngtP => // [/Atrig|/ATtrig]; rewrite ?mxE. +Qed. + +Lemma is_diag_trmx m n (A : 'M[V]_(m, n)) : is_diag_mx A^T = is_diag_mx A. +Proof. by rewrite !is_diag_mxEtrig trmxK andbC. Qed. + +Lemma ursubmx_trig m1 m2 n1 n2 (A : 'M[V]_(m1 + m2, n1 + n2)) : + m1 <= n1 -> is_trig_mx A -> ursubmx A = 0. +Proof. +move=> leq_m1_n1 /is_trig_mxP Atrig; apply/matrixP => i j. +by rewrite !mxE Atrig//= ltn_addr// (@leq_trans m1). +Qed. + +Lemma dlsubmx_diag m1 m2 n1 n2 (A : 'M[V]_(m1 + m2, n1 + n2)) : + n1 <= m1 -> is_diag_mx A -> dlsubmx A = 0. +Proof. +move=> leq_m2_n2 /is_diag_mxP Adiag; apply/matrixP => i j. +by rewrite !mxE Adiag// gtn_eqF//= ltn_addr// (@leq_trans n1). +Qed. + +Lemma ulsubmx_trig m1 m2 n1 n2 (A : 'M[V]_(m1 + m2, n1 + n2)) : + is_trig_mx A -> is_trig_mx (ulsubmx A). +Proof. +move=> /is_trig_mxP Atrig; apply/is_trig_mxP => i j lt_ij. +by rewrite !mxE Atrig. +Qed. + +Lemma drsubmx_trig m1 m2 n1 n2 (A : 'M[V]_(m1 + m2, n1 + n2)) : + m1 <= n1 -> is_trig_mx A -> is_trig_mx (drsubmx A). +Proof. +move=> leq_m1_n1 /is_trig_mxP Atrig; apply/is_trig_mxP => i j lt_ij. +by rewrite !mxE Atrig//= -addnS leq_add. +Qed. + +Lemma ulsubmx_diag m1 m2 n1 n2 (A : 'M[V]_(m1 + m2, n1 + n2)) : + is_diag_mx A -> is_diag_mx (ulsubmx A). +Proof. +rewrite !is_diag_mxEtrig trmx_ulsub. +by move=> /andP[/ulsubmx_trig-> /ulsubmx_trig->]. +Qed. + +Lemma drsubmx_diag m1 m2 n1 n2 (A : 'M[V]_(m1 + m2, n1 + n2)) : + m1 = n1 -> is_diag_mx A -> is_diag_mx (drsubmx A). +Proof. +move=> eq_m1_n1 /is_diag_mxP Adiag; apply/is_diag_mxP => i j neq_ij. +by rewrite !mxE Adiag//= eq_m1_n1 eqn_add2l. +Qed. + +Lemma is_trig_block_mx m1 m2 n1 n2 ul ur dl dr : m1 = n1 -> + @is_trig_mx (m1 + m2) (n1 + n2) (block_mx ul ur dl dr) = + [&& ur == 0, is_trig_mx ul & is_trig_mx dr]. +Proof. +move=> eq_m1_n1; rewrite {}eq_m1_n1 in ul ur dl dr *. +apply/is_trig_mxP/and3P => [Atrig|]; last first. + move=> [/eqP-> /is_trig_mxP ul_trig /is_trig_mxP dr_trig] i j; rewrite !mxE. + do 2![case: split_ordP => ? ->; rewrite ?mxE//=] => lt_ij; rewrite ?ul_trig//. + move: lt_ij; rewrite ltnNge -ltnS. + by rewrite (leq_trans (ltn_ord _))// -addnS leq_addr. + by rewrite dr_trig//; move: lt_ij; rewrite ltn_add2l. +split. +- apply/eqP/matrixP => i j; have := Atrig (lshift _ i) (rshift _ j). + rewrite !mxE; case: split_ordP => k /eqP; rewrite eq_shift// ?mxE. + case: split_ordP => l /eqP; rewrite eq_shift// ?mxE => /eqP-> /eqP<- <- //. + by rewrite /= (leq_trans (ltn_ord _)) ?leq_addr. +- apply/is_trig_mxP => i j lt_ij; have := Atrig (lshift _ i) (lshift _ j). + rewrite !mxE; case: split_ordP => k /eqP; rewrite eq_shift// ?mxE. + by case: split_ordP => l /eqP; rewrite eq_shift// ?mxE => /eqP<- /eqP<- ->. +- apply/is_trig_mxP => i j lt_ij; have := Atrig (rshift _ i) (rshift _ j). + rewrite !mxE; case: split_ordP => k /eqP; rewrite eq_shift// ?mxE. + case: split_ordP => l /eqP; rewrite eq_shift// ?mxE => /eqP<- /eqP<- -> //. + by rewrite /= ltn_add2l. +Qed. + +Lemma trigmx_ind (P : forall m n, 'M_(m, n) -> Type) : + (forall m, P m 0%N 0) -> + (forall n, P 0%N n 0) -> + (forall m n x c A, is_trig_mx A -> + P m n A -> P (1 + m)%N (1 + n)%N (block_mx x 0 c A)) -> + forall m n A, is_trig_mx A -> P m n A. +Proof. +move=> P0l P0r PS m n A; elim: A => {m n} [m|n|m n xx r c] A PA; + do ?by rewrite (flatmx0, thinmx0); by [apply: P0l|apply: P0r]. +by rewrite is_trig_block_mx => // /and3P[/eqP-> _ Atrig]; apply: PS (PA _). +Qed. + +Lemma trigsqmx_ind (P : forall n, 'M[V]_n -> Type) : (P 0%N 0) -> + (forall n x c A, is_trig_mx A -> P n A -> P (1 + n)%N (block_mx x 0 c A)) -> + forall n A, is_trig_mx A -> P n A. +Proof. +move=> P0 PS n A; elim/sqmx_ind: A => {n} [|n x r c] A PA. + by rewrite thinmx0; apply: P0. +by rewrite is_trig_block_mx => // /and3P[/eqP-> _ Atrig]; apply: PS (PA _). +Qed. + +Lemma is_diag_block_mx m1 m2 n1 n2 ul ur dl dr : m1 = n1 -> + @is_diag_mx (m1 + m2) (n1 + n2) (block_mx ul ur dl dr) = + [&& ur == 0, dl == 0, is_diag_mx ul & is_diag_mx dr]. +Proof. +move=> eq_m1_n1. +rewrite !is_diag_mxEtrig tr_block_mx !is_trig_block_mx// trmx_eq0. +by rewrite andbACA -!andbA; congr [&& _, _, _ & _]; rewrite andbCA. +Qed. + +Lemma diagmx_ind (P : forall m n, 'M_(m, n) -> Type) : + (forall m, P m 0%N 0) -> + (forall n, P 0%N n 0) -> + (forall m n x c A, is_diag_mx A -> + P m n A -> P (1 + m)%N (1 + n)%N (block_mx x 0 c A)) -> + forall m n A, is_diag_mx A -> P m n A. +Proof. +move=> P0l P0r PS m n A Adiag; have Atrig := is_diag_mx_is_trig Adiag. +elim/trigmx_ind: Atrig Adiag => // {m n} m n r c {A}A _ PA. +rewrite is_diag_block_mx => // /and4P[_ /eqP-> _ Adiag]. +exact: PS (PA _). +Qed. + +Lemma diagsqmx_ind (P : forall n, 'M[V]_n -> Type) : + (P 0%N 0) -> + (forall n x c A, is_diag_mx A -> P n A -> P (1 + n)%N (block_mx x 0 c A)) -> + forall n A, is_diag_mx A -> P n A. +Proof. +move=> P0 PS n A; elim/sqmx_ind: A => {n} [|n x r c] A PA. + by rewrite thinmx0; apply: P0. +rewrite is_diag_block_mx => // /and4P[/eqP-> /eqP-> _ Adiag]. +exact: PS (PA _). +Qed. + End MatrixZmodule. +Arguments is_diag_mx {V m n}. +Arguments is_diag_mxP {V m n A}. +Arguments is_trig_mx {V m n}. +Arguments is_trig_mxP {V m n A}. + Section FinZmodMatrix. Variables (V : finZmodType) (m n : nat). Local Notation MV := 'M[V]_(m, n). @@ -1458,46 +1696,28 @@ Lemma row_diag_mx n (d : 'rV_n) i : row i (diag_mx d) = d 0 i *: delta_mx 0 i. Proof. by apply/rowP => j; rewrite !mxE eqxx eq_sym mulr_natr. Qed. -Definition is_diag_mx m n (A : 'M[R]_(m, n)) := - [forall i : 'I__, forall j : 'I__, (i != j :> nat) ==> (A i j == 0)]. - -Lemma is_diag_mxP m n (A : 'M[R]_(m, n)) : - reflect (forall i j : 'I__, i != j :> nat -> A i j = 0) (is_diag_mx A). -Proof. by apply: (iffP 'forall_'forall_implyP) => /(_ _ _ _)/eqP. Qed. +Lemma diag_mx_row m n (l : 'rV_n) (r : 'rV_m) : + diag_mx (row_mx l r) = block_mx (diag_mx l) 0 0 (diag_mx r). +Proof. +apply/matrixP => i j. +by do ?[rewrite !mxE; case: split_ordP => ? ->]; rewrite mxE eq_shift. +Qed. Lemma diag_mxP n (A : 'M[R]_n) : reflect (exists d : 'rV_n, A = diag_mx d) (is_diag_mx A). Proof. -apply: (iffP (is_diag_mxP _)) => [Adiag|[d ->] i j neq_ij]; last first. +apply: (iffP is_diag_mxP) => [Adiag|[d ->] i j neq_ij]; last first. by rewrite !mxE -val_eqE (negPf neq_ij). exists (\row_i A i i); apply/matrixP => i j; rewrite !mxE. by case: (altP (i =P j)) => [->|/Adiag->]. Qed. Lemma diag_mx_is_diag n (r : 'rV[R]_n) : is_diag_mx (diag_mx r). -Proof. by apply/diag_mxP; eexists. Qed. - -Lemma mx0_is_diag m n : is_diag_mx (0 : 'M[R]_(m, n)). -Proof. by apply/is_diag_mxP => i j _; rewrite mxE. Qed. - -Definition is_trig_mx m n (A : 'M[R]_(m, n)) := - [forall i : 'I__, forall j : 'I__, (i < j)%N ==> (A i j == 0)]. - -Lemma is_trig_mxP m n (A : 'M[R]_(m, n)) : - reflect (forall i j : 'I__, (i < j)%N -> A i j = 0) (is_trig_mx A). -Proof. by apply: (iffP 'forall_'forall_implyP) => /(_ _ _ _)/eqP. Qed. - -Lemma is_diag_mx_is_trig m n (A : 'M[R]_(m, n)) : is_diag_mx A -> is_trig_mx A. -Proof. -by move=> /is_diag_mxP A_eq0; apply/is_trig_mxP=> i j lt_ij; rewrite A_eq0// ltn_eqF. -Qed. +Proof. by apply/diag_mxP; exists r. Qed. Lemma diag_mx_is_trig n (r : 'rV[R]_n) : is_trig_mx (diag_mx r). Proof. exact/is_diag_mx_is_trig/diag_mx_is_diag. Qed. -Lemma mx0_is_trig m n : is_trig_mx (0 : 'M[R]_(m, n)). -Proof. by apply/is_trig_mxP => i j _; rewrite mxE. Qed. - (* Scalar matrix : a diagonal matrix with a constant on the diagonal *) Section ScalarMx. @@ -1666,6 +1886,9 @@ apply/rowP=> j; rewrite !mxE (bigD1_ord i) //= mxE !eqxx mul1r. by rewrite big1 ?addr0 // => i'; rewrite mxE /= lift_eqF mul0r. Qed. +Lemma mul_rVP m n A B :((@mulmx 1 m n)^~ A =1 mulmx^~ B) <-> (A = B). +Proof. by split=> [eqAB|->//]; apply/row_matrixP => i; rewrite !rowE eqAB. Qed. + Lemma row_mul m n p (i : 'I_m) A (B : 'M_(n, p)) : row i (A *m B) = row i A *m B. Proof. by rewrite !rowE mulmxA. Qed. @@ -2154,13 +2377,15 @@ Prenex Implicits mulmx mxtrace determinant cofactor adjugate. Arguments is_scalar_mxP {R n A}. Arguments mul_delta_mx {R m n p}. -Arguments is_diag_mx {R m n}. -Arguments is_diag_mxP {R m n A}. -Arguments is_trig_mx {R m n}. -Arguments is_trig_mxP {R m n A}. -Hint Resolve scalar_mx_is_diag scalar_mx_is_trig : core. -Hint Resolve diag_mx_is_diag diag_mx_is_trig : core. +Hint Extern 0 (is_true (is_diag_mx (scalar_mx _))) => + apply: scalar_mx_is_diag : core. +Hint Extern 0 (is_true (is_trig_mx (scalar_mx _))) => + apply: scalar_mx_is_trig : core. +Hint Extern 0 (is_true (is_diag_mx (diag_mx _))) => + apply: diag_mx_is_diag : core. +Hint Extern 0 (is_true (is_trig_mx (diag_mx _))) => + apply: diag_mx_is_trig : core. Notation "a %:M" := (scalar_mx a) : ring_scope. Notation "A *m B" := (mulmx A B) : ring_scope. @@ -2469,17 +2694,6 @@ Qed. Lemma detM n' (A B : 'M[R]_n'.+1) : \det (A * B) = \det A * \det B. Proof. exact: det_mulmx. Qed. -Lemma det_diag n (d : 'rV[R]_n) : \det (diag_mx d) = \prod_i d 0 i. -Proof. -rewrite /(\det _) (bigD1 1%g) //= addrC big1 => [|p p1]. - by rewrite add0r odd_perm1 mul1r; apply: eq_bigr => i; rewrite perm1 mxE eqxx. -have{p1}: ~~ perm_on set0 p. - apply: contra p1; move/subsetP=> p1; apply/eqP/permP=> i. - by rewrite perm1; apply/eqP/idPn; move/p1; rewrite inE. -case/subsetPn=> i; rewrite !inE eq_sym; move/negPf=> p_i _. -by rewrite (bigD1 i) //= mulrCA mxE p_i mul0r. -Qed. - (* Laplace expansion lemma *) Lemma expand_cofactor n (A : 'M[R]_n) i j : cofactor A i j = @@ -2603,6 +2817,17 @@ Lemma det_lblock n1 n2 Aul (Adl : 'M[R]_(n2, n1)) Adr : \det (block_mx Aul 0 Adl Adr) = \det Aul * \det Adr. Proof. by rewrite -det_tr tr_block_mx trmx0 det_ublock !det_tr. Qed. +Lemma det_trig n (A : 'M[R]_n) : is_trig_mx A -> \det A = \prod_(i < n) A i i. +Proof. +elim/trigsqmx_ind => [|k x c B Bt IHB]; first by rewrite ?big_ord0 ?det_mx00. +rewrite det_lblock big_ord_recl [x]mx11_scalar det_scalar IHB//; congr (_ * _). + by rewrite -[ord0](lshift0 _ 0) block_mxEul mxE. +by apply: eq_bigr => i; rewrite -!rshift1 block_mxEdr. +Qed. + +Lemma det_diag n (d : 'rV[R]_n) : \det (diag_mx d) = \prod_i d 0 i. +Proof. by rewrite det_trig//; apply: eq_bigr => i; rewrite !mxE eqxx. Qed. + End ComMatrix. Arguments lin_mul_row {R m n} u. diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v index c0c4577..686da21 100644 --- a/mathcomp/algebra/mxalgebra.v +++ b/mathcomp/algebra/mxalgebra.v @@ -1122,22 +1122,30 @@ Lemma eqmx_sums P n (A B : I -> 'M[F]_n) : (\sum_(i | P i) A i :=: \sum_(i | P i) B i)%MS. Proof. by move=> eqAB; apply/eqmxP; rewrite !sumsmxS // => i; move/eqAB->. Qed. -Lemma sub_sumsmxP P m n (A : 'M_(m, n)) (B_ : I -> 'M_n) : - reflect (exists u_, A = \sum_(i | P i) u_ i *m B_ i) - (A <= \sum_(i | P i) B_ i)%MS. +Lemma sub_sums_genmxP P m n p (A : 'M_(m, p)) (B_ : I -> 'M_(n, p)) : + reflect (exists u_ : I -> 'M_(m, n), A = \sum_(i | P i) u_ i *m B_ i) + (A <= \sum_(i | P i) <<B_ i>>)%MS. Proof. apply: (iffP idP) => [| [u_ ->]]; last first. - by apply: summx_sub_sums => i _; apply: submxMl. + by apply: summx_sub_sums => i _; rewrite genmxE; apply: submxMl. have [b] := ubnP #|P|; elim: b => // b IHb in P A *. case: (pickP P) => [i Pi | P0 _]; last first. rewrite big_pred0 //; move/submx0null->. by exists (fun _ => 0); rewrite big_pred0. -rewrite (cardD1x Pi) (bigD1 i) //= => /IHb{b IHb} /= IHi /sub_addsmxP[u ->]. +rewrite (cardD1x Pi) (bigD1 i) //= => /IHb{b IHb} /= IHi. +rewrite (adds_eqmx (genmxE _) (eqmx_refl _)) => /sub_addsmxP[u ->]. have [u_ ->] := IHi _ (submxMl u.2 _). -exists [eta u_ with i |-> u.1]; rewrite (bigD1 i Pi) /= eqxx; congr (_ + _). +exists [eta u_ with i |-> u.1]; rewrite (bigD1 i Pi)/= eqxx; congr (_ + _). by apply: eq_bigr => j /andP[_ /negPf->]. Qed. +Lemma sub_sumsmxP P m n (A : 'M_(m, n)) (B_ : I -> 'M_n) : + reflect (exists u_, A = \sum_(i | P i) u_ i *m B_ i) + (A <= \sum_(i | P i) B_ i)%MS. +Proof. +by rewrite -(eqmx_sums (fun _ _ => genmxE _)); apply/sub_sums_genmxP. +Qed. + Lemma sumsmxMr_gen P m n A (B : 'M[F]_(m, n)) : ((\sum_(i | P i) A i)%MS *m B :=: \sum_(i | P i) <<A i *m B>>)%MS. Proof. diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v index f33e291..9d54f35 100644 --- a/mathcomp/algebra/mxpoly.v +++ b/mathcomp/algebra/mxpoly.v @@ -297,6 +297,18 @@ Qed. End HornerMx. +Lemma horner_mx_diag (R : comRingType) (n' : nat) + (d : 'rV[R]_n'.+1) (p : {poly R}) : + horner_mx (diag_mx d) p = diag_mx (map_mx (horner p) d). +Proof. +apply/matrixP => i j; rewrite !mxE. +elim/poly_ind: p => [|p c ihp]; first by rewrite rmorph0 horner0 mxE mul0rn. +rewrite !hornerE mulrnDl rmorphD rmorphM /= horner_mx_X horner_mx_C !mxE. +rewrite (bigD1 j)//= ihp mxE ?eqxx mulr1n -mulrnAl big1 ?addr0//. + by case: (altP (i =P j)) => [->|]; rewrite /= !(mulr1n, addr0, mul0r). +by move=> k /negPf nkF; rewrite mxE nkF mulr0. +Qed. + Prenex Implicits horner_mx powers_mx. Section CharPoly. @@ -434,6 +446,14 @@ rewrite (big_morph _ (fun p q => hornerM p q a) (hornerC 1 a)). by apply: eq_bigr => i _; rewrite !mxE !(hornerE, hornerMn). Qed. +Lemma char_poly_trig {R : comRingType} n (A : 'M[R]_n) : is_trig_mx A -> + char_poly A = \prod_(i < n) ('X - (A i i)%:P). +Proof. +move=> /is_trig_mxP Atrig; rewrite /char_poly det_trig. + by apply: eq_bigr => i; rewrite !mxE eqxx. +by apply/is_trig_mxP => i j lt_ij; rewrite !mxE -val_eqE ltn_eqF ?Atrig ?subrr. +Qed. + Definition companionmx {R : ringType} (p : seq R) (d := (size p).-1) := \matrix_(i < d, j < d) if (i == d.-1 :> nat) then - p`_j else (i.+1 == j :> nat)%:R. @@ -643,13 +663,31 @@ rewrite !hornerE rmorphD rmorphM /= horner_mx_X horner_mx_C scalerDl. by rewrite -scalerA mulmxDr mul_mx_scalar mulmxA -IHp -scalemxAl Av_av. Qed. +Lemma root_mxminpoly a : root p_A a = root (char_poly A) a. +Proof. by rewrite -eigenvalue_root_min eigenvalue_root_char. Qed. + End MinPoly. +Lemma mxminpoly_diag {F : fieldType} {n} (d : 'rV[F]_n.+1) + (u := undup [seq d 0 i | i <- enum 'I_n.+1]) : + mxminpoly (diag_mx d) = \prod_(r <- u) ('X - r%:P). +Proof. +apply/eqP; rewrite -eqp_monic ?mxminpoly_monic ?monic_prod_XsubC// /eqp. +rewrite mxminpoly_min/=; last first. + rewrite horner_mx_diag; apply/matrixP => i j; rewrite !mxE horner_prod. + case: (altP (i =P j)) => [->|neq_ij//]; rewrite mulr1n. + rewrite (bigD1_seq (d 0 j)) ?undup_uniq ?mem_undup ?map_f// /=. + by rewrite hornerD hornerN hornerX hornerC subrr mul0r. +apply: uniq_roots_dvdp; last by rewrite uniq_rootsE undup_uniq. +apply/allP => x; rewrite mem_undup root_mxminpoly char_poly_trig//. +rewrite -(big_map _ predT (fun x => _ - x%:P)) root_prod_XsubC. +by move=> /mapP[i _ ->]; apply/mapP; exists i; rewrite ?(mxE, eqxx). +Qed. Prenex Implicits degree_mxminpoly mxminpoly mx_inv_horner. Arguments mx_inv_hornerK {F n' A} [B] AnB. Arguments horner_rVpoly_inj {F n' A} [u1 u2] eq_u12A : rename. - + (* Parametricity. *) Section MapRingMatrix. diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v index 405ee08..6b26968 100644 --- a/mathcomp/ssreflect/bigop.v +++ b/mathcomp/ssreflect/bigop.v @@ -1212,12 +1212,20 @@ Lemma big_mkcondl I r (P Q : pred I) F : \big[*%M/1]_(i <- r | Q i) (if P i then F i else 1). Proof. by rewrite big_andbC big_mkcondr. Qed. -Lemma big_rmcond (I : eqType) (r : seq I) (P : pred I) F : +Lemma big_uncond I (r : seq I) (P : pred I) F : + (forall i, ~~ P i -> F i = 1) -> + \big[*%M/1]_(i <- r | P i) F i = \big[*%M/1]_(i <- r) F i. +Proof. +move=> F_eq1; rewrite big_mkcond; apply: eq_bigr => i. +by case: (P i) (F_eq1 i) => // ->. +Qed. + +Lemma big_rmcond_in (I : eqType) (r : seq I) (P : pred I) F : (forall i, i \in r -> ~~ P i -> F i = 1) -> \big[*%M/1]_(i <- r | P i) F i = \big[*%M/1]_(i <- r) F i. Proof. -move=> Fidx; rewrite big_mkcond big_seq_cond [in RHS]big_seq_cond ?big_mkcondr. -by apply: eq_bigr => i /Fidx {Fidx}; case: (P i) => // ->. +move=> F_eq1; rewrite big_seq_cond [RHS]big_seq_cond !big_mkcondl big_uncond//. +by move=> i /F_eq1; case: ifP => // _ ->. Qed. Lemma big_cat I r1 r2 (P : pred I) F : @@ -1971,3 +1979,11 @@ Arguments biggcdn_inf [I] i0 [P F m]. Notation filter_index_enum := ((fun _ => @deprecated_filter_index_enum _) (deprecate filter_index_enum big_enumP)) (only parsing). + +Notation big_rmcond := + ((fun _ _ _ _ => @big_rmcond_in _ _ _ _) + (deprecate big_rmcond big_rmcond_in)) (only parsing). + +Notation big_uncond_in := + ((fun _ _ _ _ => @big_rmcond_in _ _ _ _) + (deprecate big_uncond_in big_rmcond_in)) (only parsing). diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v index 1391b5b..1225ad9 100644 --- a/mathcomp/ssreflect/eqtype.v +++ b/mathcomp/ssreflect/eqtype.v @@ -220,10 +220,13 @@ Lemma contraFeq b x y : (x != y -> b) -> b = false -> x = y. Proof. by move=> imp /negbT; apply: contraNeq. Qed. Lemma contraPeq P x y : (x != y -> ~ P) -> P -> x = y. -Proof. by move => imp HP; apply: contraTeq isT => /imp /(_ HP). Qed. +Proof. by move=> imp HP; apply: contraTeq isT => /imp /(_ HP). Qed. Lemma contra_not_eq P x y : (x != y -> P) -> ~ P -> x = y. -Proof. by move => imp; apply: contraPeq => /imp HP /(_ HP). Qed. +Proof. by move=> imp; apply: contraPeq => /imp HP /(_ HP). Qed. + +Lemma contra_not_neq P x y : (x = y -> P) -> ~ P -> x != y. +Proof. by move=> imp; apply: contra_notN => /eqP. Qed. Lemma contraTneq b x y : (x = y -> ~~ b) -> b -> x != y. Proof. by move=> imp; apply: contraTN => /eqP. Qed. @@ -235,7 +238,7 @@ Lemma contraFneq b x y : (x = y -> b) -> b = false -> x != y. Proof. by move=> imp /negbT; apply: contraNneq. Qed. Lemma contraPneq P x y : (x = y -> ~ P) -> P -> x != y. -Proof. by move => imp; apply: contraPN => /eqP. Qed. +Proof. by move=> imp; apply: contraPN => /eqP. Qed. Lemma contra_eqN b x y : (b -> x != y) -> x = y -> ~~ b. Proof. by move=> imp /eqP; apply: contraL. Qed. @@ -255,8 +258,11 @@ Proof. by move=> imp; apply: contraNF => /imp->. Qed. Lemma contra_neqT b x y : (~~ b -> x = y) -> x != y -> b. Proof. by move=> imp; apply: contraNT => /imp->. Qed. +Lemma contra_eq_not P x y : (P -> x != y) -> x = y -> ~ P. +Proof. by move=> imp /eqP; apply: contraTnot. Qed. + Lemma contra_neq_not P x y : (P -> x = y) -> x != y -> ~ P. -Proof. by move => imp;apply: contraNnot => /imp->. Qed. +Proof. by move=> imp;apply: contraNnot => /imp->. Qed. Lemma contra_eq z1 z2 x1 x2 : (x1 != x2 -> z1 != z2) -> z1 = z2 -> x1 = x2. Proof. by move=> imp /eqP; apply: contraTeq. Qed. diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v index cd54fd3..da0e4d7 100644 --- a/mathcomp/ssreflect/order.v +++ b/mathcomp/ssreflect/order.v @@ -468,6 +468,9 @@ Reserved Notation "A `|^d` B" (at level 52, left associativity). Reserved Notation "A `\^d` B" (at level 50, left associativity). Reserved Notation "~^d` A" (at level 35, right associativity). +Reserved Notation "0^d" (at level 0). +Reserved Notation "1^d" (at level 0). + (* Reserved notations for product ordering of prod or seq *) Reserved Notation "x <=^p y" (at level 70, y at next level). Reserved Notation "x >=^p y" (at level 70, y at next level). @@ -2551,6 +2554,16 @@ Notation "x ><^d y" := (~~ (><^d%O x y)) : order_scope. Notation "x `&^d` y" := (dual_meet x y) : order_scope. Notation "x `|^d` y" := (dual_join x y) : order_scope. +Notation "0^d" := dual_bottom : order_scope. +Notation "1^d" := dual_top : order_scope. + +(* The following Local Notations are here to define the \join^d_ and \meet^d_ *) +(* notations later. Do not remove them. *) +Local Notation "0" := dual_bottom. +Local Notation "1" := dual_top. +Local Notation join := dual_join. +Local Notation meet := dual_meet. + Notation "\join^d_ ( i <- r | P ) F" := (\big[join/0]_(i <- r | P%B) F%O) : order_scope. Notation "\join^d_ ( i <- r ) F" := @@ -3130,6 +3143,111 @@ Lemma nmono_leif (f : T -> T) C : Proof. by move=> mf x y; rewrite /leif !eq_le !mf. Qed. End POrderTheory. + +Section ContraTheory. +Context {disp1 disp2 : unit} {T1 : porderType disp1} {T2 : porderType disp2}. +Implicit Types (x y : T1) (z t : T2) (b : bool) (m n : nat) (P : Prop). + +Lemma comparable_contraTle b x y : x >=< y -> (y < x -> ~~ b) -> (b -> x <= y). +Proof. by case: comparableP; case: b. Qed. + +Lemma comparable_contraTlt b x y : x >=< y -> (y <= x -> ~~ b) -> (b -> x < y). +Proof. by case: comparableP; case: b. Qed. + +Lemma comparable_contraPle P x y : x >=< y -> (y < x -> ~ P) -> (P -> x <= y). +Proof. by case: comparableP => // _ _ /(_ isT). Qed. + +Lemma comparable_contraPlt P x y : x >=< y -> (y <= x -> ~ P) -> (P -> x < y). +Proof. by case: comparableP => // _ _ /(_ isT). Qed. + +Lemma comparable_contraNle b x y : x >=< y -> (y < x -> b) -> (~~ b -> x <= y). +Proof. by case: comparableP; case: b. Qed. + +Lemma comparable_contraNlt b x y : x >=< y -> (y <= x -> b) -> (~~ b -> x < y). +Proof. by case: comparableP; case: b. Qed. + +Lemma comparable_contra_not_le P x y : x >=< y -> (y < x -> P) -> (~ P -> x <= y). +Proof. by case: comparableP => // _ _ /(_ isT). Qed. + +Lemma comparable_contra_not_lt P x y : x >=< y -> (y <= x -> P) -> (~ P -> x < y). +Proof. by case: comparableP => // _ _ /(_ isT). Qed. + +Lemma comparable_contraFle b x y : x >=< y -> (y < x -> b) -> (b = false -> x <= y). +Proof. by case: comparableP; case: b => // _ _ /implyP. Qed. + +Lemma comparable_contraFlt b x y : x >=< y -> (y <= x -> b) -> (b = false -> x < y). +Proof. by case: comparableP; case: b => // _ _ /implyP. Qed. + +Lemma contra_leT b x y : (~~ b -> x < y) -> (y <= x -> b). +Proof. by case: comparableP; case: b. Qed. + +Lemma contra_ltT b x y : (~~ b -> x <= y) -> (y < x -> b). +Proof. by case: comparableP; case: b. Qed. + +Lemma contra_leN b x y : (b -> x < y) -> (y <= x -> ~~ b). +Proof. by case: comparableP; case: b. Qed. + +Lemma contra_ltN b x y : (b -> x <= y) -> (y < x -> ~~ b). +Proof. by case: comparableP; case: b. Qed. + +Lemma contra_le_not P x y : (P -> x < y) -> (y <= x -> ~ P). +Proof. by case: comparableP => // _ PF _ /PF. Qed. + +Lemma contra_lt_not P x y : (P -> x <= y) -> (y < x -> ~ P). +Proof. by case: comparableP => // _ PF _ /PF. Qed. + +Lemma contra_leF b x y : (b -> x < y) -> (y <= x -> b = false). +Proof. by case: comparableP; case: b => // _ /implyP. Qed. + +Lemma contra_ltF b x y : (b -> x <= y) -> (y < x -> b = false). +Proof. by case: comparableP; case: b => // _ /implyP. Qed. + +Lemma comparable_contra_leq_le m n x y : x >=< y -> + (y < x -> (n < m)%N) -> ((m <= n)%N -> x <= y). +Proof. by case: comparableP; case: ltngtP. Qed. + +Lemma comparable_contra_leq_lt m n x y : x >=< y -> + (y <= x -> (n < m)%N) -> ((m <= n)%N -> x < y). +Proof. by case: comparableP; case: ltngtP. Qed. + +Lemma comparable_contra_ltn_le m n x y : x >=< y -> + (y < x -> (n <= m)%N) -> ((m < n)%N -> x <= y). +Proof. by case: comparableP; case: ltngtP. Qed. + +Lemma comparable_contra_ltn_lt m n x y : x >=< y -> + (y <= x -> (n <= m)%N) -> ((m < n)%N -> x < y). +Proof. by case: comparableP; case: ltngtP. Qed. + +Lemma contra_le_leq x y m n : ((n < m)%N -> y < x) -> (x <= y -> (m <= n)%N). +Proof. by case: comparableP; case: ltngtP. Qed. + +Lemma contra_le_ltn x y m n : ((n <= m)%N -> y < x) -> (x <= y -> (m < n)%N). +Proof. by case: comparableP; case: ltngtP. Qed. + +Lemma contra_lt_leq x y m n : ((n < m)%N -> y <= x) -> (x < y -> (m <= n)%N). +Proof. by case: comparableP; case: ltngtP. Qed. + +Lemma contra_lt_ltn x y m n : ((n <= m)%N -> y <= x) -> (x < y -> (m < n)%N). +Proof. by case: comparableP; case: ltngtP. Qed. + +Lemma comparable_contra_le x y z t : z >=< t -> + (t < z -> y < x) -> (x <= y -> z <= t). +Proof. by do 2![case: comparableP => //= ?]. Qed. + +Lemma comparable_contra_le_lt x y z t : z >=< t -> + (t <= z -> y < x) -> (x <= y -> z < t). +Proof. by do 2![case: comparableP => //= ?]. Qed. + +Lemma comparable_contra_lt_le x y z t : z >=< t -> + (t < z -> y <= x) -> (x < y -> z <= t). +Proof. by do 2![case: comparableP => //= ?]. Qed. + +Lemma comparable_contra_lt x y z t : z >=< t -> + (t <= z -> y <= x) -> (x < y -> z < t). +Proof. by do 2![case: comparableP => //= ?]. Qed. + +End ContraTheory. + Section POrderMonotonyTheory. Context {disp disp' : unit}. @@ -3695,9 +3813,76 @@ End ArgExtremum. End TotalTheory. +Hint Resolve le_total : core. +Hint Resolve ge_total : core. +Hint Resolve comparableT : core. +Hint Resolve sort_le_sorted : core. + Arguments min_idPr {disp T x y}. Arguments max_idPl {disp T x y}. +(* contra lemmas *) + +Section ContraTheory. +Context {disp1 disp2 : unit} {T1 : porderType disp1} {T2 : orderType disp2}. +Implicit Types (x y : T1) (z t : T2) (b : bool) (m n : nat) (P : Prop). + +Lemma contraTle b z t : (t < z -> ~~ b) -> (b -> z <= t). +Proof. exact: comparable_contraTle. Qed. + +Lemma contraTlt b z t : (t <= z -> ~~ b) -> (b -> z < t). +Proof. exact: comparable_contraTlt. Qed. + +Lemma contraPle P z t : (t < z -> ~ P) -> (P -> z <= t). +Proof. exact: comparable_contraPle. Qed. + +Lemma contraPlt P z t : (t <= z -> ~ P) -> (P -> z < t). +Proof. exact: comparable_contraPlt. Qed. + +Lemma contraNle b z t : (t < z -> b) -> (~~ b -> z <= t). +Proof. exact: comparable_contraNle. Qed. + +Lemma contraNlt b z t : (t <= z -> b) -> (~~ b -> z < t). +Proof. exact: comparable_contraNlt. Qed. + +Lemma contra_not_le P z t : (t < z -> P) -> (~ P -> z <= t). +Proof. exact: comparable_contra_not_le. Qed. + +Lemma contra_not_lt P z t : (t <= z -> P) -> (~ P -> z < t). +Proof. exact: comparable_contra_not_lt. Qed. + +Lemma contraFle b z t : (t < z -> b) -> (b = false -> z <= t). +Proof. exact: comparable_contraFle. Qed. + +Lemma contraFlt b z t : (t <= z -> b) -> (b = false -> z < t). +Proof. exact: comparable_contraFlt. Qed. + +Lemma contra_leq_le m n z t : (t < z -> (n < m)%N) -> ((m <= n)%N -> z <= t). +Proof. exact: comparable_contra_leq_le. Qed. + +Lemma contra_leq_lt m n z t : (t <= z -> (n < m)%N) -> ((m <= n)%N -> z < t). +Proof. exact: comparable_contra_leq_lt. Qed. + +Lemma contra_ltn_le m n z t : (t < z -> (n <= m)%N) -> ((m < n)%N -> z <= t). +Proof. exact: comparable_contra_ltn_le. Qed. + +Lemma contra_ltn_lt m n z t : (t <= z -> (n <= m)%N) -> ((m < n)%N -> z < t). +Proof. exact: comparable_contra_ltn_lt. Qed. + +Lemma contra_le x y z t : (t < z -> y < x) -> (x <= y -> z <= t). +Proof. exact: comparable_contra_le. Qed. + +Lemma contra_le_lt x y z t : (t <= z -> y < x) -> (x <= y -> z < t). +Proof. exact: comparable_contra_le_lt. Qed. + +Lemma contra_lt_le x y z t : (t < z -> y <= x) -> (x < y -> z <= t). +Proof. exact: comparable_contra_lt_le. Qed. + +Lemma contra_lt x y z t : (t <= z -> y <= x) -> (x < y -> z < t). +Proof. exact: comparable_contra_lt. Qed. + +End ContraTheory. + Section TotalMonotonyTheory. Context {disp : unit} {disp' : unit}. diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v index 6e72af0..7d1f0e9 100644 --- a/mathcomp/ssreflect/path.v +++ b/mathcomp/ssreflect/path.v @@ -193,10 +193,7 @@ Variant split x : seq T -> seq T -> seq T -> Type := Lemma splitP p x (i := index x p) : x \in p -> split x p (take i p) (drop i.+1 p). -Proof. -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. +Proof. by rewrite -has_pred1 => /split_find[? ? ? /eqP->]; constructor. Qed. Variant splitl x1 x : seq T -> Type := Splitl p1 p2 of last x1 p1 = x : splitl x1 x (p1 ++ p2). diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index 059d04c..ac9a225 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -755,6 +755,16 @@ case: ltnP => [?|le_s_n0]; rewrite ?(leq_trans le_s_n0) ?leq_addr ?addKn //=. by rewrite drop_oversize // !nth_default. Qed. +Lemma find_ltn p s i : has p (take i s) -> find p s < i. +Proof. by elim: s i => [|y s ihs] [|i]//=; case: (p _) => //= /ihs. Qed. + +Lemma has_take p s i : has p s -> has p (take i s) = (find p s < i). +Proof. by elim: s i => [|y s ihs] [|i]//=; case: (p _) => //= /ihs ->. Qed. + +Lemma has_take_leq (p : pred T) (s : seq T) i : i <= size s -> + has p (take i s) = (find p s < i). +Proof. by elim: s i => [|y s ihs] [|i]//=; case: (p _) => //= /ihs ->. Qed. + Lemma nth_take i : i < n0 -> forall s, nth (take n0 s) i = nth s i. Proof. move=> lt_i_n0 s; case lt_n0_s: (n0 < size s). @@ -1331,6 +1341,15 @@ Lemma index_cat x s1 s2 : index x (s1 ++ s2) = if x \in s1 then index x s1 else size s1 + index x s2. Proof. by rewrite /index find_cat has_pred1. Qed. +Lemma index_ltn x s i : x \in take i s -> index x s < i. +Proof. by rewrite -has_pred1; apply: find_ltn. Qed. + +Lemma in_take x s i : x \in s -> (x \in take i s) = (index x s < i). +Proof. by rewrite -?has_pred1; apply: has_take. Qed. + +Lemma in_take_leq x s i : i <= size s -> (x \in take i s) = (index x s < i). +Proof. by rewrite -?has_pred1; apply: has_take_leq. Qed. + Lemma nthK s: uniq s -> {in gtn (size s), cancel (nth s) (index^~ s)}. Proof. elim: s => //= x s IHs /andP[s'x Us] i; rewrite inE ltnS eq_sym -if_neg. @@ -1454,6 +1473,42 @@ Definition bitseq := seq bool. Canonical bitseq_eqType := Eval hnf in [eqType of bitseq]. Canonical bitseq_predType := Eval hnf in [predType of bitseq]. +(* Generalized versions of splitP (from path.v): split_find_nth and split_find *) +Section FindNth. +Variables (T : Type). +Implicit Types (x : T) (p : pred T) (s : seq T). + +Variant split_find_nth_spec p : seq T -> seq T -> seq T -> T -> Type := + FindNth x s1 s2 of p x & ~~ has p s1 : + split_find_nth_spec p (rcons s1 x ++ s2) s1 s2 x. + +Lemma split_find_nth x0 p s (i := find p s) : + has p s -> split_find_nth_spec p s (take i s) (drop i.+1 s) (nth x0 s i). +Proof. +move=> p_s; rewrite -[X in split_find_nth_spec _ X](cat_take_drop i s). +rewrite (drop_nth x0 _) -?has_find// -cat_rcons. +by constructor; [apply: nth_find | rewrite has_take -?leqNgt]. +Qed. + +Variant split_find_spec p : seq T -> seq T -> seq T -> Type := + FindSplit x s1 s2 of p x & ~~ has p s1 : + split_find_spec p (rcons s1 x ++ s2) s1 s2. + +Lemma split_find p s (i := find p s) : + has p s -> split_find_spec p s (take i s) (drop i.+1 s). +Proof. +by case: s => // x ? in i * => ?; case: split_find_nth => //; constructor. +Qed. + +Lemma nth_rcons_cat_find x0 p s1 s2 x (s := rcons s1 x ++ s2) : + p x -> ~~ has p s1 -> nth x0 s (find p s) = x. +Proof. +move=> pz pNs1; rewrite /s cat_rcons find_cat (negPf pNs1). +by rewrite nth_cat/= pz addn0 subnn ltnn. +Qed. + +End FindNth. + (* Incrementing the ith nat in a seq nat, padding with 0's if needed. This *) (* allows us to use nat seqs as bags of nats. *) @@ -1500,7 +1555,7 @@ Definition perm_eq s1 s2 := Lemma permP s1 s2 : reflect (count^~ s1 =1 count^~ s2) (perm_eq s1 s2). Proof. apply: (iffP allP) => /= [eq_cnt1 a | eq_cnt x _]; last exact/eqP. -have [n le_an] := ubnP (count a (s1 ++ s2)); elim: n => // n IHn in a le_an *. +have [n le_an] := ubnP (count a (s1 ++ s2)); elim: n => // n IHn in a le_an *. have [/eqP|] := posnP (count a (s1 ++ s2)). by rewrite count_cat addn_eq0; do 2!case: eqP => // ->. rewrite -has_count => /hasP[x s12x a_x]; pose a' := predD1 a x. @@ -2984,7 +3039,7 @@ Lemma allpairs_mapr f (g : forall x, T' x -> T x) s t : [seq f x y | x <- s, y <- map (g x) (t x)] = [seq f x (g x y) | x <- s, y <- t x]. Proof. by rewrite -(eq_map (fun=> map_comp _ _ _)). Qed. - + End AllPairsDep. Arguments allpairs_dep {S T R} f s t /. diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v index 8b4d39f..7a996d1 100644 --- a/mathcomp/ssreflect/ssrnat.v +++ b/mathcomp/ssreflect/ssrnat.v @@ -1513,6 +1513,77 @@ rewrite -[4]/(2 * 2) -mulnA mul2n -addnn sqrnD; apply/leqifP. by rewrite ltn_add2r eqn_add2r ltn_neqAle !nat_Cauchy; case: eqVneq. Qed. +Section ContraLeq. +Implicit Types (b : bool) (m n : nat) (P : Prop). + +Lemma contraTleq b m n : (n < m -> ~~ b) -> (b -> m <= n). +Proof. by rewrite ltnNge; apply: contraTT. Qed. + +Lemma contraTltn b m n : (n <= m -> ~~ b) -> (b -> m < n). +Proof. by rewrite ltnNge; apply: contraTN. Qed. + +Lemma contraPleq P m n : (n < m -> ~ P) -> (P -> m <= n). +Proof. by rewrite ltnNge; apply: contraPT. Qed. + +Lemma contraPltn P m n : (n <= m -> ~ P) -> (P -> m < n). +Proof. by rewrite ltnNge; apply: contraPN. Qed. + +Lemma contraNleq b m n : (n < m -> b) -> (~~ b -> m <= n). +Proof. by rewrite ltnNge; apply: contraNT. Qed. + +Lemma contraNltn b m n : (n <= m -> b) -> (~~ b -> m < n). +Proof. by rewrite ltnNge; apply: contraNN. Qed. + +Lemma contra_not_leq P m n : (n < m -> P) -> (~ P -> m <= n). +Proof. by rewrite ltnNge; apply: contra_notT. Qed. + +Lemma contra_not_ltn P m n : (n <= m -> P) -> (~ P -> m < n). +Proof. by rewrite ltnNge; apply: contra_notN. Qed. + +Lemma contraFleq b m n : (n < m -> b) -> (b = false -> m <= n). +Proof. by rewrite ltnNge; apply: contraFT. Qed. + +Lemma contraFltn b m n : (n <= m -> b) -> (b = false -> m < n). +Proof. by rewrite ltnNge; apply: contraFN. Qed. + +Lemma contra_leqT b m n : (~~ b -> m < n) -> (n <= m -> b). +Proof. by rewrite ltnNge; apply: contraTT. Qed. + +Lemma contra_ltnT b m n : (~~ b -> m <= n) -> (n < m -> b). +Proof. by rewrite ltnNge; apply: contraNT. Qed. + +Lemma contra_leqN b m n : (b -> m < n) -> (n <= m -> ~~ b). +Proof. by rewrite ltnNge; apply: contraTN. Qed. + +Lemma contra_ltnN b m n : (b -> m <= n) -> (n < m -> ~~ b). +Proof. by rewrite ltnNge; apply: contraNN. Qed. + +Lemma contra_leq_not P m n : (P -> m < n) -> (n <= m -> ~ P). +Proof. by rewrite ltnNge; apply: contraTnot. Qed. + +Lemma contra_ltn_not P m n : (P -> m <= n) -> (n < m -> ~ P). +Proof. by rewrite ltnNge; apply: contraNnot. Qed. + +Lemma contra_leqF b m n : (b -> m < n) -> (n <= m -> b = false). +Proof. by rewrite ltnNge; apply: contraTF. Qed. + +Lemma contra_ltnF b m n : (b -> m <= n) -> (n < m -> b = false). +Proof. by rewrite ltnNge; apply: contraNF. Qed. + +Lemma contra_leq m n p q : (q < p -> n < m) -> (m <= n -> p <= q). +Proof. by rewrite !ltnNge; apply: contraTT. Qed. + +Lemma contra_leq_ltn m n p q : (q <= p -> n < m) -> (m <= n -> p < q). +Proof. by rewrite !ltnNge; apply: contraTN. Qed. + +Lemma contra_ltn_leq m n p q : (q < p -> n <= m) -> (m < n -> p <= q). +Proof. by rewrite !ltnNge; apply: contraNT. Qed. + +Lemma contra_ltn m n p q : (q <= p -> n <= m) -> (m < n -> p < q). +Proof. by rewrite !ltnNge; apply: contraNN. Qed. + +End ContraLeq. + Section Monotonicity. Variable T : Type. |