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 16:27:04 +01:00
parent 58a834c275
commit 2315f2321e
1 changed files with 24 additions and 15 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

39
src/subsequences.v
View File

@ -712,6 +712,16 @@ Proof.
Qed. Qed.
Theorem subsequence_single {X: Type} :
forall (u: list X) a, In a u -> subsequence u [a].
Proof.
intro u. induction u; intro x; intro H. apply in_nil in H. contradiction.
destruct H. rewrite H. exists nil. exists [u]. split. reflexivity.
simpl. rewrite app_nil_r. reflexivity. apply subsequence_cons_l.
apply IHu. assumption.
Qed.
Theorem subsequence_filter_2 {X: Type} : Theorem subsequence_filter_2 {X: Type} :
forall (u v: list X) f, forall (u v: list X) f,
subsequence u v -> subsequence (filter f u) (filter f v). subsequence u v -> subsequence (filter f u) (filter f v).
@ -731,22 +741,21 @@ Proof.
assert (f a = true \/ f a = false). assert (f a = true \/ f a = false).
destruct (f a); [ left | right ]; reflexivity. destruct H0. destruct (f a); [ left | right ]; reflexivity. destruct H0.
simpl. rewrite H0. simpl. rewrite H0.
replace (a::v) with ([a] ++ v) in H. apply subsequence_split in H. replace (a::v) with ([a] ++ v) in H. apply subsequence_split_2 in H.
destruct H. destruct H. destruct H. destruct H1.
assert (subsequence ((filter f x) ++ (filter f x0))
((filter f [a]) ++ (filter f v))).
apply subsequence_app. simpl. rewrite H0.
destruct H. destruct H. destruct x0. destruct H. apply subsequence_incl in H1. apply incl_cons_inv in H1.
apply PeanoNat.Nat.neq_succ_0 in H. contradiction. destruct H1.
destruct H. simpl in H0. rewrite H0. assert (In a (filter f x)). apply filter_In. split; assumption.
apply subsequence_single. assumption. apply IHv. assumption.
rewrite <- filter_app in H3. rewrite <- H in H3. simpl in H3.
rewrite H0 in H3. assumption. reflexivity.
simpl. destruct (f a). simpl. rewrite H0. apply IHv. apply subsequence_cons_r in H.
assumption.
Qed.
apply subsequence_cons_r.