Update

src/subsequences.v

@@ -4,15 +4,216 @@ Require Import List.
 Import ListNotations.
 
 
-Definition subsequence (l s : list nat) :=
-  exists (l1: list nat) (l2 : list (list nat)),
+Definition subsequence (l s : list Type) :=
+  exists (l1: list Type) (l2 : list (list Type)),
     length s = length l2
     /\ l = l1 ++ flat_map (fun e => (fst e) :: (snd e)) (combine s l2).
 
-Definition subsequence2 (l s : list nat) :=
+Definition subsequence2 (l s : list Type) :=
   exists (t: list bool),
     length t = length l /\ s = map snd (filter fst (combine t l)).
 
+
+Theorem subsequence_nil_r : forall (l : list Type), subsequence l nil.
+Proof.
+  intro l. unfold subsequence. exists l. exists nil. rewrite app_nil_r.
+  split; easy.
+Qed.
+
+
+Theorem subsequence_nil_cons_r : forall (l: list Type) (a:Type),
+  ~ subsequence nil (a::l).
+Proof.
+  intros l a. unfold subsequence. unfold not. intro H.
+  destruct H. destruct H. destruct H.
+  destruct x. rewrite app_nil_l in H0.
+  destruct x0. apply PeanoNat.Nat.neq_succ_0 in H. contradiction H.
+  simpl in H0. apply nil_cons in H0. contradiction H0.
+  apply nil_cons in H0. contradiction H0.
+Qed.
+
+
+Theorem subsequence2_nil_r : forall (l : list Type), subsequence2 l nil.
+Proof.
+  intro l. unfold subsequence2.
+  exists (repeat false (length l)). rewrite repeat_length.
+  split. easy.
+  induction l. reflexivity. simpl. assumption.
+Qed.
+
+
+Theorem subsequence2_nil_cons_r : forall (l: list Type) (a:Type),
+  ~ subsequence2 nil (a::l).
+Proof.
+  intros l a. unfold subsequence2. unfold not. intro H. destruct H.
+  destruct H. assert (x = nil). destruct x. reflexivity.
+  apply PeanoNat.Nat.neq_succ_0 in H. contradiction H.
+  rewrite H1 in H0. symmetry in H0. apply nil_cons in H0. contradiction H0.
+Qed.
+
+
+Theorem subsequence2_cons_eq : forall (l1 l2: list Type) (a: Type),
+  subsequence2 (a::l1) (a::l2) <-> subsequence2 l1 l2.
+Proof.
+
+  assert (forall (l s: list Type) t,
+      s = map snd (filter fst (combine t l))
+      -> length t = length l
+      -> count_occ Bool.bool_dec t true = length s).
+  intros l s t.
+
+  generalize l s. induction t. intros l0 s0. intros J K.
+  simpl in J. rewrite J. reflexivity.
+  intros l0 s0. intros J K.
+  destruct a. destruct s0. destruct l0.
+  apply Nat.neq_succ_0 in K. contradiction K.
+  apply nil_cons in J. contradiction J. simpl. apply eq_S.
+
+  destruct l0. 
+  apply Nat.neq_succ_0 in K. contradiction K.
+
+  apply IHt with (l := l0). inversion J. rewrite <- H1.
+  reflexivity. inversion K. reflexivity.
+
+  simpl. destruct l0.
+  apply Nat.neq_succ_0 in K. contradiction K.
+
+  apply IHt with (l := l0). inversion J. simpl.
+  reflexivity. inversion K. reflexivity.
+  (* fin de la démonstration de H *)
+
+  intros l1 l2 a. split; intro I.
+  unfold subsequence2 in I. destruct I. destruct H0. destruct x.
+  simpl in H0. symmetry in H0.
+  apply PeanoNat.Nat.neq_succ_0 in H0. contradiction H0.
+  destruct b. simpl in H0. inversion H1. rewrite <- H3.
+  unfold subsequence2. exists x. split. inversion H0. reflexivity.
+  assumption.
+  simpl in H1. unfold subsequence2. exists x. split. inversion H0.
+  reflexivity.
+
+  assert (count_occ Bool.bool_dec x true = length (a::l2)).
+  apply H with (l := l1). assumption. inversion H0. assumption.
+
+
+
+Theorem subsequence2_dec :
+  (forall x y : Type, {x = y} + {x <> y})
+  -> forall (l s : list Type), { subsequence2 l s } + { ~ subsequence2 l s }.
+Proof.
+  intro H.
+  intros 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.
+  destruct H0.
+
+  left. unfold subsequence2. unfold subsequence2 in s0. destruct s0.
+  destruct H0. exists (false::x). split. simpl. rewrite H0. reflexivity.
+  simpl. assumption.
+
+  destruct s. left. apply subsequence2_nil_r.
+  assert ({T=a}+{T<>a}). apply H. destruct H0.
+  rewrite e.
+
+
+
+
+
+
+
+
+
+
+  intro l0. destruct l0. right. apply subsequence2_nil_cons_r.
+  assert ({ subsequence2 l0 s } + { ~ subsequence2 l0 s }). apply IHs.
+
+
+Theorem subsequence2_dec :
+  (forall x y : Type, {x = y} + {x <> y})
+  -> forall (l s : list Type), { subsequence2 l s } + { ~ subsequence2 l s }.
+Proof.
+  intro H.
+  intros l s. generalize l.  induction s. left. apply subsequence2_nil_r.
+  intro l0. destruct l0. right. apply subsequence2_nil_cons_r.
+  assert ({ subsequence2 l0 s } + { ~ subsequence2 l0 s }). apply IHs.
+  assert ({T=a}+{T<>a}). apply H. destruct H0; destruct H1.
+  left. unfold subsequence2. unfold subsequence2 in s0. destruct s0.
+  destruct H0. exists (true::x). simpl. rewrite H0. split. reflexivity.
+  rewrite e. rewrite H1. reflexivity.
+  
+  (*
+  assert ({In a l0}+{~ In a l0}). apply In_dec. assumption.
+  destruct H0. apply In_split in i. destruct i.
+   *)
+
+
+
+
+Theorem subsequence_dec : forall (l s : list Type),
+  { subsequence l s } + { ~ subsequence l s }.
+Proof.
+  intros l s. generalize l.  induction s. left. apply subsequence_nil_r.
+  intro l0. destruct l0. right. apply subsequence_nil_cons_r.
+
+
+
+  intros l s. induction s. left. apply subsequence_nil_r.
+  destruct l. right. apply subsequence_nil_cons_r.
+
+
+
+  unfold subsequence2. destruct s. simpl.
+  left. exists nil. easy. right.
+
+  unfold not. intro H. destruct H. destruct H.
+  rewrite combine_nil in H0.
+  symmetry in H0. apply nil_cons in H0. assumption.
+
+  destruct IHl. left. unfold subsequence2. assert (H := s0).
+  unfold subsequence2 in H. destruct H. destruct H.
+  exists (false::x). split. simpl. apply eq_S. assumption.
+  assumption.
+
+  (* destructurer s puis tester les deux cas : a = (car s) ou non *)
+  destruct s. left. unfold subsequence2.
+
+
+
+
+Theorem subsequence_dec : forall (l s : list nat),
+  { subsequence2 l s } + { ~ subsequence2 l s }.
+Proof.
+  intros l s. induction l.
+  unfold subsequence2. destruct s. simpl.
+  left. exists nil. easy. right.
+
+  unfold not. intro H. destruct H. destruct H.
+  rewrite combine_nil in H0.
+  symmetry in H0. apply nil_cons in H0. assumption.
+
+  destruct IHl. left. unfold subsequence2. assert (H := s0).
+  unfold subsequence2 in H. destruct H. destruct H.
+  exists (false::x). split. simpl. apply eq_S. assumption.
+  assumption.
+
+  (* destructurer s puis tester les deux cas : a = (car s) ou non *)
+  destruct s. left. unfold subsequence2.
+
+  exists (repeat false (S (length l))). rewrite repeat_length.
+  split. easy. simpl.
+  assert (forall u,
+    (nil: list nat)
+       = map snd (filter fst (combine (repeat false (length u)) u))).
+  intro u. induction u. reflexivity. simpl. assumption. apply H.
+
+  assert ({a=n0}+{a<>n0}). apply PeanoNat.Nat.eq_dec. destruct H.
+
+
+
+
+
+
 Theorem subsequence_eq_def : forall l s, subsequence l s <-> subsequence2 l s.
 Proof.
   intro l. induction l.
@@ -40,11 +241,16 @@ Proof.
   exists (repeat false (S (length l))). rewrite repeat_length.
   split. easy. simpl.
   assert (forall u,
-    (nil: list nat)
+    (nil: list Type)
        = 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 *)
+  assert ({a=n} + {a<>n}). apply PeanoNat.Nat.eq_dec. destruct H.
+  unfold subsequence. unfold subsequence2. split.
+
+