diff options
Diffstat (limited to 'mathcomp/ssreflect')
| -rw-r--r-- | mathcomp/ssreflect/bigop.v | 23 | ||||
| -rw-r--r-- | mathcomp/ssreflect/seq.v | 20 |
2 files changed, 20 insertions, 23 deletions
diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v index 7d8332c..50f05d2 100644 --- a/mathcomp/ssreflect/bigop.v +++ b/mathcomp/ssreflect/bigop.v @@ -1047,8 +1047,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 : @@ -1089,9 +1089,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 : @@ -1626,8 +1625,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. @@ -1638,8 +1637,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) @@ -1649,7 +1648,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[-> _] /=. @@ -1662,7 +1661,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. @@ -1756,7 +1755,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 347a671..a0a0548 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -3070,7 +3070,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) : @@ -3257,12 +3257,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] = @@ -3281,7 +3280,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. @@ -3528,8 +3527,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}. @@ -3581,7 +3579,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. @@ -3594,7 +3592,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. @@ -3641,8 +3639,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. |