From 49649d6fd0a72a4fc665796ddf4893def6bea48a Mon Sep 17 00:00:00 2001
From: Thomas Baruchel <baruchel@gmx.com>
Date: Mon, 30 Oct 2023 19:27:09 +0100
Subject: [PATCH] Update

---
 src/subsequences.v | 67 ++++++++++++++++++++++++++--------------------
 1 file changed, 38 insertions(+), 29 deletions(-)

diff --git a/src/subsequences.v b/src/subsequences.v
index 8064b7f..8fe687b 100644
--- a/src/subsequences.v
+++ b/src/subsequences.v
@@ -282,35 +282,14 @@ Theorem subsequence_eq_def_2 {X: Type} :
   -> (forall l s : list X, subsequence l s <-> subsequence2 l s).
 Proof.
   intro I. intro l. induction l.
-  (* first part of the induction *)
-  intro s. unfold subsequence. unfold subsequence2.
-  split. exists nil. split. reflexivity. simpl.
-  destruct H. destruct H. destruct H.
-  assert (x = nil). destruct x. reflexivity. simpl in H0.
-  apply nil_cons in H0. contradiction H0. rewrite H1 in H0.
-  simpl in H0. assert (combine s x0 = nil).
-  destruct (combine s x0). reflexivity. simpl in H0.
-  apply nil_cons in H0. contradiction H0.
-  destruct x0. destruct s. reflexivity. simpl in H.
-  apply PeanoNat.Nat.neq_succ_0 in H. contradiction H.
-  destruct s. reflexivity. simpl in H2.
-  symmetry in H2. apply nil_cons in H2. contradiction H2.
-  exists nil. exists nil. destruct s. simpl. easy.
-  destruct H. destruct H.
-  assert (x0 = nil). destruct x0. reflexivity. simpl in H.
-  apply PeanoNat.Nat.neq_succ_0 in H. contradiction H.
-  rewrite H1 in H0. simpl in H0.
-  symmetry in H0. apply nil_cons in H0. contradiction H0.
-  (* second part of the induction *)
-  intro s. destruct s. unfold subsequence. unfold subsequence2. split.
-  exists (repeat false (S (length l))). rewrite repeat_length.
-  split. easy. simpl.
-  assert (forall u,
-    (nil: list X)
-       = map snd (filter fst (combine (repeat false (length u)) u))).
-  intro u. induction u. reflexivity. simpl. assumption. apply H0.
-  exists (a::l). exists (nil). simpl. split; try rewrite app_nil_r; reflexivity.
-  (* deux cas : a = n ou non *)
+  intro s. split; intro H. destruct s. apply subsequence2_nil_r.
+  apply subsequence_nil_cons_r in H. contradiction H.
+  destruct s. apply subsequence_nil_r.
+  apply subsequence2_nil_cons_r in H. contradiction H.
+
+  intro s. destruct s. split; intro H. apply subsequence2_nil_r.
+  apply subsequence_nil_r.
+
   assert ({a=x} + {a<>x}). apply I. destruct H.
   rewrite e. rewrite subsequence2_cons_eq. rewrite <- IHl.
   rewrite subsequence_cons_eq. split; intro; assumption.
@@ -340,6 +319,36 @@ Theorem subsequence_eq_def_3 {X: Type} :
   -> (forall l s : list X, subsequence l s <-> subsequence3 l s).
 Proof.
   intro I. intro l. induction l.
+  intro s. split; intro H. destruct s. apply subsequence3_nil_r.
+  apply subsequence_nil_cons_r in H. contradiction H.
+  destruct s. apply subsequence_nil_r.
+  apply subsequence3_nil_cons_r in H. contradiction H.
+
+  intro s. destruct s. split; intro H. apply subsequence3_nil_r.
+  apply subsequence_nil_r.
+
+
+  assert ({a=x} + {a<>x}). apply I. destruct H.
+  rewrite e. rewrite subsequence2_cons_eq. rewrite <- IHl.
+  rewrite subsequence_cons_eq. split; intro; assumption.
+
+  split; intro H. apply subsequence2_cons_l. apply IHl.
+  destruct H. destruct H. destruct H.
+  destruct x0. destruct x1.
+  apply PeanoNat.Nat.neq_succ_0 in H. contradiction H.
+  simpl in H0. inversion H0. rewrite H2 in n. contradiction n.
+  reflexivity. inversion H0.
+  exists x2. exists x1. split. assumption.
+  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.