diff options
Diffstat (limited to 'mathcomp/ssreflect')
| -rw-r--r-- | mathcomp/ssreflect/Make | 2 | ||||
| -rw-r--r-- | mathcomp/ssreflect/bigop.v | 2 | ||||
| -rw-r--r-- | mathcomp/ssreflect/div.v | 2 | ||||
| -rw-r--r-- | mathcomp/ssreflect/finfun.v | 2 | ||||
| -rw-r--r-- | mathcomp/ssreflect/finset.v | 4 | ||||
| -rw-r--r-- | mathcomp/ssreflect/order.v | 6 | ||||
| -rw-r--r-- | mathcomp/ssreflect/path.v | 4 | ||||
| -rw-r--r-- | mathcomp/ssreflect/prime.v | 8 | ||||
| -rw-r--r-- | mathcomp/ssreflect/tuple.v | 2 |
9 files changed, 16 insertions, 16 deletions
diff --git a/mathcomp/ssreflect/Make b/mathcomp/ssreflect/Make index d6879a6..b909046 100644 --- a/mathcomp/ssreflect/Make +++ b/mathcomp/ssreflect/Make @@ -28,7 +28,7 @@ order.v -arg -w -arg -projection-no-head-constant -arg -w -arg -redundant-canonical-projection -arg -w -arg -notation-overridden --arg -w -arg -duplicate-clear +-arg -w -arg +duplicate-clear -arg -w -arg -ambiguous-paths -arg -w -arg +undeclared-scope -arg -w -arg -non-reversible-notation
\ No newline at end of file diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v index cd3507a..7d8332c 100644 --- a/mathcomp/ssreflect/bigop.v +++ b/mathcomp/ssreflect/bigop.v @@ -1770,7 +1770,7 @@ rewrite -{P mem_r}big_r; elim: r Ur => /= [_ | i r IHr]. rewrite (big_pred1 [ffun=> j0]) ?big_nil //= => f. apply/familyP/eqP=> /= [Df |->{f} i]; last by rewrite ffunE !inE. by apply/ffunP=> i; rewrite ffunE; apply/eqP/Df. -case/andP=> /negbTE nri; rewrite big_cons big_distrl => {IHr}/IHr <-. +case/andP=> /negbTE nri; rewrite big_cons big_distrl => {}/IHr<-. rewrite (partition_big (fun f : fIJ => f i) (Q i)) => [|f]; last first. by move/familyP/(_ i); rewrite /= inE /= eqxx. pose seti j (f : fIJ) := [ffun k => if k == i then j else f k]. diff --git a/mathcomp/ssreflect/div.v b/mathcomp/ssreflect/div.v index 4899ee3..ae46cd3 100644 --- a/mathcomp/ssreflect/div.v +++ b/mathcomp/ssreflect/div.v @@ -709,7 +709,7 @@ rewrite !natTrecE; set m := _ + r; set km := _ + kn; pose d := gcdn m n. have ->: gcdn n r = d by rewrite [d]gcdnC gcdnMDl. have m_gt0: 0 < m by rewrite addn_gt0 r_gt0 orbT. have d_gt0: 0 < d by rewrite gcdn_gt0 m_gt0. -move/IHq=> {IHq} IHq le_kn_r le_kr_n def_d; apply: IHq => //; rewrite -/d. +move=> {}/IHq IHq le_kn_r le_kr_n def_d; apply: IHq => //; rewrite -/d. by rewrite mulnDl leq_add // -mulnA leq_mul2l le_kr_n orbT. apply: (@addIn d); rewrite mulnDr -addnA addnACA -def_d addnACA mulnA. rewrite -!mulnDl -mulnDr -addnA [kr * _]mulnC; congr addn. diff --git a/mathcomp/ssreflect/finfun.v b/mathcomp/ssreflect/finfun.v index 0218f6a..1fd1a83 100644 --- a/mathcomp/ssreflect/finfun.v +++ b/mathcomp/ssreflect/finfun.v @@ -175,7 +175,7 @@ Proof. suffices ffunK f g: (forall x, f x = g x) -> f = finfun g. by split=> [/ffunK|] -> //; apply/esym/ffunK. case: f => f Dg; rewrite unlock; congr FinfunOf. -have{Dg} Dg x (aTx : mem_seq (enum aT) x): g x = fun_of_fin_rec f aTx. +have{} Dg x (aTx : mem_seq (enum aT) x): g x = fun_of_fin_rec f aTx. by rewrite -Dg /= (bool_irrelevance (mem_enum _ _) aTx). elim: (enum aT) / f (enum_uniq aT) => //= x1 s y f IHf /andP[s'x1 Us] in Dg *. rewrite Dg ?eqxx //=; case: eqP => // /eq_axiomK-> /= _. diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v index 3e60c2d..ef47cd2 100644 --- a/mathcomp/ssreflect/finset.v +++ b/mathcomp/ssreflect/finset.v @@ -1840,7 +1840,7 @@ Proof. have->: P = [set x in enum (mem P)] by apply/setP=> x; rewrite inE mem_enum. elim: {P}(enum _) (enum_uniq (mem P)) => [_ | A e IHe] /=. by rewrite /trivIset /cover !big_set0 cards0; left=> A; rewrite inE. -case/andP; rewrite set_cons -(in_set (fun B => B \in e)) => PA {IHe}/IHe. +case/andP; rewrite set_cons -(in_set (fun B => B \in e)) => PA {}/IHe. move: {e}[set x in e] PA => P PA IHP. rewrite /trivIset /cover !big_setU1 //= eq_sym. have:= leq_card_cover P; rewrite -(mono_leqif (leq_add2l #|A|)). @@ -2157,7 +2157,7 @@ move=> /and3P[/eqP defG tiP notP0] /and3P[/eqP defP tiQ notQ0]. have sQP E: E \in Q -> {subset E <= P}. by move=> Q_E; apply/subsetP; rewrite -defP (bigcup_max E). rewrite /partition cover_imset -(big_trivIset _ tiQ) defP -defG eqxx /= andbC. -have{notQ0} notQ0: set0 \notin cover @: Q. +have{} notQ0: set0 \notin cover @: Q. apply: contra notP0 => /imsetP[E Q_E E0]. have /set0Pn[/= A E_A] := memPn notQ0 E Q_E. congr (_ \in P): (sQP E Q_E A E_A). diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v index f40c1d5..97e34a2 100644 --- a/mathcomp/ssreflect/order.v +++ b/mathcomp/ssreflect/order.v @@ -6965,7 +6965,7 @@ Lemma leEtprod n T (t1 t2 : n.-tuple T) : Proof. elim: n => [|n IHn] in t1 t2 *. by rewrite tuple0 [t2]tuple0/= lexx; symmetry; apply/forallP => []. -case: (tupleP t1) (tupleP t2) => [x1 {t1}t1] [x2 {t2}t2]. +case: (tupleP t1) (tupleP t2) => [x1 {}t1] [x2 {}t2]. rewrite [_ <= _]le_cons [t1 <= t2 :> seq _]IHn. apply/idP/forallP => [/andP[lex12 /forallP/= let12 i]|lext12]. by case: (unliftP ord0 i) => [j ->|->]//; rewrite !tnthS. @@ -7275,7 +7275,7 @@ Lemma lexi_tupleP n T (t1 t2 : n.-tuple T) : Proof. elim: n => [|n IHn] in t1 t2 *. by rewrite tuple0 [t2]tuple0/= lexx; constructor; exists ord0 => -[]. -case: (tupleP t1) (tupleP t2) => [x1 {t1}t1] [x2 {t2}t2]. +case: (tupleP t1) (tupleP t2) => [x1 {}t1] [x2 {}t2]. rewrite [_ <= _]lexi_cons; apply: (iffP idP) => [|[k leif_xt12]]. case: comparableP => //= [ltx12 _|-> /IHn[k kP]]. exists ord0 => i; rewrite leqn0 => /eqP/(@ord_inj n.+1 i ord0)->. @@ -7296,7 +7296,7 @@ Lemma ltxi_tupleP n T (t1 t2 : n.-tuple T) : Proof. elim: n => [|n IHn] in t1 t2 *. by rewrite tuple0 [t2]tuple0/= ltxx; constructor => - [] []. -case: (tupleP t1) (tupleP t2) => [x1 {t1}t1] [x2 {t2}t2]. +case: (tupleP t1) (tupleP t2) => [x1 {}t1] [x2 {}t2]. rewrite [_ < _]ltxi_cons; apply: (iffP idP) => [|[k leif_xt12]]. case: (comparableP x1 x2) => //= [ltx12 _|-> /IHn[k kP]]. exists ord0 => i; rewrite leqn0 => /eqP/(@ord_inj n.+1 i ord0)->. diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v index 72c9719..fa66807 100644 --- a/mathcomp/ssreflect/path.v +++ b/mathcomp/ssreflect/path.v @@ -687,12 +687,12 @@ Proof. move=> e_p; have: x \in x :: p by apply: mem_head. elim: p x {1 3 5}x e_p => [|y2 p IHp] x y1. by rewrite mem_seq1 => _ /eqP->. -rewrite inE orbC /= => /andP[ey12 /IHp {IHp}IHp]. +rewrite inE orbC /= => /andP[ey12 {}/IHp IHp]. case: ifPn => [y2p_x _ | not_y2p_x /eqP def_x]. have [p' e_p' Up' p'p] := IHp _ y2p_x. by split=> // y /p'p; apply: predU1r. have [p' e_p' Up' p'p] := IHp y2 (mem_head y2 p). -have{p'p} p'p z: z \in y2 :: p' -> z \in y2 :: p. +have{} p'p z: z \in y2 :: p' -> z \in y2 :: p. by rewrite !inE; case: (z == y2) => // /p'p. rewrite -(last_cons y1) def_x; split=> //=; first by rewrite ey12. by rewrite (contra (p'p y1)) -?def_x. diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v index 389b1c2..ab8edce 100644 --- a/mathcomp/ssreflect/prime.v +++ b/mathcomp/ssreflect/prime.v @@ -216,13 +216,13 @@ have eq_bc_0: (b == 0) && (c == 0) = (d == 0). have lt1p: 1 < p by rewrite ltnS double_gt0. have co_p_2: coprime p 2 by rewrite /coprime gcdnC gcdnE modn2 /= odd_double. have if_d0: d = 0 -> [/\ m = (p + a.*2) * p, lb_dvd p p & lb_dvd p (p + a.*2)]. - move=> d0; have{d0 def_m} def_m: m = (p + a.*2) * p. + move=> d0; have{d0} def_m: m = (p + a.*2) * p. by rewrite d0 addn0 -!mul2n mulnA -mulnDl in def_m *. split=> //; apply/hasPn=> r /(hasPn leppm); apply: contra => /= dv_r. by rewrite def_m dvdn_mull. by rewrite def_m dvdn_mulr. case def_a: a => [|a'] /= in le_a_n *; rewrite !natTrecE -/p {}eq_bc_0. - case: d if_d0 def_m => [[//| def_m {pr_p}pr_p pr_m'] _ | d _ def_m] /=. + case: d if_d0 def_m => [[//| def_m {}pr_p pr_m'] _ | d _ def_m] /=. rewrite def_m def_a addn0 mulnA -2!expnSr. by split; rewrite /pd_ord /pf_ok /= ?muln1 ?pr_p ?leqnn. apply: apd_ok; rewrite // /pd_ok /= /pfactor expn1 muln1 /pd_ord /= ltpm. @@ -256,11 +256,11 @@ have ltdp: d < p. move/eqP: def_b'; rewrite subn_eq0 -(@leq_pmul2r kb); last first. by rewrite -def_kb1. rewrite mulnBl -def_k2 ltnS -(leq_add2r c); move/leq_trans; apply. - have{ltc} ltc: c < k.*2. + have{} ltc: c < k.*2. by apply: (leq_trans ltc); rewrite leq_double /kb; case e. rewrite -{2}(subnK (ltnW ltc)) leq_add2r leq_sub2l //. by rewrite -def_kb1 mulnS leq_addr. -case def_d: d if_d0 => [|d'] => [[//|{def_m ltdp pr_p} def_m pr_p pr_m'] | _]. +case def_d: d if_d0 => [|d'] => [[//|{ltdp pr_p}def_m pr_p pr_m'] | _]. rewrite eqxx -doubleS -addnS -def_a doubleD -addSn -/p def_m. rewrite mulnCA mulnC -expnSr. apply: IHn => {n le_a_n}//; rewrite -/p -/kb; split. diff --git a/mathcomp/ssreflect/tuple.v b/mathcomp/ssreflect/tuple.v index db53235..f32793f 100644 --- a/mathcomp/ssreflect/tuple.v +++ b/mathcomp/ssreflect/tuple.v @@ -349,7 +349,7 @@ Proof. case=> /= t t_n; rewrite -(count_map _ (pred1 t)) (pmap_filter (insubK _)). rewrite count_filter -(@eq_count _ (pred1 t)) => [|s /=]; last first. by rewrite isSome_insub; case: eqP=> // ->. -elim: n t t_n => [|m IHm] [|x t] //= {IHm}/IHm; move: (iter m _ _) => em IHm. +elim: n t t_n => [|m IHm] [|x t] //= {}/IHm; move: (iter m _ _) => em IHm. transitivity (x \in T : nat); rewrite // -mem_enum codomE. elim: (fintype.enum T) (enum_uniq T) => //= y e IHe /andP[/negPf ney]. rewrite count_cat count_map inE /preim /= [in LHS]/eq_op /= eq_sym => /IHe->. |