Merge pull request #601 from pi8027/sorting_in

Add `_in` variants of the sorting lemmas

1 files changed, 16 insertions, 0 deletions

diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v
index a0a0548..48a59ee 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/mathcomp/ssreflect/seq.v
@@ -1500,6 +1500,16 @@ Arguments count_memPn {T x s}.
 Arguments uniqPn {T} x0 {s}.
 Arguments uniqP {T} x0 {s}.
 
+(* Since both `all (mem s) s` and `all (pred_of_seq s) s` may appear in       *)
+(* goals, the following hint has to be declared using the `Hint Extern`       *)
+(* command. Additionally, `mem` and `pred_of_seq` in the above terms do not   *)
+(* reduce to each other; thus, stating `allss` in the form of one of them     *)
+(* makes `apply: allss` failing for the other case. Since both `mem` and      *)
+(* `pred_of_seq` reduce to `mem_seq`, the following explicit type annotation  *)
+(* for `allss` makes it work for both cases.                                  *)
+Hint Extern 0 (is_true (all _ _)) =>
+  apply: (allss : forall T s, all (mem_seq s) s) : core.
+
 Section NthTheory.
 
 Lemma nthP (T : eqType) (s : seq T) x x0 :
@@ -2385,6 +2395,12 @@ 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) | s = map sval s'}.
+Proof.
+elim: s => /= [_|x s ihs /andP [ax /ihs [s' ->]]]; first by exists [::].
+by exists (exist a x ax :: s').
+Qed.
+
 Section MiscMask.
 
 Lemma leq_count_mask T (P : {pred T}) m s : count P (mask m s) <= count P s.