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-23 21:29:18 +01:00
parent 34a4a7f63b
commit b94a556f7e
1 changed files with 4 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
src/subsequences.v
View File

@ -586,9 +586,8 @@ 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.
intros u v. generalize u. induction v; intros u0 f; intro H.
apply subsequence_nil_r. 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.
@ -755,8 +754,8 @@ Qed.
Theorem subsequence_add {X: Type} :
forall (u v w: list X) x, subsequence u v -> Add x u w -> subsequence w v.
Proof.
intros u v w. generalize u v. induction w; intros u0 v0 x; intro H.
intro I. inversion I. intro I. inversion I.
intros u v w. generalize u v.
induction w; intros u0 v0 x; intros H I; inversion I.
rewrite <- H2. apply subsequence_cons_l. rewrite <- H3. assumption.
assert (J := H). apply subsequence_eq_def_1 in H. rewrite <- H1 in H.