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 09:49:14 +01:00
parent 86bc880092
commit 85bda82049
1 changed files with 8 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

20
src/subsequences2.v
View File

@ -482,32 +482,28 @@ Proof.
Qed.
Theorem subsequence_incl {X: Type} :
forall (u v: list X), subsequence u v -> incl v u.
Theorem Subsequence_incl {X: Type} :
forall (u v: list X), Subsequence u v -> incl v u.
Proof.
intros u v. intro H. intro a. intro I.
generalize I. generalize H. generalize u.
induction v; intros u0; intros J K. inversion K.
destruct K. rewrite H0 in J.
apply subsequence_eq_def_1 in J.
apply subsequence_eq_def_2 in J.
destruct J. destruct H1. destruct H1. rewrite H1.
assert (J: forall (u v : list X) w, In w (u++w::v)).
intro u1. induction u1; intros v0 w. left. reflexivity.
right. apply IHu1. apply J. apply IHv.
apply subsequence_cons_r in H. assumption. assumption.
apply subsequence_cons_r in J. assumption. assumption.
apply Subsequence_cons_r in H. assumption. assumption.
apply Subsequence_cons_r in J. assumption. assumption.
Qed.
Theorem subsequence_split {X: Type} :
forall (u v w: list X),
subsequence (u++v) w