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-12-06 09:41:48 +01:00
parent 55180d7db3
commit 5212fb691f
1 changed files with 9 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

18
src/subsequences2.v
View File

@ -445,26 +445,26 @@ Proof.
Qed.
Theorem subsequence_double_cons {X: Type} :
forall (u v: list X) a, subsequence (a::u) (a::v) <-> subsequence u v.
Theorem Subsequence_double_cons {X: Type} :
forall (u v: list X) a, Subsequence (a::u) (a::v) <-> Subsequence u v.
Proof.
intros u v a. split; intro H. destruct H. destruct H. destruct H.
intros u v a. rewrite Subsequence_flat_map. rewrite Subsequence_flat_map.
split; intro H. destruct H. destruct H. destruct H.
destruct x; destruct x0. symmetry in H0. apply nil_cons in H0.
contradiction. inversion H0.
exists l. exists x0. split. inversion H. reflexivity. reflexivity.
apply PeanoNat.Nat.neq_succ_0 in H. contradiction.
inversion H0. exists (x1++x::l). exists x0. split. inversion H.
reflexivity. rewrite <- app_assoc. reflexivity.
apply subsequence_eq_def_3. exists nil. exists u.
split. reflexivity. apply subsequence_eq_def_2. apply subsequence_eq_def_1.
rewrite <- Subsequence_flat_map. exists nil. exists u.
split. reflexivity. apply Subsequence_flat_map.
assumption.
Qed.
Theorem subsequence_filter {X: Type} :
forall (u v: list X) f, subsequence (filter f u) v -> subsequence u v.
Proof.