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:10:15 +01:00
parent 5158370a77
commit 98162d1052
1 changed files with 29 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

29
src/subsequences.v
View File

@ -773,3 +773,32 @@ Proof.
inversion H. split; reflexivity. assumption.
Qed.
Theorem subsequence_nodup {X: Type} :
forall (u v: list X), subsequence u v -> NoDup u -> NoDup v.
Proof.
intros u v. intros H I. apply subsequence_eq_def_1 in H.
destruct H. destruct H. rewrite H0.
assert (J: forall z (q: list X),
NoDup q -> NoDup (map snd (filter fst (combine z q)))).
intro z. induction z; intro q; intro J. apply NoDup_nil.
destruct q. rewrite combine_nil. apply NoDup_nil.
destruct a. simpl. rewrite NoDup_cons_iff in J. destruct J.
apply IHz in H2.
apply NoDup_cons.
assert (K: forall (q: list X) g h,
~ In g q -> ~ In g (map snd (filter fst (combine h q)))).
intro q0. induction q0; intros g h; intro J.
rewrite combine_nil. easy. destruct h. easy. destruct b.
replace (map snd (filter fst (combine (true :: h) (a :: q0))))
with (a::(map snd (filter fst (combine h q0)))).
rewrite not_in_cons. split;
rewrite not_in_cons in J; destruct J. assumption. apply IHq0.
assumption. reflexivity. apply IHq0.
rewrite not_in_cons in J; destruct J. assumption. apply K. assumption.
assumption. simpl. apply IHz.
rewrite NoDup_cons_iff in J. destruct J. assumption. apply J.
assumption.
Qed.