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

Require Import Lia.


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 Type) :=
  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 : 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_l : forall (l s: list Type) (a: Type),
  subsequence2 l s -> subsequence2 (a::l) s.
Proof.
  intros l s a. intro H. unfold subsequence2 in H.
  destruct H. destruct H. exists (false::x).
  split. simpl. apply eq_S. assumption.
  simpl. assumption.
Qed.


Theorem subsequence2_cons_r : forall (l s: list Type) (a: Type),
  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. unfold subsequence2 in H.
  destruct H. destruct H. destruct x.
  symmetry in H0. apply nil_cons in H0. contradiction H0.
  destruct b. simpl in H0. inversion H0.
  unfold subsequence2. 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 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.

  (*
  induction x. symmetry in H0.
  apply Nat.neq_succ_0 in H0. contradiction H0.

  destruct a0. inversion H1. unfold subsequence2. exists x.
  split. inversion H0. reflexivity. reflexivity.
  simpl in H1.

  apply IHx.
   *)

  assert (count_occ Bool.bool_dec x true = length (a::l2)).
  apply H with (l := a::l1); assumption.
  assert (In true x). rewrite count_occ_In with (eq_dec := Bool.bool_dec).
  rewrite H2. simpl. lia. (* TODO *)
  apply In_split in H3. destruct H2. destruct H2.





  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.
   *)
  simpl in H1.
  apply H in H1. simpl in H1.


  assert (count_occ Bool.bool_dec x true = length l2).
  apply H with (l := l1). assumption. inversion H0. assumption.



  assert (count_occ Bool.bool_dec x true = length (a::l2)).
  apply H with (l := l1). assumption. inversion H0. assumption.

  destruct x. symmetry in H2. apply PeanoNat.Nat.neq_succ_0 in H2.
  contradiction H2.

  



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.
  (* 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 (x = nil). destruct x. 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 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.





  destruct H. destruct H. destruct H.
  assert (x0 = nil). symmetry in H. apply length_zero_iff_nil in H.
  assumption. rewrite H1 in H0. simpl in H0.








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.