Theorems about find and index

1 files changed, 23 insertions, 0 deletions

diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v
index 5b9d047..37fe1e6 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/mathcomp/ssreflect/seq.v
@@ -530,6 +530,9 @@ Proof. by elim: s => //= x s IHs; case a_x: (a x). Qed.
 Lemma before_find s i : i < find s -> a (nth s i) = false.
 Proof. by elim: s i => //= x s IHs; case: ifP => // a'x [|i] // /(IHs i). Qed.
 
+Lemma hasNfind s : ~~ has s -> find s = size s.
+Proof. by rewrite has_find; case: ltngtP (find_size s). Qed.
+
 Lemma filter_cat s1 s2 : filter (s1 ++ s2) = filter s1 ++ filter s2.
 Proof. by elim: s1 => //= x s1 ->; case (a x). Qed.
 
@@ -929,6 +932,23 @@ Proof.
 by move=> Pnil Pcons; elim=> [|x s IHs] [|y t] //= [eq_sz]; apply/Pcons/IHs.
 Qed.
 
+Section FindSpec.
+Variable (T : Type) (a : {pred T}) (s : seq T).
+
+Variant find_spec : bool -> nat -> Type :=
+| NotFound of ~~ has a s : find_spec false (size s)
+| Found (i : nat) of i < size s & (forall x0, a (nth x0 s i)) &
+  (forall x0 j, j < i -> a (nth x0 s j) = false) : find_spec true i.
+
+Lemma findP : find_spec (has a s) (find a s).
+Proof.
+have [a_s|aNs] := boolP (has a s); last by rewrite hasNfind//; constructor.
+by constructor=> [|x0|x0]; rewrite -?has_find ?nth_find//; apply: before_find.
+Qed.
+
+End FindSpec.
+Arguments findP {T}.
+
 Section RotRcons.
 
 Variable T : Type.
@@ -1304,6 +1324,9 @@ Proof. by rewrite /index find_size. Qed.
 Lemma index_mem x s : (index x s < size s) = (x \in s).
 Proof. by rewrite -has_pred1 has_find. Qed.
 
+Lemma memNindex x s :  x \notin s -> index x s = size s.
+Proof. by rewrite -has_pred1 => /hasNfind. Qed.
+
 Lemma nth_index x s : x \in s -> nth s (index x s) = x.
 Proof. by rewrite -has_pred1 => /(nth_find x0)/eqP. Qed.