From d44ad56beae573cc070774a43df8bbc6255893f6 Mon Sep 17 00:00:00 2001
From: Thomas Baruchel <baruchel@gmx.com>
Date: Mon, 30 Oct 2023 17:43:24 +0100
Subject: [PATCH] Update

---
 src/subsequences.v | 62 ++++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 60 insertions(+), 2 deletions(-)

diff --git a/src/subsequences.v b/src/subsequences.v
index 52482d8..46d4a58 100644
--- a/src/subsequences.v
+++ b/src/subsequences.v
@@ -3,8 +3,6 @@ Require Import PeanoNat.
 Require Import List.
 Import ListNotations.
 
-Require Import Lia.
-
 
 Definition subsequence {X: Type} (l s : list X) :=
   exists (l1: list X) (l2 : list (list X)),
@@ -15,6 +13,12 @@ Definition subsequence2 {X: Type} (l s : list X) :=
   exists (t: list bool),
     length t = length l /\ s = map snd (filter fst (combine t l)).
 
+Fixpoint subsequence3 {X: Type} (l s : list X) : Prop :=
+  match s with
+  | nil    => True
+  | hd::tl => exists l1 l2, l = l1 ++ (hd::l2) /\ subsequence3 l2 tl
+  end.
+
 (*
   TODO: problème, les éléments de l ne sont pas uniques ; or
    il doit pouvoir y avoir des différences dans la décision de les
@@ -60,6 +64,21 @@ Proof.
 Qed.
 
 
+Theorem subsequence3_nil_r {X: Type} : forall (l : list X), subsequence3 l nil.
+Proof.
+  intro l. reflexivity.
+Qed.
+
+
+Theorem subsequence3_nil_cons_r {X: Type}: forall (l: list X) (a:X),
+  ~ subsequence3 nil (a::l).
+Proof.
+  intros l a. unfold not. intro H. destruct H. destruct H. destruct H.
+  destruct x. simpl in H. apply nil_cons in H. contradiction H.
+  simpl in H. apply nil_cons in H. contradiction H.
+Qed.
+
+
 Theorem subsequence_cons_l {X: Type}: forall (l s: list X) (a: X),
   subsequence l s -> subsequence (a::l) s.
 Proof.
@@ -80,6 +99,17 @@ Proof.
 Qed.
 
 
+Theorem subsequence3_cons_l {X: Type} : forall (l s: list X) (a: X),
+  subsequence3 l s -> subsequence3 (a::l) s.
+Proof.
+  intros l s a. intro H.
+  destruct s. apply subsequence3_nil_r.
+  destruct H. destruct H. destruct H.
+  exists (a::x0). exists x1. rewrite H.
+  split. reflexivity. assumption.
+Qed.
+
+
 Theorem subsequence_cons_r {X: Type} : forall (l s: list X) (a: X),
   subsequence l (a::s) -> subsequence l s.
 Proof.
@@ -104,6 +134,18 @@ Proof.
 Qed.
 
 
+Theorem subsequence3_cons_r {X: Type} : forall (l s: list X) (a: X),
+  subsequence3 l (a::s) -> subsequence3 l s.
+Proof.
+  intros l s a. intro H. simpl in H. destruct H. destruct H.
+  destruct s. apply subsequence3_nil_r. destruct H. simpl in H0.
+  destruct H0. destruct H0. destruct H0.
+  exists (x ++ a::x2). exists x3.
+  rewrite H. rewrite H0. split. rewrite <- app_assoc.
+  rewrite app_comm_cons. reflexivity. assumption.
+Qed.
+
+
 Theorem subsequence_cons_eq {X: Type} : forall (l1 l2: list X) (a: X),
   subsequence (a::l1) (a::l2) <-> subsequence l1 l2.
 Proof.
@@ -139,6 +181,22 @@ Proof.
 Qed.
 
 
+Theorem subsequence3_cons_eq {X: Type} : forall (l1 l2: list X) (a: X),
+  subsequence3 (a::l1) (a::l2) <-> subsequence3 l1 l2.
+Proof.
+  intros l s a. split. intro H.
+  destruct H. destruct H. destruct H.
+  destruct x. inversion H. assumption.
+  destruct s. apply subsequence3_nil_r.
+  destruct H0. destruct H0. destruct H0.
+  exists (x1 ++ (a::x3)). exists x4.
+  inversion H. rewrite H0. rewrite <- app_assoc.
+  rewrite app_comm_cons. split. reflexivity.
+  assumption.
+  intro H. exists nil. exists l. split. reflexivity. assumption.
+Qed.
+
+
 (*
   assert (forall (l s: list Type) t,
       s = map snd (filter fst (combine t l))