From a948caaef89cd6c5f3baeec85b65456cbe0af0e5 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Wed, 6 Dec 2023 10:00:08 +0100 Subject: [PATCH] Update --- src/subsequences2.v | 95 ++++++++++++++++++++++----------------------- 1 file changed, 46 insertions(+), 49 deletions(-) diff --git a/src/subsequences2.v b/src/subsequences2.v index d631639..a4a8d73 100644 --- a/src/subsequences2.v +++ b/src/subsequences2.v @@ -538,17 +538,14 @@ Proof. Qed. - - - - - -Theorem subsequence_split_2 {X: Type} : +Theorem Subsequence_split_2 {X: Type} : forall (u v w: list X), - subsequence u (v++w) - -> (exists a b, u = a++b /\ (subsequence a v) /\ subsequence b w). + Subsequence u (v++w) + -> (exists a b, u = a++b /\ (Subsequence a v) /\ Subsequence b w). Proof. - intros u v w. intro H. destruct H. destruct H. destruct H. + intros u v w. intro H. + apply Subsequence_flat_map in H. + destruct H. destruct H. destruct H. exists (x ++ flat_map (fun e : X * list X => fst e :: snd e) (combine v x0)). exists ( @@ -565,70 +562,71 @@ Proof. simpl. rewrite IHw0. reflexivity. inversion I. reflexivity. rewrite L. reflexivity. rewrite app_length in H. rewrite H. reflexivity. split. - exists x. exists (firstn (length v) x0). split. - rewrite firstn_length. rewrite <- H. rewrite app_length. + + apply Subsequence_flat_map. exists x. exists (firstn (length v) x0). + split. rewrite firstn_length. rewrite <- H. rewrite app_length. rewrite min_l. reflexivity. apply PeanoNat.Nat.le_add_r. rewrite combine_firstn_l. reflexivity. - exists nil. exists (skipn (length v) x0). split. - rewrite app_length in H. rewrite skipn_length. rewrite <- H. + apply Subsequence_flat_map. exists nil. exists (skipn (length v) x0). + split. rewrite app_length in H. rewrite skipn_length. rewrite <- H. rewrite PeanoNat.Nat.add_sub_swap. rewrite PeanoNat.Nat.sub_diag. reflexivity. reflexivity. reflexivity. Qed. -Theorem subsequence_filter_2 {X: Type} : +Theorem Subsequence_filter_2 {X: Type} : 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. intros u v. generalize u. induction v; intros u0 f; intro H. - apply subsequence_nil_r. + apply Subsequence_nil_r. assert (f a = true \/ f a = false). destruct (f a); [ left | right ]; reflexivity. destruct H0. simpl. rewrite H0. - replace (a::v) with ([a] ++ v) in H. apply subsequence_split_2 in H. + replace (a::v) with ([a] ++ v) in H. apply Subsequence_split_2 in H. destruct H. destruct H. destruct H. destruct H1. - assert (subsequence ((filter f x) ++ (filter f x0)) + assert (Subsequence ((filter f x) ++ (filter f x0)) ((filter f [a]) ++ (filter f v))). - apply subsequence_app. simpl. rewrite H0. - apply subsequence_incl in H1. apply incl_cons_inv in H1. destruct H1. + apply Subsequence_app. simpl. rewrite H0. + apply Subsequence_incl in H1. apply incl_cons_inv in H1. destruct H1. assert (In a (filter f x)). apply filter_In. split; assumption. - apply subsequence_in. assumption. apply IHv. assumption. + apply Subsequence_in. assumption. apply IHv. assumption. rewrite <- filter_app in H3. rewrite <- H in H3. simpl in H3. rewrite H0 in H3. assumption. reflexivity. - simpl. rewrite H0. apply IHv. apply subsequence_cons_r in H. + simpl. rewrite H0. apply IHv. apply Subsequence_cons_r in H. assumption. Qed. -Theorem subsequence_add {X: Type} : - forall (u v w: list X) x, subsequence u v -> Add x u w -> subsequence w v. +Theorem Subsequence_add {X: Type} : + forall (u v w: list X) x, Subsequence u v -> Add x u w -> Subsequence w v. Proof. intros u v w. generalize u v. induction w; intros u0 v0 x; intros H I; inversion I. - rewrite <- H2. apply subsequence_cons_l. rewrite <- H3. assumption. + rewrite <- H2. apply Subsequence_cons_l. rewrite <- H3. assumption. - assert (J := H). apply subsequence_eq_def_1 in H. rewrite <- H1 in H. + assert (J := H). apply Subsequence_bools in H. rewrite <- H1 in H. rewrite H0 in H. destruct H. destruct H. destruct x1. apply O_S in H. contradiction. destruct b. - rewrite H4. simpl. apply subsequence_double_cons. + rewrite H4. simpl. apply Subsequence_double_cons. apply IHw with (u := l) (x := x). - apply subsequence_eq_def_3. apply subsequence_eq_def_2. exists x1. + apply Subsequence_bools. exists x1. inversion H. split; reflexivity. assumption. - apply subsequence_cons_r with (a:=a). - rewrite H4. simpl. apply subsequence_double_cons. + apply Subsequence_cons_r with (a:=a). + rewrite H4. simpl. apply Subsequence_double_cons. apply IHw with (u := l) (x := x). - apply subsequence_eq_def_3. apply subsequence_eq_def_2. exists x1. + apply Subsequence_bools. exists x1. inversion H. split; reflexivity. assumption. Qed. -Theorem subsequence_nodup {X: Type} : - forall (u v: list X), subsequence u v -> NoDup u -> NoDup v. +Theorem Subsequence_nodup {X: Type} : + forall (u v: list X), Subsequence u v -> NoDup u -> NoDup v. Proof. - intros u v. intros H I. apply subsequence_eq_def_1 in H. + intros u v. intros H I. apply Subsequence_bools in H. destruct H. destruct H. rewrite H0. assert (J: forall z (q: list X), @@ -654,23 +652,22 @@ Proof. Qed. -Theorem subsequence_in_2 {X: Type} : - forall (u v: list X) a, subsequence u v -> In a v -> In a u. +Theorem Subsequence_in_2 {X: Type} : + forall (u v: list X) a, Subsequence u v -> In a v -> In a u. Proof. intros u v. generalize u. induction v; intros u0 a0; intros H I. contradiction I. destruct I. - apply subsequence_eq_def_1 in H. apply subsequence_eq_def_2 in H. destruct H. destruct H. destruct H. rewrite H. rewrite H0. - apply in_elt. apply IHv. apply subsequence_cons_r in H. + apply in_elt. apply IHv. apply Subsequence_cons_r in H. assumption. assumption. Qed. -Theorem subsequence_not_in {X: Type} : - forall (u v: list X) a, subsequence u v -> ~ In a u -> ~ In a v. +Theorem Subsequence_not_in {X: Type} : + forall (u v: list X) a, Subsequence u v -> ~ In a u -> ~ In a v. Proof. intros u v. generalize u. induction v; intros u0 a0; intros H I. - easy. apply not_in_cons. split. apply subsequence_incl in H. + easy. apply not_in_cons. split. apply Subsequence_incl in H. apply incl_cons_inv in H. destruct H. assert (forall z (x y: X), In x z -> ~ In y z -> x <> y). @@ -680,27 +677,27 @@ Proof. apply IHz. assumption. apply not_in_cons in K. destruct K. assumption. apply not_eq_sym. generalize I. generalize H. apply H1. generalize I. apply IHv. - apply subsequence_cons_r in H. assumption. + apply Subsequence_cons_r in H. assumption. Qed. -Theorem subsequence_as_filter {X: Type} : - forall (u: list X) f, subsequence u (filter f u). +Theorem Subsequence_as_filter {X: Type} : + forall (u: list X) f, Subsequence u (filter f u). Proof. - intros u f. apply subsequence_eq_def_3. apply subsequence_eq_def_2. + intros u f. apply Subsequence_bools. exists (map f u). split. apply map_length. induction u. reflexivity. simpl. destruct (f a). simpl. rewrite IHu. reflexivity. assumption. Qed. -Theorem subsequence_as_partition {X: Type} : +Theorem Subsequence_as_partition {X: Type} : forall (u v w: list X) f, - (v, w) = partition f u -> (subsequence u v) /\ (subsequence u w). + (v, w) = partition f u -> (Subsequence u v) /\ (Subsequence u w). Proof. intros u v w f. intro H. rewrite partition_as_filter in H. split. replace v with (fst (v, w)). rewrite H. simpl. - apply subsequence_as_filter. reflexivity. + apply Subsequence_as_filter. reflexivity. replace w with (snd (v, w)). rewrite H. simpl. - apply subsequence_as_filter. reflexivity. + apply Subsequence_as_filter. reflexivity. Qed.