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:39:38 +01:00
parent 6a56e61513
commit 5216516cff
1 changed files with 7 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
src/subsequences.v
View File

@ -834,12 +834,11 @@ Qed.
Theorem subsequence_as_filter {X: Type} :
forall (u v: list X),
(exists f, v = filter f u) -> subsequence u v.
forall (u v: list X) f, v = filter f u -> subsequence u v.
Proof.
intros u v; intro H. destruct H. rewrite H.
intros u v f; intro H. rewrite H.
apply subsequence_eq_def_3. apply subsequence_eq_def_2.
exists (map x u). split. apply map_length.
exists (map f u). split. apply map_length.
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).
@ -848,10 +847,9 @@ Qed.
Theorem subsequence_partition {X: Type} :
forall (u v: list X),
(exists f, v = fst (partition f u)) -> subsequence u v .
forall (u v: list X) 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.
intros u v f. intro H. rewrite H.
rewrite partition_as_filter. simpl.
apply subsequence_as_filter with (f := f). reflexivity.
Qed.