From 61c8077d6ccb61b2de37a44afd2dc810a3a2c6b5 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Mon, 30 Oct 2023 12:33:00 +0100 Subject: [PATCH] Update --- src/subsequences.v | 30 +++++++++++++++++++++++++----- 1 file changed, 25 insertions(+), 5 deletions(-) diff --git a/src/subsequences.v b/src/subsequences.v index 7ab4864..00c819b 100644 --- a/src/subsequences.v +++ b/src/subsequences.v @@ -90,11 +90,6 @@ Proof. Qed. - - - - - Theorem subsequence2_cons_r : forall (l s: list Type) (a: Type), subsequence2 l (a::s) -> subsequence2 l s. Proof. @@ -109,6 +104,31 @@ Proof. Qed. +Theorem subsequence_cons_eq : forall (l1 l2: list Type) (a: Type), + subsequence (a::l1) (a::l2) <-> subsequence l1 l2. +Proof. + intros l s a. split. intro H. + destruct H. destruct H. destruct H. + destruct x. destruct x0. + apply PeanoNat.Nat.neq_succ_0 in H. contradiction H. + simpl in H0. inversion H0. exists l0. exists x0. + inversion H. split; reflexivity. + destruct x0. simpl in H0. + apply PeanoNat.Nat.neq_succ_0 in H. contradiction H. + exists (x ++ (a::l0)). exists x0. inversion H. split. reflexivity. + inversion H0. rewrite <- app_assoc. apply app_inv_head_iff. + rewrite app_comm_cons. reflexivity. + + intro H. destruct H. destruct H. destruct H. + exists nil. exists (x::x0). simpl. split. rewrite H. reflexivity. + rewrite H0. reflexivity. +Qed. + + + + + + Theorem subsequence2_cons_eq : forall (l1 l2: list Type) (a: Type), subsequence2 (a::l1) (a::l2) <-> subsequence2 l1 l2. Proof.