coqbooks/src/subsequences.v

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


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

Fixpoint subsequence3 {X: Type} (l s : list X) : Prop :=
  match s with
  | nil    => True
  | hd::tl => exists l1 l2, l = l1 ++ (hd::l2) /\ subsequence3 l2 tl
  end.


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 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.
  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_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 subsequence3_nil_cons_r {X: Type}: forall (l: list X) (a:X),
  ~ subsequence3 nil (a::l).
Proof.
  intros l a. unfold not. intro H. destruct H. destruct H. destruct H.
  destruct x. simpl in H. apply nil_cons in H. contradiction H.
  simpl in H. apply nil_cons in H. contradiction H.
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 subsequence3_cons_l {X: Type} : forall (l s: list X) (a: X),
  subsequence3 l s -> subsequence3 (a::l) s.
Proof.
  intros l s a. intro H.
  destruct s. apply subsequence3_nil_r.
  destruct H. destruct H. destruct H.
  exists (a::x0). exists x1. rewrite H.
  split. reflexivity. 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 subsequence3_cons_r {X: Type} : forall (l s: list X) (a: X),
  subsequence3 l (a::s) -> subsequence3 l s.
Proof.
  intros l s a. intro H. simpl in H. destruct H. destruct H.
  destruct s. apply subsequence3_nil_r. destruct H. simpl in H0.
  destruct H0. destruct H0. destruct H0.
  exists (x ++ a::x2). exists x3.
  rewrite H. rewrite H0. split. rewrite <- app_assoc.
  rewrite app_comm_cons. 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.


Theorem subsequence3_cons_eq {X: Type} : forall (l1 l2: list X) (a: X),
  subsequence3 (a::l1) (a::l2) <-> subsequence3 l1 l2.
Proof.
  intros l s a. split. intro H.
  destruct H. destruct H. destruct H.
  destruct x. inversion H. assumption.
  destruct s. apply subsequence3_nil_r.
  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.
  intro H. exists nil. exists l. split. reflexivity. assumption.
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.
  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.
  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 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.
  intro I. intro l. induction l.
  intro s. split; intro H. destruct s. apply subsequence2_nil_r.
  apply subsequence_nil_cons_r in H. contradiction H.
  destruct s. apply subsequence_nil_r.
  apply subsequence2_nil_cons_r in H. contradiction H.

  intro s. destruct s. split; intro H. apply subsequence2_nil_r.
  apply subsequence_nil_r.

  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_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.
  intro s. split; intro H. destruct s. apply subsequence3_nil_r.
  apply subsequence_nil_cons_r in H. contradiction H.
  destruct s. apply subsequence_nil_r.
  apply subsequence3_nil_cons_r in H. contradiction H.

  intro s. destruct s. split; intro H. apply subsequence3_nil_r.
  apply subsequence_nil_r.


  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.
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 }.
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.





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.