Apply suggestions from code review

Co-authored-by: Cyril Cohen <CohenCyril@users.noreply.github.com>

2 files changed, 30 insertions, 14 deletions

diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v
index 112f129..8ee8bea 100644
--- a/mathcomp/ssreflect/path.v
+++ b/mathcomp/ssreflect/path.v
@@ -1101,8 +1101,7 @@ Lemma merge_stable_path x s1 s2 :
   path leT_lex x (merge leT s1 s2).
 Proof.
 elim: s1 s2 x => //= x s1 ih1; elim => //= y s2 ih2 h.
-rewrite allrel_consl allrel_consr /= -andbA.
-move=> /and4P [xy' xs2 ys1 s1s2] /andP [hx xs1] /andP [hy ys2].
+rewrite allrel_cons2 => /and4P [xy' xs2 ys1 s1s2] /andP [hx xs1] /andP [hy ys2].
 case: ifP => xy /=; rewrite (hx, hy) /=.
 - by apply: ih1; rewrite ?allrel_consr ?ys1 //= xy xy' implybT.
 - by apply: ih2; have:= leT_total x y; rewrite ?allrel_consl ?xs2 ?xy //= => ->.
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v
index 777041f..9747f73 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/mathcomp/ssreflect/seq.v
@@ -3491,9 +3491,9 @@ Implicit Types (x : T) (y : S) (xs : seq T) (ys : seq S).
 
 Definition allrel xs ys := all [pred x | all (r x) ys] xs.
 
-Lemma allrel0s ys : allrel [::] ys. Proof. by []. Qed.
+Lemma allrel0l ys : allrel [::] ys. Proof. by []. Qed.
 
-Lemma allrels0 xs : allrel xs [::]. Proof. by elim: xs. Qed.
+Lemma allrel0r xs : allrel xs [::]. Proof. by elim: xs. Qed.
 
 Lemma allrel_consl x xs ys : allrel (x :: xs) ys = all (r x) ys && allrel xs ys.
 Proof. by []. Qed.
@@ -3502,10 +3502,15 @@ Lemma allrel_consr xs y ys :
   allrel xs (y :: ys) = all (r^~ y) xs && allrel xs ys.
 Proof. exact: all_predI. Qed.
 
-Lemma allrel1s x ys : allrel [:: x] ys = all (r x) ys. Proof. exact: andbT. Qed.
+Lemma allrel_cons2 x y xs ys :
+  allrel (x :: xs) (y :: ys) =
+  [&& r x y, all (r x) ys, all (r^~ y) xs & allrel xs ys].
+Proof. by rewrite /= allrel_consr -andbA. Qed.
 
-Lemma allrels1 xs y : allrel xs [:: y] = all (r^~ y) xs.
-Proof. by rewrite allrel_consr allrels0 andbT. Qed.
+Lemma allrel1l x ys : allrel [:: x] ys = all (r x) ys. Proof. exact: andbT. Qed.
+
+Lemma allrel1r xs y : allrel xs [:: y] = all (r^~ y) xs.
+Proof. by rewrite allrel_consr allrel0r andbT. Qed.
 
 Lemma allrel_catl xs xs' ys :
   allrel (xs ++ xs') ys = allrel xs ys && allrel xs' ys.
@@ -3514,7 +3519,7 @@ Proof. exact: all_cat. Qed.
 Lemma allrel_catr xs ys ys' :
   allrel xs (ys ++ ys') = allrel xs ys && allrel xs ys'.
 Proof.
-elim: ys => /= [|y ys ihys]; first by rewrite allrels0.
+elim: ys => /= [|y ys ihys]; first by rewrite allrel0r.
 by rewrite !allrel_consr ihys andbA.
 Qed.
 
@@ -3525,18 +3530,31 @@ Proof. by elim: xs => //= x xs ->; rewrite all_cat all_map. Qed.
 End AllRel.
 
 Arguments allrel {T S} r xs ys : simpl never.
-Arguments allrel0s {T S} r ys.
-Arguments allrels0 {T S} r xs.
+Arguments allrel0l {T S} r ys.
+Arguments allrel0r {T S} r xs.
 Arguments allrel_consl {T S} r x xs ys.
 Arguments allrel_consr {T S} r xs y ys.
-Arguments allrel1s {T S} r x ys.
-Arguments allrels1 {T S} r xs y.
+Arguments allrel1l {T S} r x ys.
+Arguments allrel1r {T S} r xs y.
 Arguments allrel_catl {T S} r xs xs' ys.
 Arguments allrel_catr {T S} r xs ys ys'.
 Arguments allrel_allpairsE {T S} r xs ys.
 
 Notation all1rel r xs := (allrel r xs xs).
 
+Lemma eq_in_allrel {T S : Type} (P : {pred T}) (Q : {pred S}) r r' :
+  {in P & Q, r =2 r'} ->
+  forall xs ys, all P xs -> all Q ys -> allrel r xs ys = allrel r' xs ys.
+Proof.
+move=> rr' + ys; elim=> //= x xs IH /andP [Px Pxs] Qys.
+congr andb => /=; last exact: IH.
+by elim: ys Qys {IH} => //= y ys IH /andP [Qy Qys]; rewrite rr' // IH.
+Qed.
+
+Lemma eq_allrel {T S : Type} (r r': T -> S -> bool) xs ys :
+  r =2 r' -> allrel r xs ys = allrel r' xs ys.
+Proof. by move=> rr'; apply/eq_in_allrel/all_predT/all_predT. Qed.
+
 Lemma allrelC {T S : Type} (r : T -> S -> bool) xs ys :
   allrel r xs ys = allrel (fun y => r^~ y) ys xs.
 Proof. by elim: xs => [|x xs ih]; [elim: ys | rewrite allrel_consr -ih]. Qed.
@@ -3568,8 +3586,7 @@ Proof. by rewrite /allrel /= rsym; do 3 case: r. Qed.
 Lemma all1rel_cons x xs :
   all1rel r (x :: xs) = [&& r x x, all (r x) xs & all1rel r xs].
 Proof.
-rewrite allrel_consl allrel_consr /= !andbA [r x x && _]andbC -andbA andbACA.
-rewrite -[RHS]andbA; congr andb; rewrite -all_predI.
+rewrite allrel_cons2; congr andb; rewrite andbA -all_predI; congr andb.
 by elim: xs => //= y xs ->; rewrite rsym andbb.
 Qed.