From 5216516cff7c22fd894047b74558bab1719f82dc Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Fri, 24 Nov 2023 08:39:38 +0100 Subject: [PATCH] Update --- src/subsequences.v | 16 +++++++--------- 1 file changed, 7 insertions(+), 9 deletions(-) diff --git a/src/subsequences.v b/src/subsequences.v index 56714fa..c708dea 100644 --- a/src/subsequences.v +++ b/src/subsequences.v @@ -834,12 +834,11 @@ Qed. Theorem subsequence_as_filter {X: Type} : - forall (u v: list X), - (exists f, v = filter f u) -> subsequence u v. + forall (u v: list X) f, v = filter f u -> subsequence u v. Proof. - intros u v; intro H. destruct H. rewrite H. + intros u v f; intro H. rewrite H. apply subsequence_eq_def_3. apply subsequence_eq_def_2. - exists (map x u). split. apply map_length. + exists (map f u). split. apply map_length. assert (L: forall g (w: list X), filter g w = map snd (filter fst (combine (map g w) w))). intros g w. induction w. reflexivity. simpl. destruct (g a). @@ -848,10 +847,9 @@ Qed. Theorem subsequence_partition {X: Type} : - forall (u v: list X), - (exists f, v = fst (partition f u)) -> subsequence u v . + forall (u v: list X) f, v = fst (partition f u) -> subsequence u v . Proof. - intros u v. intro H. destruct H. rewrite H. - rewrite partition_as_filter. simpl. apply subsequence_as_filter. - exists x. reflexivity. + intros u v f. intro H. rewrite H. + rewrite partition_as_filter. simpl. + apply subsequence_as_filter with (f := f). reflexivity. Qed.