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-12-06 08:16:50 +01:00
parent 5db7822d3c
commit 2b0a214352
1 changed files with 12 additions and 15 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

27
src/subsequences2.v
View File

@ -198,23 +198,12 @@ Proof.
Qed.
Theorem subsequence_app {X: Type} :
Theorem Subsequence_app {X: Type} :
forall l1 s1 l2 s2 : list X,
subsequence l1 s1 -> subsequence l2 s2 -> subsequence (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.
intros l1 s1 l2 s2. intros H I. apply Subsequence_bools.
apply Subsequence_bools in H. apply Subsequence_bools 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.
@ -234,6 +223,14 @@ Proof.
Qed.
Theorem subsequence_trans {X: Type} :
forall (l1 l2 l3: list X),
subsequence l1 l2 -> subsequence l2 l3 -> subsequence l1 l3.