Update

src/subsequences.v

@@ -19,13 +19,6 @@ Fixpoint subsequence3 {X: Type} (l s : list X) : Prop :=
   | 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
-   prendre ou non
-Definition subsequence3 (l s : list Type) :=
-  exists f, s = fst (partition f l).
- *)
 
 Theorem subsequence_nil_r {X: Type}: forall (l : list X), subsequence l nil.
 Proof.
@@ -33,6 +26,21 @@ Proof.
 Qed.
 
 
+Theorem subsequence2_nil_r {X: Type} : forall (l : list X), subsequence2 l nil.
+Proof.
+  intro l. 
+  exists (repeat false (length l)). rewrite repeat_length.
+  split. easy.
+  induction l. reflexivity. simpl. assumption.
+Qed.
+
+
+Theorem subsequence3_nil_r {X: Type} : forall (l : list X), subsequence3 l nil.
+Proof.
+  intro l. reflexivity.
+Qed.
+
+
 Theorem subsequence_nil_cons_r {X: Type}: forall (l: list X) (a:X),
   ~ subsequence nil (a::l).
 Proof.
@@ -45,15 +53,6 @@ Proof.
 Qed.
 
 
-Theorem subsequence2_nil_r {X: Type} : forall (l : list X), subsequence2 l nil.
-Proof.
-  intro l. 
-  exists (repeat false (length l)). rewrite repeat_length.
-  split. easy.
-  induction l. reflexivity. simpl. assumption.
-Qed.
-
-
 Theorem subsequence2_nil_cons_r {X: Type}: forall (l: list X) (a:X),
   ~ subsequence2 nil (a::l).
 Proof.
@@ -64,12 +63,6 @@ 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.
@@ -191,8 +184,7 @@ Proof.
   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.
+  rewrite app_comm_cons. split. reflexivity. assumption.
   intro H. exists nil. exists l. split. reflexivity. assumption.
 Qed.
 
@@ -230,7 +222,7 @@ Theorem subsequence2_dec {X: Type}:
   -> forall (l s : list X), { subsequence2 l s } + { ~ subsequence2 l s }.
 Proof.
   intro H.
-  intros l. induction l. intro s. destruct s. left. apply subsequence2_nil_r.
+  intro l. induction l. intro s. destruct s. left. apply subsequence2_nil_r.
   right. apply subsequence2_nil_cons_r.
 
   intro s. assert({subsequence2 l s} + {~ subsequence2 l s}). apply IHl.
@@ -256,7 +248,36 @@ Proof.
 Qed.
 
 
-Theorem subsequence_eq_def {X: Type} :
+Theorem subsequence3_dec {X: Type}:
+  (forall x y : X, {x = y} + {x <> y})
+  -> forall (l s : list X), { subsequence3 l s } + { ~ subsequence3 l s }.
+Proof.
+  intro H. intro l. induction l. intro s. destruct s. left. reflexivity.
+  right. apply subsequence3_nil_cons_r.
+
+  intro s. assert({subsequence3 l s} + {~ subsequence3 l s}). apply IHl.
+  destruct H0.
+
+  rewrite <- subsequence3_cons_eq with (a := a) in s0.
+  apply subsequence3_cons_r in s0. left. assumption.
+
+  destruct s. left. apply subsequence3_nil_r.
+  assert ({x=a}+{x<>a}). apply H. destruct H0. rewrite e.
+  destruct IHl with (s := s).
+  left. rewrite subsequence3_cons_eq. assumption.
+  right. rewrite subsequence3_cons_eq. assumption.
+
+  right. unfold not in n. unfold not. intro I.
+  destruct I. destruct H0. destruct H0. destruct x0.
+  inversion H0. rewrite H3 in n0. contradiction n0. reflexivity.
+
+  assert (subsequence3 l (x::s)). exists x2. exists x1.
+  inversion H0. split. reflexivity. assumption.
+  apply n in H2. contradiction H2.
+Qed.
+
+
+Theorem subsequence_eq_def_2 {X: Type} :
   (forall (x y : X), {x = y} + {x <> y})
   -> (forall l s : list X, subsequence l s <-> subsequence2 l s).
 Proof.
@@ -314,6 +335,14 @@ Proof.
 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).
+Proof.
+  intro I. intro l. induction l.
+Admitted.
+
+
 Theorem subsequence_dec {X: Type}:
   (forall x y : X, {x = y} + {x <> y})
   -> forall (l s : list X), { subsequence l s } + { ~ subsequence l s }.
@@ -321,8 +350,8 @@ Proof.
   intro H. intros l s.
   assert ({ subsequence2 l s } + { ~ subsequence2 l s }).
   apply subsequence2_dec. assumption. destruct H0.
-  rewrite <- subsequence_eq_def in s0. left. assumption.
-  assumption. rewrite <- subsequence_eq_def in n. right. assumption.
+  rewrite <- subsequence_eq_def_2 in s0. left. assumption.
+  assumption. rewrite <- subsequence_eq_def_2 in n. right. assumption.
   assumption.
 Qed.