Update
This commit is contained in:
parent
5e73d31a1e
commit
9f5c7bdc32
@ -361,6 +361,36 @@ Qed.
|
|||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
Theorem subsequence2_app {X: Type} :
|
||||||
|
forall l1 s1 l2 s2 : list X,
|
||||||
|
subsequence2 l1 s1 -> subsequence2 l2 s2 -> subsequence2 (l1++l2) (s1++s2).
|
||||||
|
Proof.
|
||||||
|
intros l1 s1 l2 s2. intros H I.
|
||||||
|
destruct H. destruct I. exists (x++x0). destruct H. destruct H0.
|
||||||
|
split. rewrite app_length. rewrite app_length.
|
||||||
|
rewrite H. rewrite H0. reflexivity.
|
||||||
|
rewrite H1. rewrite H2.
|
||||||
|
|
||||||
|
assert (J: forall (t : list bool) (u : list X) (v: list bool) (w : list X),
|
||||||
|
length t = length u
|
||||||
|
-> combine (t++v) (u++w) = (combine t u) ++ (combine v w)).
|
||||||
|
intros t u v w. generalize u. induction t; intro u0; intro K.
|
||||||
|
replace u0 with (nil : list X). reflexivity.
|
||||||
|
destruct u0. reflexivity. apply O_S in K. contradiction K.
|
||||||
|
destruct u0. symmetry in K. apply O_S in K. contradiction K.
|
||||||
|
simpl. rewrite IHt. reflexivity. inversion K. reflexivity.
|
||||||
|
|
||||||
|
rewrite J. rewrite filter_app. rewrite map_app. reflexivity.
|
||||||
|
assumption.
|
||||||
|
Qed.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
Example test1: subsequence [1;2;3;4;5] [1;3;5].
|
Example test1: subsequence [1;2;3;4;5] [1;3;5].
|
||||||
Proof.
|
Proof.
|
||||||
unfold subsequence.
|
unfold subsequence.
|
||||||
|
Loading…
Reference in New Issue
Block a user