Add eqsP view to destruct not only x == y, but also y == x

7 files changed, 44 insertions, 28 deletions

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 30fcd0f..b466af5 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -5,6 +5,13 @@ Last releases: [[1.9.0] - 2019-05-22](#190---2019-05-22) and [[1.8.0] - 2019-04-
 
 The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 
+## [Unreleased]
+
+### Added
+
+- `eqsP`, a view which is like `eqP`, but in addition it allows
+  simultaneous destruction of expressions of the form `x == y` and `y == x`.
+
 ## [1.9.0] - 2019-05-22
 
 MathComp 1.9.0 is compatible with Coq 8.7, 8.8, 8.9 and 8.10beta1.
diff --git a/mathcomp/algebra/intdiv.v b/mathcomp/algebra/intdiv.v
index 48e9de8..77f8781 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 eq_sym; case: eqP => // ->.
+  by apply/matrixP=> i1 j1; rewrite !mxE; case: eqsP => // ->.
 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 d3142d6..91c7747 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 eq_sym; case: eqP => // ->. Qed.
+Proof. by apply/matrixP=> i j; rewrite !mxE; case: eqsP => // ->. 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 eq_sym; case: eqP => // ->. Qed.
+Proof. by apply/matrixP=> i j; rewrite !mxE; case: eqsP => // ->. 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/fingroup/perm.v b/mathcomp/fingroup/perm.v
index b610c36..c7eaf58 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 eq_sym; case: eqP.
+by rewrite add1n eqSS; case: eqsP.
 Qed.
 
 End LiftPerm.
diff --git a/mathcomp/solvable/burnside_app.v b/mathcomp/solvable/burnside_app.v
index b5d34a5..d6115dd 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![rewrite eq_sym; case E: {+}(_ == _); rewrite // {E}(eqP E)].
+by do 3![case: eqsP=> // <-].
 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![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF // {E}(eqP E)  ].
+by do 3![case: eqsP; 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![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF // {E}(eqP E) ].
+by do 3![case: eqsP; 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![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF  // {E}(eqP E)].
+by do 3![case: eqsP; 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![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF  // {E}(eqP E)].
+by do 3![case: eqsP; 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![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF  // {E}(eqP E)].
+by do 3![case: eqsP; 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![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF  // {E}(eqP E)].
+by do 3![case: eqsP; 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![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF  // ?{E}(eqP E)].
+by do 4![case: eqsP=> 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![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF  // ?{E}(eqP E)].
+by do 4![case: eqsP=> 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![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF  // ?{E}(eqP E)].
+by do 4![case: eqsP=> 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![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF  // ?{E}(eqP E)].
+do 4![case: eqsP=> 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![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF  // ?{E}(eqP E)].
+by do 4![case: eqsP=> 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![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF  // ?{E}(eqP E)].
+by do 4![case: eqsP=> 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![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF  // ?{E}(eqP E)].
+by do 4![case: eqsP=> 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![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF  // ?{E}(eqP E)].
+by do 4![case: eqsP=> 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![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF  // ?{E}(eqP E)].
+by do 3![case: eqsP=> 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![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF  // ?{E}(eqP E)].
+by do 3![case: eqsP=> 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![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF  // ?{E}(eqP E)].
+by do 3![case: eqsP=> 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![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF  // ?{E}(eqP E)].
+by do 3![case: eqsP=> 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![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF  // ?{E}(eqP E)].
+by do 3![case: eqsP=> 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![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF  // ?{E}(eqP E)].
+by do 3![case: eqsP=> E; rewrite ?andbF // ?{}E].
 Qed.
 
 Lemma uniq4_uniq6 : forall x y z t : cube,
diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v
index 3fbc110..895a86e 100644
--- a/mathcomp/ssreflect/eqtype.v
+++ b/mathcomp/ssreflect/eqtype.v
@@ -196,6 +196,15 @@ 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.
+
+Lemma eqsP (T : eqType) (x y : T) : eq_xor_neq_sym x y (y == x) (x == y).
+Proof. by rewrite eq_sym; case: eqP; constructor. Qed.
+
+Arguments eqsP {T x y}.
+
 Section Contrapositives.
 
 Variables (T1 T2 : eqType).
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v
index 00e0a27..516dc95 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 eq_sym; case: eqP => // ->; rewrite s'y.
+by rewrite in_cons; case: eqsP => // <-; 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 eq_sym in_cons; case: eqP => // -> _; rewrite drop0.
+by rewrite in_cons; case: eqsP => // -> _; 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 eq_sym; case: eqP => [-> | _] //=; apply: IHs.
+move: s_x; rewrite inE; case: eqsP => [-> | _] //=; apply: IHs.
 by apply: sub_in2 inj_f => z; apply: predU1r.
 Qed.