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:49:53 +01:00
parent daabce4917
commit 35672797f1
1 changed files with 14 additions and 14 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

28
src/subsequences.v
View File

@ -530,6 +530,20 @@ Proof.
Qed.
Theorem subsequence_in {X: Type} :
forall (u: list X) a, In a u <-> subsequence u [a].
Proof.
intros u a. split.
induction u; 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.
intro H. destruct H. destruct H. destruct H. rewrite H0. apply in_or_app.
right. destruct x0. apply PeanoNat.Nat.neq_succ_0 in H. contradiction.
left. reflexivity.
Qed.
Theorem subsequence_rev {X: Type} :
forall (u v: list X), subsequence u v <-> subsequence (rev u) (rev v).
Proof.
@ -712,20 +726,6 @@ Proof.
Qed.
Theorem subsequence_in {X: Type} :
forall (u: list X) a, In a u <-> subsequence u [a].
Proof.
intros u a. split.
induction u; 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.
intro H. destruct H. destruct H. destruct H. rewrite H0. apply in_or_app.
right. destruct x0. apply PeanoNat.Nat.neq_succ_0 in H. contradiction.
left. reflexivity.
Qed.
Theorem subsequence_filter_2 {X: Type} :
forall (u v: list X) f,
subsequence u v -> subsequence (filter f u) (filter f v).