diff options
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/ssreflect/seq.v | 23 |
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. |