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-01 19:09:31 +01:00
parent 30e9a21065
commit 995a822cae
1 changed files with 8 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
src/subsequences.v
View File

@ -337,11 +337,14 @@ Qed.
Various general properties of a subsequence.
*)
Theorem subsequence2_app {X: Type} :
Theorem subsequence_app {X: Type} :
forall l1 s1 l2 s2 : list X,
subsequence2 l1 s1 -> subsequence2 l2 s2 -> subsequence2 (l1++l2) (s1++s2).
subsequence l1 s1 -> subsequence l2 s2 -> subsequence (l1++l2) (s1++s2).
Proof.
intros l1 s1 l2 s2. intros H I.
apply subsequence_eq_def_3. apply subsequence_eq_def_2.
apply subsequence_eq_def_1 in H.
apply subsequence_eq_def_1 in I.
destruct H. destruct I. exists (x++x0). destruct H. destruct H0.
split. rewrite app_length. rewrite app_length.
rewrite H. rewrite H0. reflexivity.
@ -363,9 +366,11 @@ Qed.
Theorem subsequence_trans {X: Type} :
forall (l1 l2 l3: list X),
subsequence l1 l2 -> subsequence2 l2 l3 -> subsequence2 l1 l3.
subsequence l1 l2 -> subsequence l2 l3 -> subsequence l1 l3.
Proof.
intros l1 l2 l3. intros H I.
apply subsequence_eq_def_3. apply subsequence_eq_def_2.
apply subsequence_eq_def_1 in I.
destruct H. destruct H. destruct H. destruct I. destruct H1.
exists (
(repeat false (length x)) ++