TPPmark 2017

LCS.v

Require Import List Omega Program.

Section ListPairDP.
  Variable A : Set.
  Variable X : Set.
  Variable f_nil_nil : A.
  Variable f_nil_l2s : list (A * X).
  Variable f_l1_nils : list (A * X).
  Variable f_cons_cons : X -> X -> A -> A -> A -> A.
  Variable R : list X -> list X -> A -> Prop.
  Hypotheses f_nil_nil_spec : R nil nil f_nil_nil.
  Hypotheses f_nil_l2s_spec : forall i f_nil_l2' y,
    nth_error f_nil_l2s i = Some (f_nil_l2', y) ->
    R nil (skipn i (map snd f_nil_l2s)) f_nil_l2'.
  Hypotheses f_l1_nils_spec : forall i f_l1'_nil x,
    nth_error f_l1_nils i = Some (f_l1'_nil, x) ->
    R (skipn i (map snd f_l1_nils)) nil f_l1'_nil.
  Hypotheses f_cons_cons_spec : forall x l1' y l2' f_l1'_l2' f_l1_l2' f_l1'_l2,
    R l1' l2' f_l1'_l2' ->
    R (x :: l1') l2' f_l1_l2' ->
    R l1' (y :: l2') f_l1'_l2 ->
    R (x :: l1') (y :: l2') (f_cons_cons x y f_l1'_l2' f_l1_l2' f_l1'_l2).

  Definition ListPairDP_body {B} x f_l1_nil f_l1'_nil := fix ListPairDP_body k f_l1'_l2s : B :=
    match f_l1'_l2s with
    | nil => k f_l1'_nil f_l1_nil nil
    | (f_l1'_l2, y) :: f_l1'_l2's  => ListPairDP_body (fun f_l1'_l2' f_l1_l2' memo_l1_l2' =>
        let f_l1_l2 := f_cons_cons x y f_l1'_l2' f_l1_l2' f_l1'_l2 in
        k f_l1'_l2 f_l1_l2 ((f_l1_l2, y) :: memo_l1_l2')) f_l1'_l2's
    end.

  Fixpoint ListPairDP_aux {B} k f_l1_nils : B :=
    match f_l1_nils with
    | nil => k f_nil_nil (hd f_nil_nil (map fst f_nil_l2s)) f_nil_l2s
    | (f_l1_nil, x) :: f_l1'_nils => ListPairDP_aux (fun f_l1'_nil _ =>
        ListPairDP_body x f_l1_nil f_l1'_nil (const (k f_l1_nil))) f_l1'_nils
    end.

  Definition ListPairDP := ListPairDP_aux (fun _ f_l1_l2 _ => f_l1_l2) f_l1_nils.

  Lemma ListPairDP_body_spec B (P : B -> Prop)  x l1' f_l1_nil f_l1'_nil f_l1'_l2s :
    R l1' nil f_l1'_nil ->
    R (x :: l1') nil f_l1_nil ->
    (forall i f_l1'_l2' y,
      nth_error f_l1'_l2s i = Some (f_l1'_l2', y) ->
      R l1' (skipn i (map snd f_l1'_l2s)) f_l1'_l2') ->
    forall k,
    (forall f_l1'_l2 f_l1_l2 f_l1_l2s,
      R l1' (map snd f_l1'_l2s) f_l1'_l2 ->
      R (x :: l1') (map snd f_l1'_l2s) f_l1_l2 ->
      map snd f_l1'_l2s = map snd f_l1_l2s ->
      (forall i f_l1_l2' y,
        nth_error f_l1_l2s i = Some (f_l1_l2', y) ->
        R (x :: l1') (skipn i (map snd f_l1'_l2s)) f_l1_l2') ->
      P (k f_l1'_l2 f_l1_l2 f_l1_l2s)) ->
    P (ListPairDP_body x f_l1_nil f_l1'_nil k f_l1'_l2s).
  Proof.
    intros ? ? Hf_l1'_l2s.
    induction f_l1'_l2s as [ | [  ] ? IHf_l1'_l2's ]; simpl; intros k Hk.
    - apply Hk; eauto.
      intros [ ]; inversion 1.
    - apply IHf_l1'_l2's.
      + intros i. apply Hf_l1'_l2s with (i := S i).
      + intros ? ? ? ? ? ? ?.
        specialize (Hf_l1'_l2s 0 _ _ eq_refl); simpl in *.
        apply Hk; eauto.
        * simpl. congruence.
        * intros [ ]; inversion 1; subst; simpl; eauto.
  Qed.

  Lemma ListPairDP_aux_spec B (P : B -> Prop) f_l1'_nils :
    (forall i f_l1'_nil x,
      nth_error f_l1'_nils i = Some (f_l1'_nil, x) ->
      R (skipn i (map snd f_l1'_nils)) nil f_l1'_nil) ->
    forall k,
    (forall f_l1_nil f_l1_l2 f_l1_l2s,
      R (map snd f_l1'_nils) nil f_l1_nil ->
      R (map snd f_l1'_nils) (map snd f_nil_l2s) f_l1_l2 ->
      map snd f_nil_l2s = map snd f_l1_l2s ->
      (forall i f_l1_l2' y,
        nth_error f_l1_l2s i = Some (f_l1_l2', y) ->
        R (map snd f_l1'_nils) (skipn i (map snd f_nil_l2s)) f_l1_l2') ->
      P (k f_l1_nil f_l1_l2 f_l1_l2s)) ->
    P (ListPairDP_aux k f_l1'_nils).
  Proof.
    intros Hf_l1'_nil.
    induction f_l1'_nils as [ | [ ? ? ] f_l1'_nils IHf_l1'_nils ]; simpl; intros k Hk.
    - apply Hk; eauto.
      destruct f_nil_l2s as [ | [ ? ? ]]; simpl in *; eauto.
      apply (f_nil_l2s_spec 0 _ _ eq_refl).
    - apply IHf_l1'_nils.
      + intros i. apply Hf_l1'_nil with (i := S i).
      + specialize (Hf_l1'_nil 0 _ _ eq_refl). simpl in *.
        intros ? ? ? ? ? Heq ?.
        rewrite Heq in *.
        apply ListPairDP_body_spec with (l1' := map snd f_l1'_nils); eauto.
  Qed.

  Corollary ListPairDP_spec l1 l2 :
    l1 = map snd f_l1_nils ->
    l2 = map snd f_nil_l2s ->
    R l1 l2 ListPairDP.
  Proof.
    intros.
    subst.
    apply ListPairDP_aux_spec with (P := R (map snd f_l1_nils) (map snd f_nil_l2s)); eauto.
  Qed.
End ListPairDP.

Section LCS.
  Variable X : Set.
  Hypotheses X_eq_dec : forall x y : X, { x = y } + { x <> y }.

  Inductive subseq : list X -> list X -> Prop :=
    | subsq_nil : subseq nil nil
    | subseq_skip x l1 l2 :
        subseq l1 l2 ->
        subseq l1 (x :: l2)
    | subseq_common x l1 l2 :
        subseq l1 l2 ->
        subseq (x :: l1) (x :: l2).
  Hint Constructors subseq.

  Lemma subseq_nil l : subseq nil l.
  Proof. induction l; eauto. Qed.

  Lemma subseq_tl l l2 :
    subseq l l2 ->
    forall x l1, l = x :: l1 ->
    subseq l1 l2.
  Proof. induction 1; inversion 1; subst; eauto. Qed.

  Hint Resolve subseq_nil subseq_tl.

  Definition LCS_aux l1 l2 :=
    ListPairDP _ _ (0, nil)
      (map (pair (0, nil)) l2)
      (map (pair (0, nil)) l1)
      (fun x y (f_l1'_l2' f_l1_l2' f_l1'_l2 : _ * _) =>
        if X_eq_dec x y then
          let (n, s) := f_l1'_l2' in (S n, x :: s)
        else
          let (n1, s1) := f_l1'_l2 in
          let (n2, s2) := f_l1_l2' in
          if le_ge_dec n1 n2 then (n2, s2) else (n1, s1)).

  Definition LCS l1 l2 := snd (LCS_aux l1 l2).

  Lemma LCS_aux_subseq l1 l2 :
    subseq (snd (LCS_aux l1 l2)) l1 /\ subseq (snd (LCS_aux l1 l2)) l2.
  Proof.
    refine (ListPairDP_spec _ _ _ _ _ _ (fun l1 l2 p => subseq (snd p) l1 /\ subseq (snd p) l2) _ _ _ _ _ _ _ _);
      repeat rewrite map_map, map_id;
      simpl;
      eauto.
    - intros ? ? ? HIn.
      apply nth_error_In in HIn.
      apply in_map_iff in HIn.
      destruct HIn as [ ? [ Heq ]].
      inversion Heq. subst. eauto.
    - intros ? ? ? HIn.
      apply nth_error_In in HIn.
      apply in_map_iff in HIn.
      destruct HIn as [ ? [ Heq ]].
      inversion Heq. subst. eauto.
    - intros x ? y ? [ ? s ] [ n1 s1 ] [ n2 s2 ] [ ? ? ] [ ? ? ] [ ? ? ].
      destruct (X_eq_dec x y); subst; simpl; eauto.
      destruct (le_ge_dec n2 n1); eauto.
  Qed.

  Corollary LCS_subseq l1 l2 : subseq (LCS l1 l2) l1 /\ subseq (LCS l1 l2) l2.
  Proof. apply LCS_aux_subseq. Qed.

  Lemma LCS_aux_longest l1 l2 :
    let (n, s) := LCS_aux l1 l2 in
    n = length s /\ (forall l, subseq l l1 -> subseq l l2 -> length l <= length s).
  Proof.
    Local Hint Resolve le_n_S.
    refine (ListPairDP_spec _ _ _ _ _ _ (fun l1 l2 (p : _ * _) =>
      let (n, s) := p in
      n = length s /\ (forall l, subseq l l1 -> subseq l l2 -> length l <= length s)) _ _ _ _ _ _ _ _);
      repeat rewrite map_map, map_id;
      simpl;
      eauto.
    - split; eauto. inversion 1; simpl; eauto.
    - intros ? ? ? HIn.
      apply nth_error_In in HIn.
      apply in_map_iff in HIn.
      destruct HIn as [ ? [ Heq ] ].
      inversion Heq. subst. simpl.
      split; eauto.
      inversion 1. simpl. eauto.
    - intros ? ? ? HIn.
      apply nth_error_In in HIn.
      apply in_map_iff in HIn.
      destruct HIn as [ ? [ Heq ] ].
      inversion Heq. subst. simpl.
      split; eauto.
      inversion 2. simpl. eauto.
    - intros x ? y ? [ ? ? ] [ n1 ? ] [ n2 ? ] [ ? ? ] [ ? IH2 ] [ ? IH3 ].
      destruct (X_eq_dec x y);
        [ subst | destruct (le_ge_dec n2 n1) ]; simpl;
        split; eauto;
        intros ? Hsubseq1 Hsubseq2;
        inversion Hsubseq1 as [ | ? ? ? Hsubseq1' | ]; subst;
        inversion Hsubseq2 as [ | ? ? ? Hsubseq2' | ]; subst;
        try specialize (IH2 _ Hsubseq1 Hsubseq2');
        try specialize (IH3 _ Hsubseq1' Hsubseq2);
        simpl in *;
        (congruence || omega || eauto).
  Qed.

  Corollary LCS_longest l1 l2 l :
    subseq l l1 ->
    subseq l l2 ->
    length l <= length (LCS l1 l2).
  Proof.
    unfold LCS.
    specialize (LCS_aux_longest l1 l2).
    destruct (LCS_aux l1 l2).
    intros [ ? ? ].
    eauto.
  Qed.
End LCS.

LCS_naive.v

Require Import List Omega.

Section LCS.
  Variable X : Set.
  Hypotheses X_eq_dec : forall x y : X, { x = y } + { x <> y }.

  Inductive subseq : list X -> list X -> Prop :=
    | subsq_nil : subseq nil nil
    | subseq_skip x l1 l2 :
        subseq l1 l2 ->
        subseq l1 (x :: l2)
    | subseq_common x l1 l2 :
        subseq l1 l2 ->
        subseq (x :: l1) (x :: l2).
  Hint Constructors subseq.

  Lemma subseq_nil l : subseq nil l.
  Proof. induction l; eauto. Qed.

  Lemma subseq_tl l l2 :
    subseq l l2 ->
    forall x l1, l = x :: l1 ->
    subseq l1 l2.
  Proof. induction 1; inversion 1; subst; eauto. Qed.

  Hint Resolve subseq_nil subseq_tl.

  Fixpoint LCS_body LCS x l2 :=
    match l2 with
    | nil => nil
    | y :: l2' =>
        if X_eq_dec x y then x :: LCS l2'
        else
          let s1 := LCS (y :: l2') in
          let s2 := LCS_body LCS x l2' in
          if le_ge_dec (length s1) (length s2) then s2 else s1
    end.

  Fixpoint LCS l1 l2 :=
    match l1 with
    | nil => nil
    | x :: l1' => LCS_body (LCS l1') x l2
    end.

  Lemma LCS_rect (P : list X -> list X -> Type) (Q : X -> list X -> list X -> Type) :
    (forall l2, P nil l2) ->
    (forall x l1 l2, Q x l1 l2 -> P (x :: l1) l2) ->
    (forall x l1, Q x l1 nil) ->
    (forall x l1 y l2, P l1 l2 -> P l1 (y :: l2) -> Q x l1 l2 -> Q x l1 (y :: l2)) ->
    forall l1 l2, P l1 l2.
  Proof.
    intros ? IH2 ? ? l1.
    induction l1; intros l2; eauto.
    - apply IH2.
      induction l2; eauto.
  Qed.

  Theorem LCS_subseq : forall l1 l2, subseq (LCS l1 l2) l1 /\ subseq (LCS l1 l2) l2.
  Proof.
    refine (LCS_rect _
      (fun x l1 l2 =>
         subseq (LCS_body (LCS l1) x l2) (x :: l1) /\ subseq (LCS_body (LCS l1) x l2) l2) _ _ _ _); simpl; eauto.
    intros x l1 y l2 [? ?] [? ?] [? ?].
    destruct (X_eq_dec x y); subst; eauto.
    destruct (le_ge_dec (length (LCS l1 (y :: l2))) (length (LCS_body (LCS l1) x l2))); eauto.
  Qed.

  Theorem LCS_longest : forall l1 l2 l,
    subseq l l1 ->
    subseq l l2 ->
    length l <= length (LCS l1 l2).
  Proof.
    Local Hint Resolve le_n_S.
    refine (LCS_rect _
      (fun x l1 l2 => forall l,
        subseq l (x :: l1) ->
        subseq l l2 ->
        length l <= length (LCS_body (LCS l1) x l2)) _ _ _ _); simpl; eauto.
    - inversion 1; simpl; eauto.
    - inversion 2; simpl; eauto.
    - intros x l1' y l2' ? IH2 IH3.
      destruct (X_eq_dec x y);
        [ subst | destruct (le_ge_dec (length (LCS l1' (y :: l2'))) (length (LCS_body (LCS l1') x l2'))) ];
        intros ? Hsubseq1 Hsubseq2;
        inversion Hsubseq1 as [ | ? ? ? Hsubseq1' | ]; subst;
        inversion Hsubseq2 as [ | ? ? ? Hsubseq2' | ]; subst;
        try specialize (IH2 _ Hsubseq1' Hsubseq2);
        try specialize (IH3 _ Hsubseq1 Hsubseq2');
        simpl in *;
        (congruence || omega || eauto).
  Qed.
End LCS.