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:24:20 +01:00
parent cd232bf73a
commit ea396978db
1 changed files with 15 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
src/subsequences.v
View File

@ -831,3 +831,18 @@ Proof.
generalize I. generalize H. apply H1. generalize I. apply IHv.
apply subsequence_cons_r in H. assumption.
Qed.
Theorem subsequence_partition {X: Type} :
forall (u v: list X),
(exists f, v = fst (partition f u)) -> subsequence u v .
Proof.
intros u v. intro H. destruct H.
apply subsequence_eq_def_3. apply subsequence_eq_def_2.
exists (map x u). split. apply map_length. rewrite H.
rewrite partition_as_filter. simpl.
assert (L: forall g (w: list X),
filter g w = map snd (filter fst (combine (map g w) w))).
intros g w. induction w. reflexivity. simpl. destruct (g a).
simpl. rewrite IHw. reflexivity. assumption. apply L.
Qed.