From d3cb1fc17529a0491f3f6b9c2dd0b502389318c9 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Thu, 23 Nov 2023 11:43:14 +0100 Subject: [PATCH] Update --- src/subsequences.v | 46 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 46 insertions(+) diff --git a/src/subsequences.v b/src/subsequences.v index f41a8f9..7a2fce0 100644 --- a/src/subsequences.v +++ b/src/subsequences.v @@ -604,6 +604,52 @@ Proof. Qed. +Theorem subsequence_split {X: Type} : + forall (u v w: list X), + subsequence (u++v) w + -> (exists a b, w = a++b /\ (subsequence u a) /\ subsequence v b). +Proof. + intros u v w. intro H. + apply subsequence_eq_def_1 in H. + destruct H. destruct H. + + assert (forall (b: list bool) (u v: list X), + length b = length (u++v) + -> exists x y, b = x++y /\ length x = length u /\ length y = length v). + intros b u0 v0. intro I. + rewrite app_length in I. + exists (firstn (length u0) b). exists (skipn (length u0) b). + split. symmetry. apply firstn_skipn. split. + rewrite firstn_length_le. reflexivity. rewrite I. + apply PeanoNat.Nat.le_add_r. rewrite skipn_length. + rewrite I. rewrite Nat.add_sub_swap. rewrite PeanoNat.Nat.sub_diag. + reflexivity. apply le_n. + apply H1 in H. destruct H. destruct H. destruct H. destruct H2. + + exists (map snd (filter fst (combine x0 u))). + exists (map snd (filter fst (combine x1 v))). + rewrite <- map_app. rewrite <- filter_app. + + assert (L: forall (g i: list bool) (h j: list X), length g = length h + -> (combine g h) ++ (combine i j) = combine (g++i) (h++j)). + intro g. induction g; intros i h j; intro I. + symmetry in I. apply length_zero_iff_nil in I. rewrite I. + reflexivity. + destruct h. apply PeanoNat.Nat.neq_succ_0 in I. contradiction. + simpl. rewrite IHg. reflexivity. inversion I. reflexivity. + rewrite L. rewrite <- H. split. assumption. split. + + apply subsequence_eq_def_3. apply subsequence_eq_def_2. + exists x0. split. assumption. reflexivity. + apply subsequence_eq_def_3. apply subsequence_eq_def_2. + exists x1. split. assumption. reflexivity. + + assumption. +Qed. + + + + (** * Tests *)