baruchel/coqbooks
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Update

Browse Source
This commit is contained in:
Thomas Baruchel 2023-11-24 08:56:39 +01:00
parent c81e236fe3
commit 451c3b218a
1 changed files with 7 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
src/subsequences.v
View File

@ -844,9 +844,12 @@ Qed.
Theorem subsequence_as_partition {X: Type} :
forall (u: list X) f, subsequence u (fst (partition f u)).
forall (u v w: list X) f,
(v, w) = partition f u -> (subsequence u v) /\ (subsequence u w).
Proof.
intros u f.
rewrite partition_as_filter. simpl.
apply subsequence_as_filter with (f := f).
intros u v w f. intro H. rewrite partition_as_filter in H. split.
replace v with (fst (v, w)). rewrite H. simpl.
apply subsequence_as_filter. reflexivity.
replace w with (snd (v, w)). rewrite H. simpl.
apply subsequence_as_filter. reflexivity.
Qed.