diff options
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/algebra/matrix.v | 32 | ||||
| -rw-r--r-- | mathcomp/character/mxrepresentation.v | 4 | ||||
| -rw-r--r-- | mathcomp/ssreflect/bigop.v | 23 | ||||
| -rw-r--r-- | mathcomp/ssreflect/seq.v | 20 |
4 files changed, 37 insertions, 42 deletions
diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index 77d2e4f..b67bdba 100644 --- a/mathcomp/algebra/matrix.v +++ b/mathcomp/algebra/matrix.v @@ -1935,7 +1935,7 @@ Proof. by rewrite scale_scalar_mx mulr1. Qed. Lemma scalar_mx_sum_delta a : a%:M = \sum_i a *: delta_mx i i. Proof. -by rewrite -diag_const_mx diag_mx_sum_delta; apply: eq_bigr => i _; rewrite mxE. +by rewrite -diag_const_mx diag_mx_sum_delta; under eq_bigr do rewrite mxE. Qed. Lemma mx1_sum_delta : 1%:M = \sum_i delta_mx i i. @@ -1996,11 +1996,9 @@ Local Notation "A *m B" := (mulmx A B) : ring_scope. Lemma mulmxA m n p q (A : 'M_(m, n)) (B : 'M_(n, p)) (C : 'M_(p, q)) : A *m (B *m C) = A *m B *m C. Proof. -apply/matrixP=> i l; rewrite !mxE. -transitivity (\sum_j (\sum_k (A i j * (B j k * C k l)))). - by apply: eq_bigr => j _; rewrite mxE big_distrr. +apply/matrixP=> i l; rewrite !mxE; under eq_bigr do rewrite mxE big_distrr/=. rewrite exchange_big; apply: eq_bigr => j _; rewrite mxE big_distrl /=. -by apply: eq_bigr => k _; rewrite mulrA. +by under eq_bigr do rewrite mulrA. Qed. Lemma mul0mx m n p (A : 'M_(n, p)) : 0 *m A = 0 :> 'M_(m, p). @@ -2016,13 +2014,13 @@ Qed. Lemma mulmxN m n p (A : 'M_(m, n)) (B : 'M_(n, p)) : A *m (- B) = - (A *m B). Proof. apply/matrixP=> i k; rewrite !mxE -sumrN. -by apply: eq_bigr => j _; rewrite mxE mulrN. +by under eq_bigr do rewrite mxE mulrN. Qed. Lemma mulNmx m n p (A : 'M_(m, n)) (B : 'M_(n, p)) : - A *m B = - (A *m B). Proof. apply/matrixP=> i k; rewrite !mxE -sumrN. -by apply: eq_bigr => j _; rewrite mxE mulNr. +by under eq_bigr do rewrite mxE mulNr. Qed. Lemma mulmxDl m n p (A1 A2 : 'M_(m, n)) (B : 'M_(n, p)) : @@ -2083,12 +2081,12 @@ Proof. by rewrite !rowE mulmxA. Qed. Lemma mulmx_sum_row m n (u : 'rV_m) (A : 'M_(m, n)) : u *m A = \sum_i u 0 i *: row i A. Proof. -by apply/rowP=> j; rewrite mxE summxE; apply: eq_bigr => i _; rewrite !mxE. +by apply/rowP=> j; rewrite mxE summxE; under [RHS]eq_bigr do rewrite !mxE. Qed. Lemma mxsub_mul m n m' n' p f g (A : 'M_(m, p)) (B : 'M_(p, n)) : mxsub f g (A *m B) = rowsub f A *m colsub g B :> 'M_(m', n'). -Proof. by split_mxE; apply: eq_bigr => k _; rewrite !mxE. Qed. +Proof. by split_mxE; under [RHS]eq_bigr do rewrite !mxE. Qed. Lemma mul_rowsub_mx m n m' p f (A : 'M_(m, p)) (B : 'M_(p, n)) : rowsub f A *m B = rowsub f (A *m B) :> 'M_(m', n). @@ -2330,14 +2328,14 @@ Lemma mul_mx_row m n p1 p2 (A : 'M_(m, n)) (Bl : 'M_(n, p1)) (Br : 'M_(n, p2)) : A *m row_mx Bl Br = row_mx (A *m Bl) (A *m Br). Proof. apply/matrixP=> i k; rewrite !mxE. -by case defk: (split k); rewrite mxE; apply: eq_bigr => j _; rewrite mxE defk. +by case defk: (split k); rewrite mxE; under eq_bigr do rewrite mxE defk. Qed. Lemma mul_col_mx m1 m2 n p (Au : 'M_(m1, n)) (Ad : 'M_(m2, n)) (B : 'M_(n, p)) : col_mx Au Ad *m B = col_mx (Au *m B) (Ad *m B). Proof. apply/matrixP=> i k; rewrite !mxE. -by case defi: (split i); rewrite mxE; apply: eq_bigr => j _; rewrite mxE defi. +by case defi: (split i); rewrite mxE; under eq_bigr do rewrite mxE defi. Qed. Lemma mul_row_col m n1 n2 p (Al : 'M_(m, n1)) (Ar : 'M_(m, n2)) @@ -2465,8 +2463,8 @@ Proof. by apply: eq_bigr=> i _; rewrite mxE. Qed. Lemma mxtrace_is_scalar : scalar mxtrace. Proof. -move=> a A B; rewrite mulr_sumr -big_split /=; apply: eq_bigr=> i _. -by rewrite !mxE. +move=> a A B; rewrite mulr_sumr -big_split /=. +by apply: eq_bigr=> i _; rewrite !mxE. Qed. Canonical mxtrace_additive := Additive mxtrace_is_scalar. Canonical mxtrace_linear := Linear mxtrace_is_scalar. @@ -2480,8 +2478,8 @@ Proof. by apply: eq_bigr => j _; rewrite mxE eqxx. Qed. Lemma mxtrace_scalar a : \tr a%:M = a *+ n. Proof. -rewrite -diag_const_mx mxtrace_diag. -by rewrite (eq_bigr _ (fun j _ => mxE _ _ 0 j)) sumr_const card_ord. +rewrite -diag_const_mx mxtrace_diag; under eq_bigr do rewrite mxE. +by rewrite sumr_const card_ord. Qed. Lemma mxtrace1 : \tr 1%:M = n%:R. Proof. exact: mxtrace_scalar. Qed. @@ -2496,7 +2494,7 @@ Lemma mxtrace_block n1 n2 (Aul : 'M_n1) Aur Adl (Adr : 'M_n2) : \tr (block_mx Aul Aur Adl Adr) = \tr Aul + \tr Adr. Proof. rewrite /(\tr _) big_split_ord /=. -by congr (_ + _); apply: eq_bigr => i _; rewrite (block_mxEul, block_mxEdr). +by congr (_ + _); under eq_bigr do rewrite (block_mxEul, block_mxEdr). Qed. (* The matrix ring structure requires a strutural condition (dimension of the *) @@ -3057,7 +3055,7 @@ Lemma expand_det_col n (A : 'M[R]_n) j0 : \det A = \sum_i (A i j0 * cofactor A i j0). Proof. rewrite -det_tr (expand_det_row _ j0). -by apply: eq_bigr => i _; rewrite cofactor_tr mxE. +by under eq_bigr do rewrite cofactor_tr mxE. Qed. Lemma trmx_adj n (A : 'M[R]_n) : (\adj A)^T = \adj A^T. diff --git a/mathcomp/character/mxrepresentation.v b/mathcomp/character/mxrepresentation.v index e94e69f..4202c6e 100644 --- a/mathcomp/character/mxrepresentation.v +++ b/mathcomp/character/mxrepresentation.v @@ -5684,9 +5684,9 @@ elim: t => //=. - by move=> k _; apply/rowP=> i; rewrite !mxE /= nth_row_env nth_map_rVval. - by move=> x _; rewrite eval_mx_term. - by move=> x _; rewrite eval_mx_term. -- move=> t1 IH1 t2 IH2 /andP[rt1 rt2]; rewrite -{}IH1 // -{}IH2 //. +- move=> t1 + t2 + /andP[rt1 rt2] => <-// <-//. by apply/rowP=> k; rewrite !mxE. -- by move=> t1 IH1 rt1; rewrite -{}IH1 //; apply/rowP=> k; rewrite !mxE. +- by move=> t1 + rt1 => <-//; apply/rowP=> k; rewrite !mxE. - move=> t1 IH1 n1 rt1; rewrite eval_mulmx eval_mx_term mul_scalar_mx. by rewrite scaler_nat {}IH1 //; elim: n1 => //= n1 IHn1; rewrite !mulrS IHn1. - by move=> t1 IH1 t2 IH2 /andP[rt1 rt2]; rewrite eval_mulT IH1 ?IH2. diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v index 0ece733..0c9e94f 100644 --- a/mathcomp/ssreflect/bigop.v +++ b/mathcomp/ssreflect/bigop.v @@ -1045,8 +1045,8 @@ Lemma big_index_uniq (I : eqType) (r : seq I) (E : 'I_(size r) -> R) : uniq r -> \big[op/idx]_i E i = \big[op/idx]_(x <- r) oapp E idx (insub (index x r)). Proof. -move=> Ur; apply/esym; rewrite big_tnth; apply: eq_bigr => i _. -by rewrite index_uniq // valK. +move=> Ur; apply/esym; rewrite big_tnth. +by under [LHS]eq_bigr do rewrite index_uniq// valK. Qed. Lemma big_tuple I n (t : n.-tuple I) (P : pred I) F : @@ -1087,9 +1087,8 @@ Lemma big_ord_recl n F : op (F ord0) (\big[op/idx]_(i < n) F (@lift n.+1 ord0 i)). Proof. pose G i := F (inord i); have eqFG i: F i = G i by rewrite /G inord_val. -rewrite (eq_bigr _ (fun i _ => eqFG i)) -(big_mkord _ (fun _ => _) G) eqFG. -rewrite big_ltn // big_add1 /= big_mkord; congr op. -by apply: eq_bigr => i _; rewrite eqFG. +under eq_bigr do rewrite eqFG; under [in RHS]eq_bigr do rewrite eqFG. +by rewrite -(big_mkord _ (fun _ => _) G) eqFG big_ltn // big_add1 /= big_mkord. Qed. Lemma big_nseq_cond I n a (P : pred I) F : @@ -1624,8 +1623,8 @@ Lemma exchange_big_dep I J rI rJ (P : pred I) (Q : I -> pred J) \big[*%M/1]_(j <- rJ | xQ j) \big[*%M/1]_(i <- rI | P i && Q i j) F i j. Proof. move=> PQxQ; pose p u := (u.2, u.1). -rewrite (eq_bigr _ _ _ (fun _ _ => big_tnth _ _ rI _ _)) (big_tnth _ _ rJ). -rewrite (eq_bigr _ _ _ (fun _ _ => (big_tnth _ _ rJ _ _))) big_tnth. +under [LHS]eq_bigr do rewrite big_tnth; rewrite [LHS]big_tnth. +under [RHS]eq_bigr do rewrite big_tnth; rewrite [RHS]big_tnth. rewrite !pair_big_dep (reindex_onto (p _ _) (p _ _)) => [|[]] //=. apply: eq_big => [] [j i] //=; symmetry; rewrite eqxx andbT andb_idl //. by case/andP; apply: PQxQ. @@ -1636,8 +1635,8 @@ Lemma exchange_big I J rI rJ (P : pred I) (Q : pred J) F : \big[*%M/1]_(i <- rI | P i) \big[*%M/1]_(j <- rJ | Q j) F i j = \big[*%M/1]_(j <- rJ | Q j) \big[*%M/1]_(i <- rI | P i) F i j. Proof. -rewrite (exchange_big_dep Q) //; apply: eq_bigr => i /= Qi. -by apply: eq_bigl => j; rewrite Qi andbT. +rewrite (exchange_big_dep Q) //. +by under eq_bigr => i Qi do under eq_bigl do rewrite Qi andbT. Qed. Lemma exchange_big_dep_nat m1 n1 m2 n2 (P : pred nat) (Q : rel nat) @@ -1647,7 +1646,7 @@ Lemma exchange_big_dep_nat m1 n1 m2 n2 (P : pred nat) (Q : rel nat) \big[*%M/1]_(m2 <= j < n2 | xQ j) \big[*%M/1]_(m1 <= i < n1 | P i && Q i j) F i j. Proof. -move=> PQxQ; rewrite (eq_bigr _ _ _ (fun _ _ => big_seq_cond _ _ _ _ _)). +move=> PQxQ; under eq_bigr do rewrite big_seq_cond. rewrite big_seq_cond /= (exchange_big_dep xQ) => [|i j]; last first. by rewrite !mem_index_iota => /andP[mn_i Pi] /andP[mn_j /PQxQ->]. rewrite 2!(big_seq_cond _ _ _ xQ); apply: eq_bigr => j /andP[-> _] /=. @@ -1660,7 +1659,7 @@ Lemma exchange_big_nat m1 n1 m2 n2 (P Q : pred nat) F : \big[*%M/1]_(m2 <= j < n2 | Q j) \big[*%M/1]_(m1 <= i < n1 | P i) F i j. Proof. rewrite (exchange_big_dep_nat Q) //. -by apply: eq_bigr => i /= Qi; apply: eq_bigl => j; rewrite Qi andbT. +by under eq_bigr => i Qi do under eq_bigl do rewrite Qi andbT. Qed. End Abelian. @@ -1754,7 +1753,7 @@ Proof. by rewrite big_endo ?mulm0 // => x y; apply: mulmDr. Qed. Lemma big_distrlr I J rI rJ (pI : pred I) (pJ : pred J) F G : (\big[+%M/0]_(i <- rI | pI i) F i) * (\big[+%M/0]_(j <- rJ | pJ j) G j) = \big[+%M/0]_(i <- rI | pI i) \big[+%M/0]_(j <- rJ | pJ j) (F i * G j). -Proof. by rewrite big_distrl; apply: eq_bigr => i _; rewrite big_distrr. Qed. +Proof. by rewrite big_distrl; under eq_bigr do rewrite big_distrr. Qed. Lemma big_distr_big_dep (I J : finType) j0 (P : pred I) (Q : I -> pred J) F : \big[*%M/1]_(i | P i) \big[+%M/0]_(j | Q i j) F i j = diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index 9747171..6c70502 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -3059,7 +3059,7 @@ move=> sz_s; apply/(canLR revK)/eq_from_flatten_shape. transitivity (rev (shape (reshape (rev sh) (rev s)))). by rewrite !reshapeKl ?revK ?size_rev ?sz_s ?sumn_rev. rewrite shape_rev; congr (rev _); rewrite -[RHS]map_comp. -by apply: eq_map => t /=; rewrite size_rev. +by under eq_map do rewrite /= size_rev. Qed. Lemma reshape_rcons s sh n (m := sumn sh) : @@ -3246,12 +3246,11 @@ Proof. by []. Qed. Lemma eq_allpairs (f1 f2 : forall x, T x -> R) s t : (forall x, f1 x =1 f2 x) -> [seq f1 x y | x <- s, y <- t x] = [seq f2 x y | x <- s, y <- t x]. -Proof. by move=> eq_f; rewrite (eq_map (fun x => eq_map (eq_f x) (t x))). Qed. +Proof. by move=> eq_f; under eq_map do under eq_map do rewrite eq_f. Qed. Lemma eq_allpairsr (f : forall x, T x -> R) s t1 t2 : (forall x, t1 x = t2 x) -> [seq f x y | x <- s, y <- t1 x] = [seq f x y | x <- s, y <- t2 x]. -(* From Coq 8.10 Proof. by move=> eq_t; under eq_map do rewrite eq_t. Qed. *) -Proof. by move=> eq_t; congr flatten; apply: eq_map => x; rewrite eq_t. Qed. +Proof. by move=> eq_t; under eq_map do rewrite eq_t. Qed. Lemma allpairs_cat f s1 s2 t : [seq f x y | x <- s1 ++ s2, y <- t x] = @@ -3270,7 +3269,7 @@ Proof. by rewrite -map_comp. Qed. 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. +Proof. by under eq_map do rewrite -map_comp. Qed. End AllPairsDep. @@ -3517,8 +3516,7 @@ Local Notation tseq := tally_seq. Lemma size_tally_seq bs : size (tally_seq bs) = sumn (unzip2 bs). Proof. -rewrite size_flatten /shape -map_comp; congr sumn. -by apply/eq_map=> b; apply: size_nseq. +by rewrite size_flatten /shape -map_comp; under eq_map do rewrite /= size_nseq. Qed. Lemma tally_seqK : {in wf_tally, cancel tally_seq tally}. @@ -3570,7 +3568,7 @@ Proof. have /andP[Ubs _] := tallyP s; pose b := [fun s x => (x, count_mem x (tseq s))]. suffices /permPl->: perm_eq (tally s) (map (b (tally s)) (unzip1 (tally s))). congr perm_eq: (perm_map (b (tally s)) (tallyEl s)). - by apply/eq_map=> x; rewrite /= (permP (tallyK s)). + by under eq_map do rewrite /= (permP (tallyK s)). elim: (tally s) Ubs => [|[x m] bs IH] //= /andP[bs'x /IH-IHbs {IH}]. rewrite /tseq /= -/(tseq _) count_cat count_nseq /= eqxx mul1n. rewrite (count_memPn _) ?addn0 ?perm_cons; last first. @@ -3583,7 +3581,7 @@ Qed. Lemma perm_tally s1 s2 : perm_eq s1 s2 -> perm_eq (tally s1) (tally s2). Proof. move=> eq_s12; apply: (@perm_trans _ [seq (x, count_mem x s2) | x <- undup s1]). - by congr perm_eq: (tallyE s1); apply/eq_map=> x; rewrite (permP eq_s12). + by congr perm_eq: (tallyE s1); under eq_map do rewrite (permP eq_s12). by rewrite (permPr (tallyE s2)); apply/perm_map/perm_undup/(perm_mem eq_s12). Qed. @@ -3630,8 +3628,8 @@ have cpE: forall f & forall s bs, is_acc (f s bs), is_acc (cons_perms_ f _ _ _). have prE: is_acc (perms_rec _ _ _) by elim=> //= n IHn s bs; apply: cpE. pose has_suffix f := forall s : seq T, f s = [seq t ++ s | t <- f [::]]. suffices prEs n bs: has_suffix (fun s => perms_rec n s bs [::]). - move=> n x bs bs1 bs2 /=; rewrite cpE // prEs; congr (_ ++ _). - by apply/eq_map=> t; rewrite cats1. + move=> n x bs bs1 bs2 /=; rewrite cpE // prEs. + by under eq_map do rewrite cats1. elim: n bs => //= n IHn bs s; elim: bs [::] => [|[x [|m]] bs IHbs] //= bs1. rewrite cpE // IHbs IHn [in RHS]cpE // [in RHS]IHn map_cat -map_comp. by congr (_ ++ _); apply: eq_map => t /=; rewrite -catA. |