From 995a822cae49358b880b8ff0e51389ccb8c63cf2 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Wed, 1 Nov 2023 19:09:31 +0100 Subject: [PATCH] Update --- src/subsequences.v | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/src/subsequences.v b/src/subsequences.v index e0e2631..bd9af72 100644 --- a/src/subsequences.v +++ b/src/subsequences.v @@ -337,11 +337,14 @@ Qed. Various general properties of a subsequence. *) -Theorem subsequence2_app {X: Type} : +Theorem subsequence_app {X: Type} : forall l1 s1 l2 s2 : list X, - subsequence2 l1 s1 -> subsequence2 l2 s2 -> subsequence2 (l1++l2) (s1++s2). + subsequence l1 s1 -> subsequence l2 s2 -> subsequence (l1++l2) (s1++s2). Proof. intros l1 s1 l2 s2. intros H I. + apply subsequence_eq_def_3. apply subsequence_eq_def_2. + apply subsequence_eq_def_1 in H. + apply subsequence_eq_def_1 in I. destruct H. destruct I. exists (x++x0). destruct H. destruct H0. split. rewrite app_length. rewrite app_length. rewrite H. rewrite H0. reflexivity. @@ -363,9 +366,11 @@ Qed. Theorem subsequence_trans {X: Type} : forall (l1 l2 l3: list X), - subsequence l1 l2 -> subsequence2 l2 l3 -> subsequence2 l1 l3. + subsequence l1 l2 -> subsequence l2 l3 -> subsequence l1 l3. Proof. intros l1 l2 l3. intros H I. + apply subsequence_eq_def_3. apply subsequence_eq_def_2. + apply subsequence_eq_def_1 in I. destruct H. destruct H. destruct H. destruct I. destruct H1. exists ( (repeat false (length x)) ++