factoring out in_sig

3 files changed, 60 insertions, 21 deletions

diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v
index 2d2182b..f4ecfbb 100644
--- a/mathcomp/ssreflect/path.v
+++ b/mathcomp/ssreflect/path.v
@@ -882,21 +882,20 @@ Arguments sort_map {T T' f leT}.
 Section SortSeq_in.
 
 Variables (T : Type) (P : {pred T}) (leT : rel T).
+Notation le_sT := (relpre (val : sig P -> _) leT).
 
 Hypothesis leT_total : {in P &, total leT}.
+Let le_sT_total : total le_sT := in2_sig leT_total.
 
 Lemma sort_sorted_in s : all P s -> sorted leT (sort leT s).
-Proof.
-move=> /all_sigP [{}s <-]; rewrite sort_map sorted_map.
-by apply: sort_sorted; move=> [x Px] [y Py]; apply: leT_total.
-Qed.
+Proof. by move=> /all_sigP[? ->]; rewrite sort_map sorted_map sort_sorted. Qed.
 
 Hypothesis leT_tr : {in P & &, transitive leT}.
+Let le_sT_tr : transitive le_sT := in3_sig leT_tr.
 
 Lemma sorted_sort_in s : all P s -> sorted leT s -> sort leT s = s.
 Proof.
-move=> /all_sigP [{}s <-]; rewrite sort_map sorted_map.
-by move=> /sorted_sort -> // [x Px] [y Py] [z Pz]; apply: leT_tr.
+by move=> /all_sigP [{}s ->]; rewrite sort_map sorted_map => /sorted_sort->.
 Qed.
 
 End SortSeq_in.
@@ -1099,19 +1098,16 @@ Lemma sort_stable_in T (P : {pred T}) (leT leT' : rel T) :
   forall s : seq T, all P s -> sorted leT' s ->
   sorted [rel x y | leT x y && (leT y x ==> leT' x y)] (sort leT s).
 Proof.
-move=> leT_total leT_tr _ /all_sigP [s <-]; rewrite sort_map !sorted_map.
-apply: sort_stable; first by move=> [x Px] [y Py]; apply: leT_total.
-by move=> [x Px] [y Py] [z Pz]; apply: leT_tr.
+move=> /in2_sig leT_total /in3_sig leT_tr _ /all_sigP[s ->].
+by rewrite sort_map !sorted_map; apply: sort_stable.
 Qed.
 
 Lemma filter_sort_in T (P : {pred T}) (leT : rel T) :
   {in P &, total leT} -> {in P & &, transitive leT} ->
   forall p s, all P s -> filter p (sort leT s) = sort leT (filter p s).
 Proof.
-move=> leT_total leT_tr p _ /all_sigP [s <-].
-rewrite !(sort_map, filter_map) filter_sort //.
-  by move=> [x Px] [y Py]; apply: leT_total.
-by move=> [x Px] [y Py] [z Pz]; apply: leT_tr.
+move=> /in2_sig leT_total /in3_sig leT_tr p _ /all_sigP[s ->].
+by rewrite !(sort_map, filter_map) filter_sort.
 Qed.
 
 Section Stability_mask.
@@ -1142,20 +1138,21 @@ Variables (T : Type) (P : {pred T}) (leT : rel T).
 Hypothesis leT_total : {in P &, total leT}.
 Hypothesis leT_tr : {in P & &, transitive leT}.
 
+Notation le_sT := (relpre (val : sig P -> _) leT).
+Let le_sT_total : total le_sT := in2_sig leT_total.
+Let le_sT_tr : transitive le_sT := in3_sig leT_tr.
+
 Lemma mask_sort_in s m :
   all P s -> {m_s : bitseq | mask m_s (sort leT s) = sort leT (mask m s)}.
 Proof.
-move=> /all_sigP [{}s <-]; case: (mask_sort (leT := relpre sval leT) _ _ s m).
-- by move=> [x Px] [y Py]; apply: leT_total.
-- by move=> [x Px] [y Py] [z Pz]; apply: leT_tr.
-- by move=> m' m'E; exists m'; rewrite -map_mask !sort_map -map_mask m'E.
+move=> /all_sigP [{}s ->]; case: (mask_sort (leT := le_sT) _ _ s m) => //.
+by move=> m' m'E; exists m'; rewrite -map_mask !sort_map -map_mask m'E.
 Qed.
 
 Lemma sorted_mask_sort_in s m :
   all P s -> sorted leT (mask m s) -> {m_s | mask m_s (sort leT s) = mask m s}.
 Proof.
-move=> ? /(sorted_sort_in leT_tr _) <-; last exact: all_mask.
-exact: mask_sort_in.
+move=> ? /(sorted_sort_in leT_tr _) <-; [exact: mask_sort_in | exact: all_mask].
 Qed.
 
 End Stability_mask_in.
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v
index fab3fa9..999ec0a 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/mathcomp/ssreflect/seq.v
@@ -2385,9 +2385,9 @@ Notation "[ 'seq' E : R | i : T <- s & C ]" :=
 Lemma filter_mask T a (s : seq T) : filter a s = mask (map a s) s.
 Proof. by elim: s => //= x s <-; case: (a x). Qed.
 
-Lemma all_sigP T a (s : seq T) : all a s -> {s' : seq (sig a) | map sval s' = s}.
+Lemma all_sigP T a (s : seq T) : all a s -> {s' : seq (sig a) | s = map sval s'}.
 Proof.
-elim: s => /= [_|x s ihs /andP [ax /ihs [s' <-]]]; first by exists [::].
+elim: s => /= [_|x s ihs /andP [ax /ihs [s' ->]]]; first by exists [::].
 by exists (exist a x ax :: s').
 Qed.
 
diff --git a/mathcomp/ssreflect/ssrbool.v b/mathcomp/ssreflect/ssrbool.v
index 48f0262..1864b53 100644
--- a/mathcomp/ssreflect/ssrbool.v
+++ b/mathcomp/ssreflect/ssrbool.v
@@ -349,3 +349,45 @@ Proof. by case: b => // /(_ isT). Qed.
 Lemma contra_notF P b : (b -> P) -> ~ P -> b = false.
 Proof. by case: b => // /(_ isT). Qed.
 End Contra.
+
+(******************)
+(* v8.14 addtions *)
+(******************)
+
+Section in_sig.
+Local Notation "{ 'all1' P }" := (forall x, P x : Prop) (at level 0).
+Local Notation "{ 'all2' P }" := (forall x y, P x y : Prop) (at level 0).
+Local Notation "{ 'all3' P }" := (forall x y z, P x y z : Prop) (at level 0).
+
+Variables T1 T2 T3 : Type.
+Variables (D1 : {pred T1}) (D2 : {pred T2})  (D3 : {pred T3}).
+Variable P1 : T1 -> Prop.
+Variable P11 : T1 -> T2 -> Prop.
+Variable P111 : T1 -> T2 -> T3 -> Prop.
+Variable P2 :  T1 -> T1 -> Prop.
+Variable P3 :  T1 -> T1 -> T1 -> Prop.
+
+Lemma in1_sig : {in D1, {all1 P1}} -> forall x : sig D1, P1 (sval x).
+Proof. by move=> DP [x Dx]; have := DP _ Dx. Qed.
+
+Lemma in11_sig : {in D1 & D2, {all2 P11}} ->
+  forall (x : sig D1) (y : sig D2), P11 (sval x) (sval y).
+Proof. by move=> DP [x Dx] [y Dy]; have := DP _ _ Dx Dy. Qed.
+
+Lemma in111_sig : {in D1 & D2 & D3, {all3 P111}} ->
+  forall (x : sig D1) (y : sig D2) (z : sig D3), P111 (sval x) (sval y) (sval z).
+Proof. by move=> DP [x Dx] [y Dy] [z Dz]; have := DP _ _ _ Dx Dy Dz. Qed.
+
+Lemma in2_sig : {in D1 &, {all2 P2}} -> forall x y : sig D1, P2 (sval x) (sval y).
+Proof. by move=> DP [x Dx] [y Dy]; have := DP _ _ Dx Dy. Qed.
+
+Lemma in3_sig : {in D1 & &, {all3 P3}} ->
+   forall x y z : sig D1, P3 (sval x) (sval y) (sval z).
+Proof. by move=> DP [x Dx] [y Dy] [z Dz]; have := DP _ _ _ Dx Dy Dz. Qed.
+
+End in_sig.
+Arguments in1_sig {T1 D1 P1}.
+Arguments in11_sig {T1 T2 D1 D2 P11}.
+Arguments in111_sig {T1 T2 T3 D1 D2 D3 P111}.
+Arguments in2_sig {T1 D1 P2}.
+Arguments in3_sig {T1 D1 P3}.