From d62a5752aee8040bc4cbd60c5dd1fe7736c3bd2d Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Mon, 30 Oct 2023 19:34:21 +0100 Subject: [PATCH] Update --- src/subsequences.v | 17 +++++++---------- 1 file changed, 7 insertions(+), 10 deletions(-) diff --git a/src/subsequences.v b/src/subsequences.v index 8fe687b..6a19959 100644 --- a/src/subsequences.v +++ b/src/subsequences.v @@ -329,10 +329,10 @@ Proof. assert ({a=x} + {a<>x}). apply I. destruct H. - rewrite e. rewrite subsequence2_cons_eq. rewrite <- IHl. + rewrite e. rewrite subsequence3_cons_eq. rewrite <- IHl. rewrite subsequence_cons_eq. split; intro; assumption. - split; intro H. apply subsequence2_cons_l. apply IHl. + split; intro H. apply subsequence3_cons_l. apply IHl. destruct H. destruct H. destruct H. destruct x0. destruct x1. apply PeanoNat.Nat.neq_succ_0 in H. contradiction H. @@ -342,14 +342,11 @@ Proof. reflexivity. apply subsequence_cons_l. apply IHl. - destruct H. destruct H. - destruct x0. simpl in H0. - symmetry in H0. apply nil_cons in H0. contradiction H0. - destruct b. simpl in H0. inversion H0. rewrite H2 in n. - contradiction n. reflexivity. - exists x0. inversion H. inversion H0. - split; reflexivity. -Admitted. + destruct H. destruct H. destruct H. + + destruct x0. inversion H. rewrite H2 in n. contradiction n. reflexivity. + exists x2. exists x1. split. inversion H. reflexivity. assumption. +Qed. Theorem subsequence_dec {X: Type}: