Get rid of "; by"

math-comp · Sep 23, 2018 · f3a37ba · f3a37ba
1 parent 0c39777
commit f3a37ba
Show file tree

Hide file tree

Showing 19 changed files with 1,103 additions and 1,062 deletions.
diff --git a/3rdparty/ALEA/Qmeasure.v b/3rdparty/ALEA/Qmeasure.v
@@ -1098,9 +1098,9 @@ Lemma mu_stable_sum (A : Type) (m : distr A)
   mu m (fun a => \sum_(i <- s) f i a) = \sum_(i <- s) (mu m (f i)).
 Proof.
 elim: s => [| s0 s IHs] /=.
-  rewrite big_nil; apply mu_zero_eq => x; by rewrite big_nil.
+  by rewrite big_nil; apply mu_zero_eq => x; rewrite big_nil.
 rewrite big_cons -IHs -mu_stable_add.
-apply Mstable_eq => x /=; by rewrite big_cons.
+by apply Mstable_eq => x /=; rewrite big_cons.
 Qed.
 
 
@@ -1113,7 +1113,7 @@ Lemma in_seq_sum s x :
   uniq s -> (x \in s)%:~R = \sum_(i <- s) (x == i)%:~R :> rat.
 Proof.
 elim: s => [| s0 s IHs] /=; first by rewrite big_nil.
-rewrite inE big_cons => /andP [] /negbTE Hs0 /IHs <- {IHs}.
+rewrite inE big_cons => /andP [/negbTE Hs0 /IHs <- {IHs}].
 case: (boolP (x == s0)) => [/= /eqP -> | _ ]; last by rewrite /= add0r.
 by rewrite Hs0 addr0.
 Qed.

diff --git a/theories/Combi/composition.v b/theories/Combi/composition.v
@@ -94,7 +94,7 @@ Lemma enum_compn_rec_any aux1 aux2 n :
   n <= aux1 -> n <= aux2 -> enum_compn_rec aux1 n = enum_compn_rec aux2 n.
 Proof.
 elim: aux1 aux2 n => [| aux1 IHaux1] aux2 n /=.
-  rewrite leqn0 => /eqP -> //=; by case aux2.
+  by rewrite leqn0 => /eqP -> //=; case aux2.
 case: (altP (n =P 0)) => [-> | Hn Haux1] //=; first by case aux2.
 case: aux2 => [| aux2 /= Haux2].
   by rewrite leqn0 => /eqP H; rewrite H eq_refl in Hn.
@@ -172,7 +172,7 @@ Qed.
 Lemma enum_compnP n s : (is_comp_of_n n s) = (s \in enum_compn n).
 Proof.
 apply/idP/idP; last by move/(allP (enum_compn_allP n)).
-rewrite -has_pred1 has_count; by move/enum_compn_countE ->.
+by rewrite -has_pred1 has_count; move/enum_compn_countE ->.
 Qed.
 
 
@@ -208,7 +208,7 @@ Definition intcomp_of_intcompn (p : intcompn) := IntComp (intcompnP p).
 Coercion intcomp_of_intcompn : intcompn >-> intcomp.
 
 Lemma intcompn_sumn (p : intcompn) : sumn p = n.
-Proof using . by case: p => /= p /andP [] /eqP. Qed.
+Proof using . by case: p => /= p /andP [/eqP]. Qed.
 
 Lemma enum_intcompnE : map val (enum {:intcompn}) = enum_compn n.
 Proof using . rewrite /=; exact: enum_subE. Qed.
@@ -231,18 +231,18 @@ Lemma intcompn2 (sh : intcompn 2) :
   sh = [:: 2]  :> seq nat \/ sh = [:: 1; 1] :> seq nat.
 Proof.
 case: sh => sh Hsh /=; move: Hsh; rewrite enum_compnP.
-rewrite /enum_compn /= !inE => /orP [] /eqP ->; by [left | right].
+by rewrite /enum_compn /= !inE => /orP [] /eqP ->; [right | left].
 Qed.
 
 Definition intcompn_cast m n (eq_mn : m = n) p :=
   let: erefl in _ = n := eq_mn return intcompn n in p.
 
 Lemma intcompn_castE m n (eq_mn : m = n) p : val (intcompn_cast eq_mn p) = val p.
-Proof. subst m; by case: p. Qed.
+Proof. by subst m; case: p. Qed.
 
 Definition rowcomp d := if d is _.+1 then [:: d] else [::].
 Fact rowcompnP d : is_comp_of_n d (rowcomp d).
-Proof. case: d => [//= | d]; by rewrite /is_comp_of_n /= addn0 eq_refl. Qed.
+Proof. by case: d => [//= | d]; rewrite /is_comp_of_n /= addn0 eq_refl. Qed.
 Canonical rowcompn d : intcompn d := IntCompN (rowcompnP d).
 
 Definition colcomp d := nseq d 1%N.

diff --git a/theories/Combi/vectNK.v b/theories/Combi/vectNK.v
@@ -43,7 +43,7 @@ Fixpoint vect_n_k n k :=
 Lemma vect_n_k_in n k s : sumn s == n -> size s == k -> s \in vect_n_k n k.
 Proof.
 elim: k n s => [| k IHk n].
-- case => [s _ /nilP -> //= | n]; by case.
+- by case => [s _ /nilP -> //= | n]; case.
 - case => [//= | s0 s] /eqP Hsum Hsize.
   apply/flattenP; rewrite -/vect_n_k /mkseq.
   exists (map (cons s0) (vect_n_k (n - s0) k)).
@@ -57,10 +57,10 @@ Qed.
 Lemma in_vect_n_k n k s : s \in vect_n_k n k -> (sumn s == n) && (size s == k).
 Proof.
 elim: k n s => [| k IHk n]; first case => [[| s0 s]|] //=.
-case => [|s0 s] /flattenP [] ll /mapP [] i Hi -> /mapP [] s' //=.
-rewrite -/vect_n_k => /IHk /andP [] /eqP Hsum /eqP Hsize [] -> ->.
+case => [|s0 s] /flattenP /= [ll /mapP [i Hi ->] /mapP [s' //=]].
+rewrite -/vect_n_k => /IHk /andP [/eqP Hsum /eqP Hsize] [-> ->].
 rewrite Hsize /= eq_refl andbT Hsum.
-move: Hi; rewrite mem_iota add0n ltnS => /andP [] _ Hi.
+move: Hi; rewrite mem_iota add0n ltnS => /andP [_ Hi].
 by rewrite addnC subnK.
 Qed.
 
@@ -78,17 +78,16 @@ Lemma count_mem_vect_n_k_eq_1 n k s :
 Proof.
 elim: k n s=> [/=| k IHk n s]; first by case=> s //=; rewrite mem_seq1 => /eqP ->.
 rewrite count_flatten -/vect_n_k -map_comp.
-case: s => [|s0 s]; first by rewrite vect_n_kP /= => /andP [] _.
-move/flatten_mapP; rewrite -/vect_n_k => [] [] i.
+case: s => [|s0 s]; first by rewrite vect_n_kP /= => /andP [_].
+move/flatten_mapP; rewrite -/vect_n_k => [] [i].
 rewrite mem_iota [iota _ _]lock add0n => Hs0.
-move/mapP => [] t Ht [] H1 H2; subst i; subst t.
+move/mapP => [t Ht [H1 H2]]; subst i; subst t.
 rewrite (eq_map (f2 := (fun i : nat => i == s0 : nat))).
   by unlock; apply: sumn_iota; rewrite add0n.
 move=> i; rewrite /= count_map /=.
 rewrite (eq_count (a2 := fun t => (i == s0) && (s == t))); first last.
   rewrite /= /preim => t /=.
-  apply/idP/idP => [/eqP [] -> -> | /andP [] /eqP -> /eqP -> //].
-  by rewrite !eq_refl.
+  by apply/eqP/andP => [[-> ->] | [/eqP -> /eqP ->]].
 case H : (i == s0) => /=; last by rewrite count_pred0.
 rewrite (eq_count (a2 := (xpred1 s))); last exact: eq_sym.
 by apply: IHk; rewrite (eqP H).
@@ -129,13 +128,13 @@ Qed.
 Lemma flatten_equiv_cut_k s ss : s == flatten ss <-> ss \in cut_k (size ss) s.
 Proof using.
 split; first by move=> /eqP ->; apply (cut_k_flatten ss).
-move => /mapP [] sh; rewrite vect_n_kP => /andP [] /eqP Hsum _ H; subst ss.
+move => /mapP [sh]; rewrite vect_n_kP => /andP [/eqP Hsum _] H; subst ss.
 by rewrite reshapeKr; last rewrite Hsum.
 Qed.
 
 Lemma size_cut_k k s ss : ss \in (cut_k k s) -> size ss = k.
 Proof using.
-rewrite /cut_k => /mapP [] sh /in_vect_n_k /andP [] /eqP Hsum /eqP Hsize -> {ss}.
+rewrite /cut_k => /mapP [sh /in_vect_n_k/andP [/eqP Hsum /eqP Hsize] -> {ss}].
 by rewrite -(size_map size _) -/(shape _) reshapeKl; last rewrite Hsum.
 Qed.
 
@@ -160,13 +159,13 @@ Lemma cat3_equiv_cut3 s a b c : s == a ++ b ++ c <-> (a, b, c) \in cut3 s.
 Proof using.
 have -> : (a ++ b ++ c) = flatten [:: a; b; c] by rewrite /= cats0.
 rewrite flatten_equiv_cut_k /cut3; split.
-- move=> H; apply/mapP; by exists [:: a; b; c].
-- move=> /mapP [] t.
+- by move=> H; apply/mapP; exists [:: a; b; c].
+- move=> /mapP [t].
   case: t => [| t0 t]; first by rewrite /cut_k => /size_cut_k.
   case: t => [| t1 t]; first by rewrite /cut_k => /size_cut_k.
   case: t => [| t2 t]; first by rewrite /cut_k => /size_cut_k.
   case: t => [| t3 t]; last by rewrite /cut_k => /size_cut_k.
-  by move=> Hcut [] -> -> ->.
+  by move=> Hcut [-> -> ->].
 Qed.
 
 End Cut3.
diff --git a/theories/LRrule/Yam_plact.v b/theories/LRrule/Yam_plact.v
@@ -54,8 +54,8 @@ Lemma is_part_incr_nthE sh i j :
   i.+1 < j -> is_part sh -> is_part (incr_nth (incr_nth sh j) i) ->
   is_part (incr_nth sh i) = is_part (incr_nth sh j).
 Proof.
-move=> Hij Hpart /is_partP [] Hlastji Hpartij.
-apply/idP/idP => /is_partP [] H1 H2; apply: (is_part_incr_nth Hpart) => /=.
+move=> Hij Hpart /is_partP [Hlastji Hpartij].
+apply/idP/idP => /is_partP [H1 H2]; apply: (is_part_incr_nth Hpart) => /=.
 - case H : j => [//= | j'] /=; subst j.
   move/(_ j'): Hpartij; rewrite !nth_incr_nth.
   rewrite eq_refl (ltn_eqF (ltnW Hij)).
@@ -73,7 +73,7 @@ Lemma is_part_incr_nth1E sh i :
 Proof.
 move=> Hpart; apply/idP/idP => Hparti.
 - apply (is_part_incr_nth Hpart) => /=.
-  case: i Hparti => [//= | i] /is_partP [] _ Hparti /=.
+  case: i Hparti => [//= | i] /is_partP [_ Hparti /=].
   move/(_ i): Hparti.
   rewrite !nth_incr_nth /= eq_refl.
   rewrite eq_sym ltn_eqF // eq_sym ltn_eqF //.
@@ -83,18 +83,18 @@ move=> Hpart; apply/idP/idP => Hparti.
   elim: sh i Hpart Hparti => [//= | s0 sh IHsh] /= i.
     by move=> _ /part_head_non0 Hhead; have -> : i = 0 by case: i Hhead.
   case: i => [| i] /=  /andP [Head Hp]; first by move=> _ ; move: Head; case sh.
-  by move=> /andP [] _ Hpi; exact: IHsh.
+  by move=> /andP [_ Hpi]; exact: IHsh.
 Qed.
 
 Lemma is_yam_plactic y : is_yam y -> forall w, y =Pl w -> is_yam w.
 Proof.
 move=> Hy; apply: gencongr_ind; first exact Hy.
 elim => [/= | a0 aw /= IHaw].
 - move=> b1 cw b2 H /plactruleP [] Hrew.
-  + move: Hrew H => /plact1P [] a [] b [] c [].
-    rewrite leqXnatE ltnXnatE => /andP [] Hab Hbc -> -> /=.
+  + move: Hrew H => /plact1P [a] [b] [c] [].
+    rewrite leqXnatE ltnXnatE => /andP [Hab Hbc] -> -> /=.
     set yc := (incr_nth (evalseq cw) b).
-    move=> /and4P [] H1 H2 Hpart ->; rewrite Hpart.
+    move=> /and4P [H1 H2 Hpart ->]; rewrite Hpart.
     rewrite incr_nthC H1 !andbT /=.
     case (ltnP a.+1 c) => Hac; first by rewrite (is_part_incr_nthE Hac).
     have {Hab} Hab : a = b.
@@ -105,8 +105,8 @@ elim => [/= | a0 aw /= IHaw].
       by apply/eqP; rewrite eqn_leq Hbc Hac.
     subst c.
     by rewrite -is_part_incr_nth1E.
-  + move: Hrew H => /plact1iP [] a [] b [] c [].
-    rewrite leqXnatE ltnXnatE => /andP [] Hab Hbc -> -> /=.
+  + move: Hrew H => /plact1iP [a] [b] [c] [].
+    rewrite leqXnatE ltnXnatE => /andP [Hab Hbc] -> -> /=.
     set yc := (incr_nth (evalseq cw) b).
     move=> /and4P []; rewrite incr_nthC => H1 H2 Hpart Hyam.
     rewrite Hpart Hyam H1 !andbT /=.
@@ -120,8 +120,8 @@ elim => [/= | a0 aw /= IHaw].
     subst c; subst yc.
     rewrite incr_nthC is_part_incr_nth1E; first exact Hpart.
     exact: is_part_eval_yam.
-  + move: Hrew H => /plact2P [] a [] b [] c [].
-    rewrite leqXnatE ltnXnatE => /andP [] Hab Hbc -> -> /=.
+  + move: Hrew H => /plact2P [a] [b] [c] [].
+    rewrite leqXnatE ltnXnatE => /andP [Hab Hbc] -> -> /=.
     move=> /and4P []; rewrite [(incr_nth (incr_nth _ a) c)]incr_nthC.
     move => H1 H2 Hpart Hyam.
     rewrite Hyam H1 H2 !andbT /= {H1}.
@@ -131,11 +131,11 @@ elim => [/= | a0 aw /= IHaw].
       by apply/eqP; rewrite eqn_leq Hbc /=; exact: (leq_trans Hac).
     subst b.
     have {Hac Hab} Hac : c = a.+1.
-      apply/eqP; by rewrite eqn_leq Hac Hab.
+      by apply/eqP; rewrite eqn_leq Hac Hab.
     subst c.
     by rewrite -(is_part_incr_nth1E _ (is_part_eval_yam Hyam)).
-  + move: Hrew H => /plact2iP [] a [] b [] c [].
-    rewrite leqXnatE ltnXnatE => /andP [] Hab Hbc -> -> /=.
+  + move: Hrew H => /plact2iP [a] [b] [c] [].
+    rewrite leqXnatE ltnXnatE => /andP [Hab Hbc] -> -> /=.
     move=> /and4P []; rewrite (incr_nthC _ a c) => H1 H2 Hpart Hyam.
     rewrite Hyam H1 H2 !andbT /=.
     case (ltnP a.+1 c) => Hac.
@@ -147,9 +147,9 @@ elim => [/= | a0 aw /= IHaw].
       by apply/eqP; rewrite eqn_leq Hac Hab.
     subst c.
     apply (is_part_incr_nth (is_part_eval_yam Hyam)) => /=.
-    move: H1 => /is_partP [] _ /(_ a).
+    move: H1 => /is_partP [_ /(_ a)].
     by rewrite !nth_incr_nth !eq_refl [_.+1 == _]eq_sym  ltn_eqF.
-- move=> b1 cw b2 /andP [] Hpart Hyam Hrew.
+- move=> b1 cw b2 /andP [Hpart Hyam] Hrew.
   rewrite (IHaw _ _ _ Hyam Hrew) andbT.
   suff -> : (evalseq (aw ++ b2 ++ cw)) = (evalseq (aw ++ b1 ++ cw)) by [].
   rewrite -!evalseq_countE /evalseq_count /=.
@@ -196,12 +196,12 @@ apply /and4P; repeat split.
   by elim: l => [//= | l] /= ->; rewrite andbT.
 - have -> : head [::] (yamtab_rec i.+1 sh) = nseq (head 0 sh) i.+1.
     by case sh => [//= | l0 l] /=.
-  move: Hpart => /= /andP [] Hhead _.
+  move: Hpart => /= /andP [Hhead _].
   move: Hhead; case: sh {IHsh} => [//= | s1 /= _] Hs.
   apply /dominateP; split; first by rewrite !size_nseq.
   move=> j; rewrite size_nseq !nth_nseq => Hj.
   by rewrite Hj (leq_trans Hj Hs) ltnXnatE.
-- by move: Hpart => /= /andP [] _; exact: IHsh.
+- by move: Hpart => /= /andP [_]; exact: IHsh.
 Qed.
 
 Lemma yamtab_rcons sh sn :
@@ -224,32 +224,33 @@ have := is_part_sht Htab.
 rewrite /shape map_rcons -/shape.
 move: Hrec; move: (shape t) => sh Ht; subst t.
 case/lastP: sh Htab Hyam => [| sh sn] /=.
-  move=> /and3P [] _ Hrow _.
+  move=> /and3P [_ Hrow _].
   rewrite /yamtab /= cats0 => /last_yam Hlast _.
   case: tn Hrow Hlast => [//= | l0 tn] /=.
-  elim: tn l0 => [l0 _ /= -> //= | l1 t' IHt] /= l0 /andP [] Hl0l1 Hpath Hlast.
+  elim: tn l0 => [l0 _ /= -> //= | l1 t' IHt] /= l0 /andP [Hl0l1 Hpath] Hlast.
   have {IHt Hpath Hlast} [] := IHt l1 Hpath Hlast => Hl1 <-.
   by move: Hl0l1; rewrite Hl1 leqXnatE leqn0 => /eqP ->.
 rewrite {1}yamtab_rcons -2!cats1 -catA /=.
 move => /is_tableau_catr /= /and4P [].
-case: sn => [//= | sn] /= _ _ Hdom /and3P [] Hrow Hn2 _.
+case: sn => [//= | sn] /= _ _ Hdom /and3P [Hrow Hn2 _].
 rewrite to_word_yamtab size_rcons.
 case/lastP: tn Hrow Hn2 Hdom => [//=| tn ln] /= _ Hrow Hdom.
-rewrite -{1}cats1 -catA cat1s => /is_yam_catr /= /andP [] Hpart _ /is_part_rconsK Hp0.
+rewrite -{1}cats1 -catA cat1s.
+move=> /is_yam_catr /= /andP [Hpart _] /is_part_rconsK Hp0.
 move: Hpart; rewrite (evalseq_hyper_yam Hp0) => Hp1.
 have Hln : ln <= (size sh).+1.
   elim: sh ln Hp0 Hp1 {Hdom Hrow} => [| s0 sh IHsh] /= ln.
-    case: ln => [//= | ln] _ /= /andP [] _ /part_head_non0.
+    case: ln => [//= | ln] _ /= /andP [_ /part_head_non0].
     by case: ln.
   case: ln => [//= | ln].
-  rewrite ltnS /= => /andP [] _ H1 /andP [] _ H2.
+  rewrite ltnS /= => /andP [_ H1] /andP [_ H2].
   exact: IHsh.
 case: tn Hrow Hdom {Hp0 Hp1} => [_ /= | l0 tn].
-  move=> /dominateP [] _ Hdom; congr [:: _].
+  move=> /dominateP [_ Hdom]; congr [:: _].
   apply/eqP; rewrite eqn_leq Hln /=.
   have {Hdom} /= := Hdom 0 (ltn0Sn _).
   by rewrite ltnXnatE.
-rewrite rcons_cons => Hrow /dominateP [] _ Hdom.
+rewrite rcons_cons => Hrow /dominateP [_ Hdom].
 have {Hdom} /= := Hdom 0 (ltn0Sn _).
 rewrite ltnXnatE => Hl0.
 elim: tn l0 Hl0 Hrow => [/= | l1 tn /= IHtn] l0 Hl0; rewrite leqXnatE => /andP [].
@@ -264,7 +265,7 @@ move=> Hl0l1 Hpath.
 have Hrec :=  (IHtn l1 (leq_trans Hl0 Hl0l1) Hpath).
 rewrite -Hrec; congr (_ :: _).
 apply/eqP; rewrite eqn_leq Hl0 andbT.
-by move: Hrec => [] <- _.
+by move: Hrec => [<- _].
 Qed.
 
 Corollary RS_yam_RS y : is_yam y -> RS y = yamtab (shape (RS y)).
@@ -299,7 +300,7 @@ move=> Hyam; split.
 - move=> HPl; split; first exact (is_yam_plactic Hyam HPl).
   rewrite -(shape_RS_yam Hyam) -(shape_RS_yam (is_yam_plactic Hyam HPl)).
   exact: plactic_shapeRS.
-- move=> [] Hyamz Hsh.
+- move=> [Hyamz Hsh].
   apply Sch_plact.
   by rewrite (RS_yam Hyam) (RS_yam Hyamz) Hsh.
 Qed.
@@ -350,7 +351,7 @@ Theorem plact_from_yam sh w :
   { y | is_yam_of_eval sh y & std y = w }.
 Proof.
 move=> Hsh.
-have := (plactic_RS w (std (hyper_yam sh))) => [] [] H _.
+have := (plactic_RS w (std (hyper_yam sh))) => [] [H _].
 move=> /H => /eqP HRS.
 pose Sh := IntPart Hsh.
 have Hyam : is_yam_of_eval Sh (RSmap w).2.
@@ -370,7 +371,7 @@ exists y.
     by rewrite -RSmapE; case RSmap.
   rewrite RSE [RSmap w]RSE HRS.
   congr (RSmapinv2 (_, _)).
-  + have := stdtab_of_yamP (hyper_yamP Hsh); rewrite /is_stdtab => /andP [] Htab _.
+  + have := stdtab_of_yamP (hyper_yamP Hsh); rewrite /is_stdtab => /andP [Htab _].
     apply/eqP; rewrite -plactic_RS.
     apply std_plact.
     rewrite (yam_plactic_shape _ (yamevalP _)); split; first exact: hyper_yamP.