From 2315f2321e26fbea6fdf9349d5a8896b8ca11ea5 Mon Sep 17 00:00:00 2001
From: Thomas Baruchel <baruchel@gmx.com>
Date: Thu, 23 Nov 2023 16:27:04 +0100
Subject: [PATCH] Update

---
 src/subsequences.v | 39 ++++++++++++++++++++++++---------------
 1 file changed, 24 insertions(+), 15 deletions(-)

diff --git a/src/subsequences.v b/src/subsequences.v
index 6624a04..99be30e 100644
--- a/src/subsequences.v
+++ b/src/subsequences.v
@@ -712,6 +712,16 @@ Proof.
  Qed.
 
 
+ Theorem subsequence_single {X: Type} :
+   forall (u: list X) a, In a u -> subsequence u [a].
+ Proof.
+   intro u. induction u; intro x; intro H. apply in_nil in H. contradiction.
+   destruct H. rewrite H. exists nil. exists [u]. split. reflexivity.
+   simpl. rewrite app_nil_r. reflexivity. apply subsequence_cons_l.
+   apply IHu. assumption.
+Qed.
+
+
 Theorem subsequence_filter_2 {X: Type} :
   forall (u v: list X) f,
     subsequence u v -> subsequence (filter f u) (filter f v).
@@ -731,22 +741,21 @@ Proof.
   assert (f a = true \/ f a = false).
   destruct (f a); [ left | right ]; reflexivity. destruct H0.
   simpl. rewrite H0.
-  replace (a::v) with ([a] ++ v) in H. apply subsequence_split in H.
+  replace (a::v) with ([a] ++ v) in H. apply subsequence_split_2 in H.
+  destruct H. destruct H. destruct H. destruct H1.
 
-
-
-
-  destruct H. destruct H. destruct x0. destruct H.
-  apply PeanoNat.Nat.neq_succ_0 in H. contradiction.
-  destruct H. simpl in H0. rewrite H0.
-
-
-
-  simpl. destruct (f a).
-
-
-
-  apply subsequence_cons_r.
+  assert (subsequence ((filter f x) ++ (filter f x0))
+                      ((filter f [a]) ++ (filter f v))).
+  apply subsequence_app. simpl. rewrite H0.
+  apply subsequence_incl in H1. apply incl_cons_inv in H1.
+  destruct H1.
+  assert (In a (filter f x)). apply filter_In. split; assumption.
+  apply subsequence_single. assumption. apply IHv. assumption.
+  rewrite <- filter_app in H3. rewrite <- H in H3. simpl in H3.
+  rewrite H0 in H3. assumption. reflexivity.
+  simpl. rewrite H0. apply IHv. apply subsequence_cons_r in H.
+  assumption.
+Qed.