coqbooks/src/subsequences.v

Require Import Nat.
Require Import PeanoNat.
Require Import List.
Import ListNotations.

Require Import Lia.


Definition subsequence {X: Type} (l s : list X) :=
  exists (l1: list X) (l2 : list (list X)),
    length s = length l2
    /\ l = l1 ++ flat_map (fun e => (fst e) :: (snd e)) (combine s l2).

Definition subsequence2 {X: Type} (l s : list X) :=
  exists (t: list bool),
    length t = length l /\ s = map snd (filter fst (combine t l)).

(*
  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.
  intro l. exists l. exists nil. rewrite app_nil_r. split; easy.
Qed.


Theorem subsequence_nil_cons_r {X: Type}: forall (l: list X) (a:X),
  ~ subsequence nil (a::l).
Proof.
  intros l a. 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 {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.
  intros l a. 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 subsequence_cons_l {X: Type}: forall (l s: list X) (a: X),
  subsequence l s -> subsequence (a::l) s.
Proof.
  intros l s a. intro H.
  destruct H. destruct H. destruct H.
  exists (a::x). exists x0. split. assumption.
  rewrite H0. reflexivity.
Qed.


Theorem subsequence2_cons_l {X: Type} : forall (l s: list X) (a: X),
  subsequence2 l s -> subsequence2 (a::l) s.
Proof.
  intros l s a. intro H.
  destruct H. destruct H. exists (false::x).
  split. simpl. apply eq_S. assumption.
  simpl. assumption.
Qed.


Theorem subsequence_cons_r {X: Type} : forall (l s: list X) (a: X),
  subsequence l (a::s) -> subsequence l s.
Proof.
  intros l s a. intro H. destruct H. destruct H. destruct H.
  destruct x0. apply PeanoNat.Nat.neq_succ_0 in H. contradiction H.
  exists (x++a::l0). exists x0. split. inversion H. reflexivity. rewrite H0.
  rewrite <- app_assoc. apply app_inv_head_iff. simpl. reflexivity.
Qed.


Theorem subsequence2_cons_r {X: Type} : forall (l s: list X) (a: X),
  subsequence2 l (a::s) -> subsequence2 l s.
Proof.
  intro l. induction l. intros. apply subsequence2_nil_cons_r in H.
  contradiction H. intros s a0 . intro H. destruct H. destruct H. destruct x.
  symmetry in H0. apply nil_cons in H0. contradiction H0.
  destruct b. simpl in H0. inversion H0.
  exists (false::x). split; try rewrite <- H; reflexivity.
  simpl in H0. apply subsequence2_cons_l. apply IHl with (a := a0).
  unfold subsequence2. exists (x). split. inversion H.
  reflexivity. assumption.
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.
  destruct H. destruct H. destruct H.
  destruct x. destruct x0.
  apply PeanoNat.Nat.neq_succ_0 in H. contradiction H.
  simpl in H0. inversion H0. exists l0. exists x0.
  inversion H. rewrite H3. split; reflexivity.
  destruct x0. simpl in H0.
  apply PeanoNat.Nat.neq_succ_0 in H. contradiction H.
  exists (x1 ++ (a::l0)). exists x0. inversion H. rewrite H2. split. reflexivity.
  inversion H0. rewrite <- app_assoc. apply app_inv_head_iff.
  rewrite app_comm_cons. reflexivity.

  intro H. destruct H. destruct H. destruct H.
  exists nil. exists (x::x0). simpl. split. rewrite H. reflexivity.
  rewrite H0. reflexivity.
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.
  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.
Qed.


(*
  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.
 *)


Theorem subsequence2_dec {X: Type}:
  (forall x y : X, {x = y} + {x <> y})
  -> 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.
  right. apply subsequence2_nil_cons_r.

  intro s. assert({subsequence2 l s} + {~ subsequence2 l s}). apply IHl.
  destruct H0.

  rewrite <- subsequence2_cons_eq with (a := a) in s0.
  apply subsequence2_cons_r in s0. left. assumption.

  destruct s. left. apply subsequence2_nil_r.
  assert ({x=a}+{x<>a}). apply H. destruct H0. rewrite e.
  destruct IHl with (s := s).
  left. rewrite subsequence2_cons_eq. assumption.
  right. rewrite subsequence2_cons_eq. assumption.

  right. unfold not in n. unfold not. intro I.
  destruct I. destruct H0. destruct x0.
  symmetry in H1. apply nil_cons in H1. contradiction H1.
  destruct b.
  inversion H1. rewrite H3 in n0. contradiction n0. reflexivity.

  assert (subsequence2 l (x::s)). exists x0. split.
  inversion H0. reflexivity. assumption. apply n in H2. contradiction H2.
Qed.


Theorem subsequence_eq_def {X: Type} :
  (forall (x y : X), {x = y} + {x <> y})
  -> (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 *)
  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.
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 in s0. left. assumption.
  assumption. rewrite <- subsequence_eq_def in n. right. assumption.
  assumption.
Qed.





Example test1: subsequence [1;2;3;4;5] [1;3;5].
Proof.
  unfold subsequence.
  exists [].
  exists [[2];[4];[]]. simpl. easy.
Qed.

Example test2: subsequence [1;2;3;4;5] [2;4].
Proof.
  unfold subsequence.
  exists [1].
  exists [[3];[5]]. simpl. easy.
Qed.

Example test3: subsequence [1;2;3;4;5] [1;3;5].
Proof.
  rewrite subsequence_eq_def.
  exists [true; false; true; false; true].
  split; reflexivity.
  apply Nat.eq_dec.
Qed.