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:45:41 +01:00
parent 5216516cff
commit c81e236fe3
1 changed files with 8 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

19
src/subsequences.v
View File

@ -834,22 +834,19 @@ Qed.
Theorem subsequence_as_filter {X: Type} :
forall (u v: list X) f, v = filter f u -> subsequence u v.
forall (u: list X) f, subsequence u (filter f u).
Proof.
intros u v f; intro H. rewrite H.
apply subsequence_eq_def_3. apply subsequence_eq_def_2.
intros u f. apply subsequence_eq_def_3. apply subsequence_eq_def_2.
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).
simpl. rewrite IHw. reflexivity. assumption. apply L.
induction u. reflexivity. simpl. destruct (f a).
simpl. rewrite IHu. reflexivity. assumption.
Qed.
Theorem subsequence_partition {X: Type} :
forall (u v: list X) f, v = fst (partition f u) -> subsequence u v .
Theorem subsequence_as_partition {X: Type} :
forall (u: list X) f, subsequence u (fst (partition f u)).
Proof.
intros u v f. intro H. rewrite H.
intros u f.
rewrite partition_as_filter. simpl.
apply subsequence_as_filter with (f := f). reflexivity.
apply subsequence_as_filter with (f := f).
Qed.