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. 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. 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. 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).
  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.
  inversion H0. exists l0. exists x0.
  inversion H. rewrite H3. split; reflexivity.
  destruct x0. 
  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.

  exists nil. exists (x::x0). simpl.
  split; [ rewrite H | 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; destruct H; destruct H.
  destruct x. inversion H0.
  destruct b. exists (x). split. inversion H. rewrite H2. reflexivity.
  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.
  exists (true :: x).
  split. apply eq_S. assumption. 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.
  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.

  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 | right ];
  rewrite subsequence2_cons_eq; assumption.

  right. 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 | right ];
  rewrite subsequence3_cons_eq; assumption.

  right. 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_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.


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 subsequence3_cons_eq. rewrite <- IHl.
  rewrite subsequence_cons_eq. split; intro; assumption.

  split; intro H. apply subsequence3_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 H.

  destruct x0. inversion H. rewrite H2 in n. contradiction n. reflexivity.
  exists x2. exists x1. split. inversion H. reflexivity. assumption.
Qed.


Theorem subsequence2_app {X: Type} :
  forall l1 s1 l2 s2 : list X,
  subsequence2 l1 s1 -> subsequence2 l2 s2 -> subsequence2 (l1++l2) (s1++s2).
Proof.
  intros l1 s1 l2 s2. intros H I.
  destruct H. destruct I. exists (x++x0). destruct H. destruct H0.
  split. rewrite app_length. rewrite app_length.
  rewrite H. rewrite H0. reflexivity.
  rewrite H1. rewrite H2.

  assert (J: forall (t : list bool) (u : list X) (v: list bool) (w : list X),
    length t = length u
    -> combine (t++v) (u++w) = (combine t u) ++ (combine v w)).
  intros t u v w. generalize u. induction t; intro u0; intro K.
  replace u0 with (nil : list X). reflexivity.
  destruct u0. reflexivity. apply O_S in K. contradiction K.
  destruct u0. symmetry in K. apply O_S in K. contradiction K.
  simpl. rewrite IHt. reflexivity. inversion K. reflexivity.

  rewrite J. rewrite filter_app. rewrite map_app. reflexivity.
  assumption.
Qed.


Theorem subsequence_trans {X: Type} :
  forall (l1 l2 l3: list X),
  subsequence l1 l2 -> subsequence2 l2 l3 -> subsequence2 l1 l3.
Proof.
  intros l1 l2 l3. intros H I.
  destruct H. destruct H. destruct H. destruct I. destruct H1.
  exists (
    (repeat false (length x)) ++
    (flat_map (fun e => (fst e) :: (repeat false (length (snd e))))
              (combine x1 x0))).
  split.

  rewrite app_length. rewrite repeat_length.
  rewrite H0. rewrite app_length. rewrite Nat.add_cancel_l.
  rewrite flat_map_length. rewrite flat_map_length.
  assert (forall (u: list X) (v: list (list X)),
    length u = length v
    -> list_sum (map (fun z => length (fst z :: snd z))
                     (combine u v))
       = list_sum (map (fun z => S (length z)) v)).
  intros u v. generalize u. induction v; intro u0; intro I.
  apply length_zero_iff_nil in I. rewrite I. reflexivity.
  destruct u0.
  symmetry in I. apply PeanoNat.Nat.neq_succ_0 in I. contradiction I.
  simpl. rewrite IHv. reflexivity. inversion I. reflexivity.
  rewrite H3.
  assert (forall (u: list bool) (v: list (list X)),
    length u = length v
    -> list_sum (map (fun z => length (fst z :: repeat false (length (snd z))))
                     (combine u v))
       = list_sum (map (fun z => S (length z)) v)).
  intros u v. generalize u.
  induction v; intro u0; intro I; destruct u0. reflexivity.
  apply PeanoNat.Nat.neq_succ_0 in I. contradiction I.
  symmetry in I. apply PeanoNat.Nat.neq_succ_0 in I. contradiction I.
  simpl. rewrite IHv. rewrite repeat_length. reflexivity.
  inversion I. reflexivity. rewrite H4. reflexivity.
  rewrite H1. rewrite H. reflexivity. assumption.

  assert (K: forall (w v: list X) u,
    filter fst (combine ((repeat false (length w)) ++ u)
                        (w ++ v)) = filter fst (combine u v)).
  intro w0. induction w0. reflexivity. apply IHw0.
  rewrite H2. rewrite H0.
  assert (forall (u v: list X) (w: list bool),
    map snd (filter fst (combine ((repeat false (length u)) ++ w) (u ++ v)))
      = map snd (filter fst (combine w v))).
  intro u. induction u; intros v w. reflexivity.
  apply IHu. rewrite H3.
  assert (forall (u: list bool) (v: list X) (w: list (list X)),
    length u = length w
    -> length u = length v
    -> filter fst (combine
                      (flat_map
                         (fun e => fst e:: (repeat false (length (snd e))))
                         (combine u w))
                      (flat_map (fun e => fst e :: snd e) (combine v w)))
         = filter fst (combine u v)).
  intros u v w. generalize u. generalize v.
  induction w; intros v0 u0; intros I J.
  apply length_zero_iff_nil in I. rewrite I in J. rewrite I.
  symmetry in J. apply length_zero_iff_nil in J. rewrite J.
  reflexivity.
  destruct u0. reflexivity. destruct v0.
  apply PeanoNat.Nat.neq_succ_0 in J. contradiction J.
  destruct b; simpl; rewrite K; rewrite IHw.
  reflexivity. inversion I. reflexivity. inversion J. reflexivity.
  reflexivity. inversion I. reflexivity. inversion J. reflexivity.
  rewrite H4. reflexivity.
  rewrite H1. rewrite H. reflexivity.
  rewrite H1. reflexivity.
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_2.
  exists [true; false; true; false; true].
  split; reflexivity.
  apply Nat.eq_dec.
Qed.