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:34:02 +01:00
parent ea396978db
commit 6a56e61513
1 changed files with 14 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

19
src/subsequences.v
View File

@ -833,16 +833,25 @@ Proof.
Qed. Qed.
Theorem subsequence_partition {X: Type} : Theorem subsequence_as_filter {X: Type} :
forall (u v: list X), forall (u v: list X),
(exists f, v = fst (partition f u)) -> subsequence u v . (exists f, v = filter f u) -> subsequence u v.
Proof. Proof.
intros u v. intro H. destruct H. intros u v; intro H. destruct H. rewrite H.
apply subsequence_eq_def_3. apply subsequence_eq_def_2. apply subsequence_eq_def_3. apply subsequence_eq_def_2.
exists (map x u). split. apply map_length. rewrite H. exists (map x u). split. apply map_length.
rewrite partition_as_filter. simpl.
assert (L: forall g (w: list X), assert (L: forall g (w: list X),
filter g w = map snd (filter fst (combine (map g w) w))). filter g w = map snd (filter fst (combine (map g w) w))).
intros g w. induction w. reflexivity. simpl. destruct (g a). intros g w. induction w. reflexivity. simpl. destruct (g a).
simpl. rewrite IHw. reflexivity. assumption. apply L. simpl. rewrite IHw. reflexivity. assumption. apply L.
Qed. 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. rewrite H.
rewrite partition_as_filter. simpl. apply subsequence_as_filter.
exists x. reflexivity.
Qed.