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-22 15:50:05 +01:00
parent 57df938818
commit 9c7d6b156f
1 changed files with 15 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
src/subsequences.v
View File

@ -507,7 +507,7 @@ Proof.
contradiction H5. assumption. contradiction H5. assumption.
Qed. Qed.
Theorem subsequence_reverse {X: Type} : Theorem subsequence_rev {X: Type} :
forall (u v: list X), subsequence u v <-> subsequence (rev u) (rev v). forall (u v: list X), subsequence u v <-> subsequence (rev u) (rev v).
Proof. Proof.
assert (MAIN: forall (u v: list X), assert (MAIN: forall (u v: list X),
@ -546,6 +546,20 @@ Proof.
Qed. Qed.
Theorem subsequence_map {X Y: Type} :
forall (u v: list X) (f: X -> Y),
subsequence u v -> subsequence (map f u) (map f v).
intros u v. generalize u. induction v; intros u0 f.
intro. apply subsequence_nil_r. intro H.
apply subsequence_eq_def_3.
apply subsequence_eq_def_1 in H. apply subsequence_eq_def_2 in H.
destruct H. destruct H. destruct H.
exists (map f x). exists (map f x0). split.
rewrite <- map_cons. rewrite <- map_app. rewrite H. reflexivity.
apply subsequence_eq_def_2. apply subsequence_eq_def_1.
apply IHv. apply subsequence_eq_def_3. assumption.
Qed.