From 86bc88009295fd6ec7ea50c4842f1ea787ed440c Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Wed, 6 Dec 2023 09:48:08 +0100 Subject: [PATCH] Update --- src/subsequences2.v | 29 ++++++++++++++++------------- 1 file changed, 16 insertions(+), 13 deletions(-) diff --git a/src/subsequences2.v b/src/subsequences2.v index 794da94..757b204 100644 --- a/src/subsequences2.v +++ b/src/subsequences2.v @@ -462,29 +462,32 @@ Proof. Qed. - - - -Theorem subsequence_filter {X: Type} : - forall (u v: list X) f, subsequence (filter f u) v -> subsequence u v. +Theorem Subsequence_filter {X: Type} : + forall (u v: list X) f, Subsequence (filter f u) v -> Subsequence u v. Proof. intro u. induction u; intros v f; intro H. assumption. simpl in H. destruct (f a). assert (K := H). - apply subsequence_eq_def_1 in H. destruct H. destruct H. + apply Subsequence_bools in H. + destruct H. destruct H. destruct x. apply O_S in H. contradiction. destruct b. - destruct v. apply subsequence_nil_r. assert (x0 = a). inversion H0. + destruct v. apply Subsequence_nil_r. assert (x0 = a). inversion H0. reflexivity. rewrite H1. - apply subsequence_eq_def_3. exists nil. exists u. split. reflexivity. - apply subsequence_eq_def_2. apply subsequence_eq_def_1. + exists nil. exists u. split. reflexivity. apply IHu with (f := f). rewrite H1 in K. - apply subsequence_double_cons in K. assumption. - apply subsequence_cons_l. apply IHu with (f := f). - apply subsequence_eq_def_3. apply subsequence_eq_def_2. + apply Subsequence_double_cons in K. assumption. + apply Subsequence_cons_l. apply IHu with (f := f). + apply Subsequence_bools. exists x. split. inversion H. reflexivity. apply H0. - apply subsequence_cons_l. apply IHu with (f := f). assumption. + apply Subsequence_cons_l. apply IHu with (f := f). assumption. Qed. + + + + + + Theorem subsequence_incl {X: Type} : forall (u v: list X), subsequence u v -> incl v u. Proof.