From 23a6870a6a3d2823b6b895d47e267a2ce911714e Mon Sep 17 00:00:00 2001
From: Thomas Baruchel <baruchel@gmx.com>
Date: Tue, 31 Oct 2023 09:03:37 +0100
Subject: [PATCH] Update

---
 src/subsequences.v | 40 ++++++++++++++++++++--------------------
 1 file changed, 20 insertions(+), 20 deletions(-)

diff --git a/src/subsequences.v b/src/subsequences.v
index 6a19959..0ac0b63 100644
--- a/src/subsequences.v
+++ b/src/subsequences.v
@@ -142,7 +142,7 @@ Qed.
 Theorem subsequence_cons_eq {X: Type} : forall (l1 l2: list X) (a: X),
   subsequence (a::l1) (a::l2) <-> subsequence l1 l2.
 Proof.
-  intros l s a. split. intro H.
+  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.
@@ -154,7 +154,7 @@ Proof.
   inversion H0. rewrite <- app_assoc. apply app_inv_head_iff.
   rewrite app_comm_cons. reflexivity.
 
-  intro H. destruct H. destruct H. destruct H.
+  destruct H. destruct H. destruct H.
   exists nil. exists (x::x0). simpl. split. rewrite H. reflexivity.
   rewrite H0. reflexivity.
 Qed.
@@ -163,14 +163,14 @@ Qed.
 Theorem subsequence2_cons_eq {X: Type}: forall (l1 l2: list X) (a: X),
   subsequence2 (a::l1) (a::l2) <-> subsequence2 l1 l2.
 Proof.
-  intros l s a. split. intro H. unfold subsequence2 in H.
-  destruct H. destruct H. destruct x. inversion H0.
+  intros l s a. split; intro H; destruct H; destruct H.
+  destruct x. inversion H0.
   destruct b. exists (x). split. inversion H. rewrite H2. reflexivity. simpl in H0.
   inversion H0. reflexivity. simpl in H0. inversion H.
   assert (subsequence2 l (a::s)). exists x. split; assumption.
   apply subsequence2_cons_r with (a := a). assumption.
-  intro H. destruct H. destruct H. exists (true :: x).
-  split. simpl. apply eq_S. assumption. simpl. rewrite H0. reflexivity.
+  exists (true :: x).
+  split. simpl. apply eq_S. assumption. rewrite H0. reflexivity.
 Qed.
 
 
@@ -314,6 +314,19 @@ Proof.
 Qed.
 
 
+Theorem subsequence_dec {X: Type}:
+  (forall x y : X, {x = y} + {x <> y})
+  -> forall (l s : list X), { subsequence l s } + { ~ subsequence l s }.
+Proof.
+  intro H. intros l s.
+  assert ({ subsequence2 l s } + { ~ subsequence2 l s }).
+  apply subsequence2_dec. assumption. destruct H0.
+  rewrite <- subsequence_eq_def_2 in s0. left. assumption.
+  assumption. rewrite <- subsequence_eq_def_2 in n. right. assumption.
+  assumption.
+Qed.
+
+
 Theorem subsequence_eq_def_3 {X: Type} :
   (forall (x y : X), {x = y} + {x <> y})
   -> (forall l s : list X, subsequence l s <-> subsequence3 l s).
@@ -349,19 +362,6 @@ Proof.
 Qed.
 
 
-Theorem subsequence_dec {X: Type}:
-  (forall x y : X, {x = y} + {x <> y})
-  -> forall (l s : list X), { subsequence l s } + { ~ subsequence l s }.
-Proof.
-  intro H. intros l s.
-  assert ({ subsequence2 l s } + { ~ subsequence2 l s }).
-  apply subsequence2_dec. assumption. destruct H0.
-  rewrite <- subsequence_eq_def_2 in s0. left. assumption.
-  assumption. rewrite <- subsequence_eq_def_2 in n. right. assumption.
-  assumption.
-Qed.
-
-
 
 
 
@@ -381,7 +381,7 @@ Qed.
 
 Example test3: subsequence [1;2;3;4;5] [1;3;5].
 Proof.
-  rewrite subsequence_eq_def.
+  rewrite subsequence_eq_def_2.
   exists [true; false; true; false; true].
   split; reflexivity.
   apply Nat.eq_dec.