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 14:58:56 +01:00
parent cc4b168720
commit 4b4f52756f
1 changed files with 6 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
src/subsequences.v
View File

@ -585,15 +585,18 @@ Qed.
Theorem subsequence_double_cons {X: Type} : Theorem subsequence_double_cons {X: Type} :
forall (u v: list X) a, subsequence (a::u) (a::v) -> subsequence u v. forall (u v: list X) a, subsequence (a::u) (a::v) <-> subsequence u v.
Proof. Proof.
intros u v a. intro H. destruct H. destruct H. destruct H. intros u v a. split; intro H. destruct H. destruct H. destruct H.
destruct x; destruct x0. symmetry in H0. apply nil_cons in H0. destruct x; destruct x0. symmetry in H0. apply nil_cons in H0.
contradiction. inversion H0. contradiction. inversion H0.
exists l. exists x0. split. inversion H. reflexivity. reflexivity. exists l. exists x0. split. inversion H. reflexivity. reflexivity.
apply PeanoNat.Nat.neq_succ_0 in H. contradiction. apply PeanoNat.Nat.neq_succ_0 in H. contradiction.
inversion H0. exists (x1++x::l). exists x0. split. inversion H. inversion H0. exists (x1++x::l). exists x0. split. inversion H.
reflexivity. rewrite <- app_assoc. reflexivity. 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.
assumption.
Qed. Qed.
@ -617,7 +620,7 @@ Proof.
Qed. Qed.
Theorem subsequence_filter {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).
Proof. Proof.
@ -634,13 +637,6 @@ Proof.
apply subsequence_nil_r. simpl. destruct (f a). apply subsequence_nil_r. simpl. destruct (f a).
apply subsequence_cons_r. apply subsequence_cons_r.
Theorem subsequence_trans {X: Type} :
forall (l1 l2 l3: list X),
subsequence l1 l2 -> subsequence l2 l3 -> subsequence l1 l3.
Theorem subsequence_incl {X: Type} : Theorem subsequence_incl {X: Type} :
forall (u v: list X), subsequence u v -> incl v u. forall (u v: list X), subsequence u v -> incl v u.