diff options
| -rw-r--r-- | CHANGELOG.md | 9 | ||||
| -rw-r--r-- | mathcomp/algebra/intdiv.v | 2 | ||||
| -rw-r--r-- | mathcomp/algebra/matrix.v | 4 | ||||
| -rw-r--r-- | mathcomp/algebra/poly.v | 2 | ||||
| -rw-r--r-- | mathcomp/algebra/polydiv.v | 14 | ||||
| -rw-r--r-- | mathcomp/fingroup/perm.v | 2 | ||||
| -rw-r--r-- | mathcomp/solvable/abelian.v | 6 | ||||
| -rw-r--r-- | mathcomp/solvable/burnside_app.v | 42 | ||||
| -rw-r--r-- | mathcomp/solvable/extraspecial.v | 2 | ||||
| -rw-r--r-- | mathcomp/solvable/maximal.v | 2 | ||||
| -rw-r--r-- | mathcomp/ssreflect/eqtype.v | 13 | ||||
| -rw-r--r-- | mathcomp/ssreflect/finset.v | 6 | ||||
| -rw-r--r-- | mathcomp/ssreflect/seq.v | 6 |
13 files changed, 55 insertions, 55 deletions
diff --git a/CHANGELOG.md b/CHANGELOG.md index 7d6f2d4..9fc7501 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -7,10 +7,13 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). ## [Unreleased] -### Added +### Changed -- `eqPsym`, a view which is like `eqP`, but in addition it allows - simultaneous destruction of expressions of the form `x == y` and `y == x`. +- `eqVneq` lemma is changed from `{x = y} + {x != y}` to + `eq_xor_neq x y (y == x) (x == y)` which allows to use it as + a view like `eqP`, in addition providing simultaneous destruction + of expressions of the form `x == y` and `y == x`, while keeping + the ability to use it in a way it was used before. ## [1.9.0] - 2019-05-22 diff --git a/mathcomp/algebra/intdiv.v b/mathcomp/algebra/intdiv.v index edd2620..0a5bfde 100644 --- a/mathcomp/algebra/intdiv.v +++ b/mathcomp/algebra/intdiv.v @@ -969,7 +969,7 @@ without loss{IHa} /forallP/(_ (_, _))/= a_dvM: / [forall k, a %| M k.1 k.2]%Z. by exists i; rewrite mxE. exists R^T; last exists L^T; rewrite ?unitmx_tr //; exists d => //. rewrite -[M]trmxK dM !trmx_mul mulmxA; congr (_ *m _ *m _). - by apply/matrixP=> i1 j1; rewrite !mxE; case: eqPsym => // ->. + by apply/matrixP=> i1 j1; rewrite !mxE; case: eqVneq => // ->. without loss{nz_a a_dvM} a1: M a Da / a = 1. pose M1 := map_mx (divz^~ a) M; case/(_ M1 1)=> // [k|L uL [R uR [d dvD dM]]]. by rewrite !mxE Da divzz nz_a. diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index ff9d43a..9d6e2be 100644 --- a/mathcomp/algebra/matrix.v +++ b/mathcomp/algebra/matrix.v @@ -1392,7 +1392,7 @@ Definition diag_mx n (d : 'rV[R]_n) := \matrix[diag_mx_key]_(i, j) (d 0 i *+ (i == j)). Lemma tr_diag_mx n (d : 'rV_n) : (diag_mx d)^T = diag_mx d. -Proof. by apply/matrixP=> i j; rewrite !mxE; case: eqPsym => // ->. Qed. +Proof. by apply/matrixP=> i j; rewrite !mxE; case: eqVneq => // ->. Qed. Lemma diag_mx_is_linear n : linear (@diag_mx n). Proof. @@ -1744,7 +1744,7 @@ by rewrite eqn_leq andbC leqNgt lshift_subproof. Qed. Lemma tr_pid_mx m n r : (pid_mx r)^T = pid_mx r :> 'M_(n, m). -Proof. by apply/matrixP=> i j; rewrite !mxE; case: eqPsym => // ->. Qed. +Proof. by apply/matrixP=> i j; rewrite !mxE; case: eqVneq => // ->. Qed. Lemma pid_mx_minv m n r : pid_mx (minn m r) = pid_mx r :> 'M_(m, n). Proof. by apply/matrixP=> i j; rewrite !mxE leq_min ltn_ord. Qed. diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v index d898774..a3b9211 100644 --- a/mathcomp/algebra/poly.v +++ b/mathcomp/algebra/poly.v @@ -368,7 +368,7 @@ Lemma nil_poly p : nilp p = (p == 0). Proof. exact: size_poly_eq0. Qed. Lemma poly0Vpos p : {p = 0} + {size p > 0}. -Proof. by rewrite lt0n size_poly_eq0; apply: eqVneq. Qed. +Proof. by rewrite lt0n size_poly_eq0; case: eqVneq; [left | right]. Qed. Lemma polySpred p : p != 0 -> size p = (size p).-1.+1. Proof. by rewrite -size_poly_eq0 -lt0n => /prednK. Qed. diff --git a/mathcomp/algebra/polydiv.v b/mathcomp/algebra/polydiv.v index 6f9d837..2ac2c3e 100644 --- a/mathcomp/algebra/polydiv.v +++ b/mathcomp/algebra/polydiv.v @@ -2037,8 +2037,7 @@ Lemma egcdp_recP : forall k p q, q != 0 -> size q <= k -> size q <= size p -> [/\ size e.1 <= size q, size e.2 <= size p & gcdp p q %= e.1 * p + e.2 * q]. Proof. elim=> [|k ihk] p q /= qn0; first by rewrite leqn0 size_poly_eq0 (negPf qn0). -move=> sqSn qsp; case: (eqVneq q 0)=> q0; first by rewrite q0 eqxx in qn0. -rewrite (negPf qn0). +move=> sqSn qsp; rewrite (negPf qn0). have sp : size p > 0 by apply: leq_trans qsp; rewrite size_poly_gt0. case: (eqVneq (p %% q) 0) => [r0 | rn0] /=. rewrite r0 /egcdp_rec; case: k ihk sqSn => [|n] ihn sqSn /=. @@ -2239,8 +2238,7 @@ Proof. apply/eqP/idP=> [d0|]; last first. case/or3P; [by move/eqP->; rewrite div0p| by move/eqP->; rewrite divp0|]. by move/divp_small. -case: (eqVneq p 0) => [->|pn0]; first by rewrite eqxx. -case: (eqVneq q 0) => [-> | qn0]; first by rewrite eqxx orbT. +case: (eqVneq p 0) => [->//|pn0]; case: (eqVneq q 0) => [->//| qn0]. move: (divp_eq p q); rewrite d0 mul0r add0r. move/(f_equal (fun x : {poly R} => size x)). by rewrite size_scale ?lc_expn_scalp_neq0 // => ->; rewrite ltn_modp qn0 !orbT. @@ -3039,8 +3037,8 @@ Proof. move=> eqr; rewrite /gdcop; move: (size p)=> n. elim: n p q r eqr {1 3}p (eqpxx p) => [|n ihn] p q r eqr s esp /=. move: eqr; case: (eqVneq q 0)=> [-> | nq0 eqr] /=. - by rewrite eqp_sym eqp0; move->; rewrite eqxx eqpxx. - suff rn0 : r != 0 by rewrite (negPf nq0) (negPf rn0) eqpxx. + by rewrite eqp_sym eqp0 => ->; rewrite eqpxx. + suff rn0 : r != 0 by rewrite (negPf rn0) eqpxx. by apply: contraTneq eqr => ->; rewrite eqp0. rewrite (eqp_coprimepr _ eqr) (eqp_coprimepl _ esp); case: ifP=> _ //. by apply: ihn => //; apply: eqp_div => //; apply: eqp_gcd. @@ -3051,8 +3049,8 @@ Proof. rewrite /rgdcop /gdcop; move: (size p)=> n. elim: n p q {1 3}p {1 3}q (eqpxx p) (eqpxx q) => [|n ihn] p q s t /= sp tq. move: tq; case: (eqVneq t 0)=> [-> | nt0 etq]. - by rewrite eqp_sym eqp0; move->; rewrite eqxx eqpxx. - suff qn0 : q != 0 by rewrite (negPf nt0) (negPf qn0) eqpxx. + by rewrite eqp_sym eqp0 => ->; rewrite eqpxx. + suff qn0 : q != 0 by rewrite (negPf qn0) eqpxx. by apply: contraTneq etq => ->; rewrite eqp0. rewrite rcoprimep_coprimep (eqp_coprimepl t sp) (eqp_coprimepr p tq). case: ifP=> // _; apply: ihn => //; apply: eqp_trans (eqp_rdiv_div _ _) _. diff --git a/mathcomp/fingroup/perm.v b/mathcomp/fingroup/perm.v index a1bb896..f1ff532 100644 --- a/mathcomp/fingroup/perm.v +++ b/mathcomp/fingroup/perm.v @@ -570,7 +570,7 @@ apply/permP=> i; case: (unliftP j i) => [i'|] ->; last first. apply: ord_inj; rewrite lift_perm_lift !permE /= eq_sym -if_neg neq_lift. rewrite fun_if -val_eqE /= def_k /bump ltn_neqAle andbC. case: leqP => [_ | lt_i'm] /=; last by rewrite -if_neg neq_ltn leqW. -by rewrite add1n eqSS; case: eqPsym. +by rewrite add1n eqSS; case: eqVneq. Qed. End LiftPerm. diff --git a/mathcomp/solvable/abelian.v b/mathcomp/solvable/abelian.v index a51cbf2..dd14013 100644 --- a/mathcomp/solvable/abelian.v +++ b/mathcomp/solvable/abelian.v @@ -836,9 +836,9 @@ Qed. Lemma rank_gt0 G : ('r(G) > 0) = (G :!=: 1). Proof. -case: (eqsVneq G 1) => [-> |]; first by rewrite rank1 eqxx. -case: (trivgVpdiv G) => [-> | [p p_pr]]; first by case/eqP. -case/Cauchy=> // x Gx oxp ->; apply: leq_trans (p_rank_le_rank p G). +case: (eqsVneq G 1) => [-> |]; first by rewrite rank1. +case: (trivgVpdiv G) => [-> | [p p_pr]]; first by rewrite eqxx. +case/Cauchy=> // x Gx oxp _; apply: leq_trans (p_rank_le_rank p G). have EpGx: <[x]>%G \in 'E_p(G). by rewrite inE cycle_subG Gx abelemE // cycle_abelian -oxp exponent_dvdn. by apply: leq_trans (logn_le_p_rank EpGx); rewrite -orderE oxp logn_prime ?eqxx. diff --git a/mathcomp/solvable/burnside_app.v b/mathcomp/solvable/burnside_app.v index 4e84bb5..18c6509 100644 --- a/mathcomp/solvable/burnside_app.v +++ b/mathcomp/solvable/burnside_app.v @@ -371,7 +371,7 @@ Lemma F_r3 : 'Fix_to[r3] = Proof. apply/setP=> x; rewrite (sameP afix1P eqP) !inE eqperm_map /=. rewrite /act_f r3_inv !ffunE !permE /=. -by do 3![case: eqPsym=> // <-]. +by do 3![case: eqVneq=> // <-]. Qed. Lemma card_n2 : forall x y z t : square, uniq [:: x; y; z; t] -> @@ -950,7 +950,7 @@ Proof. apply sym_equal. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g r05_inv !ffunE !permE /=. rewrite !eqxx /= !andbT /col1/col2/col3/col4/col5/col0. -by do 3![case: eqPsym; rewrite ?andbF // => <-]. +by do 3![case: eqVneq; rewrite ?andbF // => <-]. Qed. Lemma F_r50 : 'Fix_to_g[r50]= @@ -959,7 +959,7 @@ Lemma F_r50 : 'Fix_to_g[r50]= Proof. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g r50_inv !ffunE !permE /=. apply sym_equal; rewrite !eqxx /= !andbT /col1/col2/col3/col4. -by do 3![case: eqPsym; rewrite ?andbF // => <-]. +by do 3![case: eqVneq; rewrite ?andbF // => <-]. Qed. Lemma F_r23 : 'Fix_to_g[r23] = @@ -969,7 +969,7 @@ Proof. have r23_inv: r23^-1 = r32 by inv_tac. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g r23_inv !ffunE !permE /=. apply sym_equal; rewrite !eqxx /= !andbT /col1/col0/col5/col4. -by do 3![case: eqPsym; rewrite ?andbF // => <-]. +by do 3![case: eqVneq; rewrite ?andbF // => <-]. Qed. Lemma F_r32 : 'Fix_to_g[r32] = @@ -979,7 +979,7 @@ Proof. have r32_inv: r32^-1 = r23 by inv_tac. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g r32_inv !ffunE !permE /=. apply sym_equal; rewrite !eqxx /= !andbT /col1/col0/col5/col4. -by do 3![case: eqPsym; rewrite ?andbF // => <-]. +by do 3![case: eqVneq; rewrite ?andbF // => <-]. Qed. Lemma F_r14 : 'Fix_to_g[r14] = @@ -987,7 +987,7 @@ Lemma F_r14 : 'Fix_to_g[r14] = Proof. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g r14_inv !ffunE !permE /=. apply sym_equal; rewrite !eqxx /= !andbT /col2/col0/col5/col3. -by do 3![case: eqPsym; rewrite ?andbF // => <-]. +by do 3![case: eqVneq; rewrite ?andbF // => <-]. Qed. Lemma F_r41 : 'Fix_to_g[r41] = @@ -995,7 +995,7 @@ Lemma F_r41 : 'Fix_to_g[r41] = Proof. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g r41_inv !ffunE !permE /=. apply sym_equal; rewrite !eqxx /= !andbT /col2/col0/col5/col3. -by do 3![case: eqPsym; rewrite ?andbF // => <-]. +by do 3![case: eqVneq; rewrite ?andbF // => <-]. Qed. Lemma F_r024 : 'Fix_to_g[r024] = @@ -1005,7 +1005,7 @@ Proof. have r024_inv: r024^-1 = r042 by inv_tac. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g r024_inv !ffunE !permE /=. apply sym_equal; rewrite ?eqxx /= !andbT /col0/col1/col2/col3/col4/col5. -by do 4![case: eqPsym=> E; rewrite ?andbF // ?{}E]. +by do 4![case: eqVneq=> E; rewrite ?andbF // ?{}E]. Qed. Lemma F_r042 : 'Fix_to_g[r042] = @@ -1015,7 +1015,7 @@ Proof. have r042_inv: r042^-1 = r024 by inv_tac. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g r042_inv !ffunE !permE /=. apply sym_equal; rewrite ?eqxx /= !andbT /col0/col1/col2/col3/col4/col5. -by do 4![case: eqPsym=> E; rewrite ?andbF // ?{}E]. +by do 4![case: eqVneq=> E; rewrite ?andbF // ?{}E]. Qed. Lemma F_r012 : 'Fix_to_g[r012] = @@ -1025,7 +1025,7 @@ Proof. have r012_inv: r012^-1 = r021 by inv_tac. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g r012_inv !ffunE !permE /=. apply sym_equal; rewrite ?eqxx /= !andbT /col0/col1/col2/col3/col4/col5. -by do 4![case: eqPsym=> E; rewrite ?andbF // ?{}E]. +by do 4![case: eqVneq=> E; rewrite ?andbF // ?{}E]. Qed. Lemma F_r021 : 'Fix_to_g[r021] = @@ -1035,7 +1035,7 @@ Proof. have r021_inv: r021^-1 = r012 by inv_tac. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g r021_inv !ffunE !permE /=. apply sym_equal; rewrite ?eqxx /= !andbT /col0/col1/col2/col3/col4/col5. -do 4![case: eqPsym=> E; rewrite ?andbF // ?{}E]. +do 4![case: eqVneq=> E; rewrite ?andbF // ?{}E]. Qed. Lemma F_r031 : 'Fix_to_g[r031] = @@ -1045,7 +1045,7 @@ Proof. have r031_inv: r031^-1 = r013 by inv_tac. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g r031_inv !ffunE !permE /=. apply sym_equal; rewrite ?eqxx /= !andbT /col0/col1/col2/col3/col4/col5. -by do 4![case: eqPsym=> E; rewrite ?andbF // ?{}E]. +by do 4![case: eqVneq=> E; rewrite ?andbF // ?{}E]. Qed. Lemma F_r013 : 'Fix_to_g[r013] = @@ -1055,7 +1055,7 @@ Proof. have r013_inv: r013^-1 = r031 by inv_tac. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g r013_inv !ffunE !permE /=. apply sym_equal; rewrite ?eqxx /= !andbT /col0/col1/col2/col3/col4/col5. -by do 4![case: eqPsym=> E; rewrite ?andbF // ?{}E]. +by do 4![case: eqVneq=> E; rewrite ?andbF // ?{}E]. Qed. Lemma F_r043 : 'Fix_to_g[r043] = @@ -1065,7 +1065,7 @@ Proof. have r043_inv: r043^-1 = r034 by inv_tac. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g r043_inv !ffunE !permE /=. apply sym_equal; rewrite ?eqxx /= !andbT /col0/col1/col2/col3/col4/col5. -by do 4![case: eqPsym=> E; rewrite ?andbF // ?{}E]. +by do 4![case: eqVneq=> E; rewrite ?andbF // ?{}E]. Qed. Lemma F_r034 : 'Fix_to_g[r034] = @@ -1075,7 +1075,7 @@ Proof. have r034_inv: r034^-1 = r043 by inv_tac. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g r034_inv !ffunE !permE /=. apply sym_equal; rewrite ?eqxx /= !andbT /col0/col1/col2/col3/col4/col5. -by do 4![case: eqPsym=> E; rewrite ?andbF // ?{}E]. +by do 4![case: eqVneq=> E; rewrite ?andbF // ?{}E]. Qed. Lemma F_s1 : 'Fix_to_g[s1] = @@ -1084,7 +1084,7 @@ Proof. have s1_inv: s1^-1 = s1 by inv_tac. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g s1_inv !ffunE !permE /=. apply sym_equal; rewrite ?eqxx /= !andbT /col0/col1/col2/col3/col4/col5. -by do 3![case: eqPsym=> E; rewrite ?andbF // ?{}E]. +by do 3![case: eqVneq=> E; rewrite ?andbF // ?{}E]. Qed. Lemma F_s2 : 'Fix_to_g[s2] = @@ -1093,7 +1093,7 @@ Proof. have s2_inv: s2^-1 = s2 by inv_tac. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g s2_inv !ffunE !permE /=. apply sym_equal; rewrite ?eqxx /= !andbT /col0/col1/col2/col3/col4/col5. -by do 3![case: eqPsym=> E; rewrite ?andbF // ?{}E]. +by do 3![case: eqVneq=> E; rewrite ?andbF // ?{}E]. Qed. Lemma F_s3 : 'Fix_to_g[s3] = @@ -1102,7 +1102,7 @@ Proof. have s3_inv: s3^-1 = s3 by inv_tac. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g s3_inv !ffunE !permE /=. apply sym_equal; rewrite ?eqxx /= !andbT /col0/col1/col2/col3/col4/col5. -by do 3![case: eqPsym=> E; rewrite ?andbF // ?{}E]. +by do 3![case: eqVneq=> E; rewrite ?andbF // ?{}E]. Qed. Lemma F_s4 : 'Fix_to_g[s4] = @@ -1111,7 +1111,7 @@ Proof. have s4_inv: s4^-1 = s4 by inv_tac. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g s4_inv !ffunE !permE /=. apply sym_equal; rewrite ?eqxx /= !andbT /col0/col1/col2/col3/col4/col5. -by do 3![case: eqPsym=> E; rewrite ?andbF // ?{}E]. +by do 3![case: eqVneq=> E; rewrite ?andbF // ?{}E]. Qed. Lemma F_s5 : 'Fix_to_g[s5] = @@ -1120,7 +1120,7 @@ Proof. have s5_inv: s5^-1 = s5 by inv_tac. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g s5_inv !ffunE !permE /=. apply sym_equal; rewrite ?eqxx /= !andbT /col0/col1/col2/col3/col4/col5. -by do 3![case: eqPsym=> E; rewrite ?andbF // ?{}E]. +by do 3![case: eqVneq=> E; rewrite ?andbF // ?{}E]. Qed. Lemma F_s6 : 'Fix_to_g[s6] = @@ -1129,7 +1129,7 @@ Proof. have s6_inv: s6^-1 = s6 by inv_tac. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g s6_inv !ffunE !permE /=. apply sym_equal; rewrite ?eqxx /= !andbT /col0/col1/col2/col3/col4/col5. -by do 3![case: eqPsym=> E; rewrite ?andbF // ?{}E]. +by do 3![case: eqVneq=> E; rewrite ?andbF // ?{}E]. Qed. Lemma uniq4_uniq6 : forall x y z t : cube, diff --git a/mathcomp/solvable/extraspecial.v b/mathcomp/solvable/extraspecial.v index aa3ebed..0aacd7c 100644 --- a/mathcomp/solvable/extraspecial.v +++ b/mathcomp/solvable/extraspecial.v @@ -340,7 +340,7 @@ have ntY: Y != 1 by apply: subG1_contra ntZ. have p_odd: odd p by rewrite -oZ (oddSg sZG). have expY: exponent Y %| p by rewrite exponent_Ohm1_class2 // nil_class2 defG'. rewrite (prime_nt_dvdP p_pr _ expY) -?dvdn1 -?trivg_exponent //. -have [-> | neYG] := eqVneq Y G; first by rewrite indexgg dvd1n eqxx; split. +have [-> | neYG] := eqVneq Y G; first by rewrite indexgg dvd1n; split. have sG1Z: 'Mho^1(G) \subset Z by rewrite -defPhiG (Phi_joing pG) joing_subr. have Z_Gp: {in G, forall x, x ^+ p \in Z}. by move=> x Gx; rewrite /= (subsetP sG1Z) ?(Mho_p_elt 1) ?(mem_p_elt pG). diff --git a/mathcomp/solvable/maximal.v b/mathcomp/solvable/maximal.v index f3d79fc..0dfb4d1 100644 --- a/mathcomp/solvable/maximal.v +++ b/mathcomp/solvable/maximal.v @@ -1642,4 +1642,4 @@ Qed. End SCN. -Arguments SCN_P {gT G A}.
\ No newline at end of file +Arguments SCN_P {gT G A}. diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v index 75a04ef..e4e0003 100644 --- a/mathcomp/ssreflect/eqtype.v +++ b/mathcomp/ssreflect/eqtype.v @@ -196,14 +196,14 @@ Proof. exact/eqP/eqP. Qed. Hint Resolve eq_refl eq_sym : core. -Variant eq_xor_neq_sym (T : eqType) (x y : T) : bool -> bool -> Set := - | EqNotNeqSym of x = y : eq_xor_neq_sym x y true true - | NeqNotEqSym of x != y : eq_xor_neq_sym x y false false. +Variant eq_xor_neq (T : eqType) (x y : T) : bool -> bool -> Set := + | EqNotNeq of x = y : eq_xor_neq x y true true + | NeqNotEq of x != y : eq_xor_neq x y false false. -Lemma eqPsym (T : eqType) (x y : T) : eq_xor_neq_sym x y (y == x) (x == y). +Lemma eqVneq (T : eqType) (x y : T) : eq_xor_neq x y (y == x) (x == y). Proof. by rewrite eq_sym; case: eqP=> [|/eqP]; constructor. Qed. -Arguments eqPsym {T x y}. +Arguments eqVneq {T} x y, {T x y}. Section Contrapositives. @@ -379,9 +379,6 @@ Proof. by move->; rewrite eqxx. Qed. Lemma predU1r : b -> (x == y) || b. Proof. by move->; rewrite orbT. Qed. -Lemma eqVneq : {x = y} + {x != y}. -Proof. by case: eqP; [left | right]. Qed. - End EqPred. Arguments predU1P {T x y b}. diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v index 204843a..c01fb39 100644 --- a/mathcomp/ssreflect/finset.v +++ b/mathcomp/ssreflect/finset.v @@ -232,14 +232,16 @@ Definition setTfor (phT : phant T) := [set x : T | true]. Lemma in_setT x : x \in setTfor (Phant T). Proof. by rewrite in_set. Qed. -Lemma eqsVneq A B : {A = B} + {A != B}. -Proof. exact: eqVneq. Qed. +Lemma eqsVneq A B : eq_xor_neq A B (B == A) (A == B). +Proof. by apply: eqVneq. Qed. Lemma eq_finset (pA pB : pred T) : pA =1 pB -> finset pA = finset pB. Proof. by move=> eq_p; apply/setP => x; rewrite !(in_set, inE) eq_p. Qed. End BasicSetTheory. +Arguments eqsVneq {T} A B, {T A B}. + Definition inE := (in_set, inE). Arguments set0 {T}. diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index 2ed0ee1..9581a95 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -1191,7 +1191,7 @@ Proof. by rewrite -has_pred1 has_count -eqn0Ngt; apply: eqP. Qed. Lemma count_uniq_mem s x : uniq s -> count_mem x s = (x \in s). Proof. elim: s => //= y s IHs /andP[/negbTE s'y /IHs-> {IHs}]. -by rewrite in_cons; case: eqPsym => // <-; rewrite s'y. +by rewrite in_cons; case: eqVneq => // <-; rewrite s'y. Qed. Lemma filter_pred1_uniq s x : uniq s -> x \in s -> filter (pred1 x) s = [:: x]. @@ -1303,7 +1303,7 @@ Lemma rot_to s x : x \in s -> rot_to_spec s x. Proof. move=> s_x; pose i := index x s; exists i (drop i.+1 s ++ take i s). rewrite -cat_cons {}/i; congr cat; elim: s s_x => //= y s IHs. -by rewrite in_cons; case: eqPsym => // -> _; rewrite drop0. +by rewrite in_cons; case: eqVneq => // -> _; rewrite drop0. Qed. End EqSeq. @@ -2167,7 +2167,7 @@ Lemma nth_index_map s x0 x : {in s &, injective f} -> x \in s -> nth x0 s (index (f x) (map f s)) = x. Proof. elim: s => //= y s IHs inj_f s_x; rewrite (inj_in_eq inj_f) ?mem_head //. -move: s_x; rewrite inE; case: eqPsym => [-> | _] //=; apply: IHs. +move: s_x; rewrite inE; case: eqVneq => [-> | _] //=; apply: IHs. by apply: sub_in2 inj_f => z; apply: predU1r. Qed. |