From 9ad87a7470fb438ef6e18eceafed50e9b0022183 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Wed, 6 Dec 2023 09:51:37 +0100 Subject: [PATCH] Update --- src/subsequences2.v | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) diff --git a/src/subsequences2.v b/src/subsequences2.v index 8ca1445..d631639 100644 --- a/src/subsequences2.v +++ b/src/subsequences2.v @@ -500,17 +500,13 @@ Proof. Qed. - - - - -Theorem subsequence_split {X: Type} : +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). + 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. + apply Subsequence_bools in H. destruct H. destruct H. assert (forall (b: list bool) (u v: list X), length b = length (u++v) @@ -535,13 +531,18 @@ Proof. 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; + split; apply Subsequence_bools; [ exists x0 | exists x1]; split; try assumption; reflexivity. assumption. Qed. + + + + + Theorem subsequence_split_2 {X: Type} : forall (u v w: list X), subsequence u (v++w)