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:47:42 +01:00
parent b94a556f7e
commit 0f3f602c0d
1 changed files with 17 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
src/subsequences.v
View File

@ -813,3 +813,20 @@ Proof.
assumption. assumption.
Qed.
Theorem subsequence_not_in {X: Type} :
forall (u v: list X) a, subsequence u v -> ~ In a u -> ~ In a v.
Proof.
intros u v. generalize u. induction v; intros u0 a0; intros H I.
easy. apply not_in_cons. split. apply subsequence_incl in H.
apply incl_cons_inv in H. destruct H.
assert (forall z (x y: X), In x z -> ~ In y z -> x <> y).
intro z. induction z; intros x y; intros J K. inversion J.
apply in_inv in J. destruct J. rewrite <- H1.
apply not_in_cons in K. destruct K. apply not_eq_sym. assumption.
apply IHz. assumption.
apply not_in_cons in K. destruct K. assumption. apply not_eq_sym.
generalize I. generalize H. apply H1. generalize I. apply IHv.
apply subsequence_cons_r in H. assumption.
Qed.