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:22:58 +01:00
parent 98162d1052
commit 34a4a7f63b
1 changed files with 14 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
src/subsequences.v
View File

@ -785,8 +785,7 @@ Proof.
intro z. induction z; intro q; intro J. apply NoDup_nil. intro z. induction z; intro q; intro J. apply NoDup_nil.
destruct q. rewrite combine_nil. apply NoDup_nil. destruct q. rewrite combine_nil. apply NoDup_nil.
destruct a. simpl. rewrite NoDup_cons_iff in J. destruct J. destruct a. simpl. rewrite NoDup_cons_iff in J. destruct J.
apply IHz in H2. apply IHz in H2. apply NoDup_cons.
apply NoDup_cons.
assert (K: forall (q: list X) g h, assert (K: forall (q: list X) g h,
~ In g q -> ~ In g (map snd (filter fst (combine h q)))). ~ In g q -> ~ In g (map snd (filter fst (combine h q)))).
@ -802,3 +801,16 @@ Proof.
rewrite NoDup_cons_iff in J. destruct J. assumption. apply J. rewrite NoDup_cons_iff in J. destruct J. assumption. apply J.
assumption. assumption.
Qed. Qed.
Theorem subsequence_in_2 {X: Type} :
forall (u v: list X) a, subsequence u v -> In a v -> In a u.
Proof.
intros u v. generalize u. induction v; intros u0 a0; intros H I.
contradiction I. destruct I.
apply subsequence_eq_def_1 in H. apply subsequence_eq_def_2 in H.
destruct H. destruct H. destruct H. rewrite H. rewrite H0.
apply in_elt. apply IHv. apply subsequence_cons_r in H.
assumption. assumption.
Qed.