Require Import List.
Import ListNotations.
Require Import StructTact.StructTactics.

Set Implicit Arguments.

Fixpoint Prefix {A} (l1 : list A) l2 : Prop :=
  match l1, l2 with
    | a :: l1', b :: l2' => a = b /\ Prefix l1' l2'
    | [], _ => True
    | _, _ => False
  end.

Section prefix.
  Variable A : Type.

  Lemma Prefix_refl :
    forall (l : list A),
      Prefix l l.
  Proof using.
(* Goal: forall (x : A) (_ : @In A x (@cons A a0 l')), @In A x (@cons A a l) *)
    intros. induction l; simpl in *; auto.
  Qed.

  Lemma Prefix_nil :
    forall (l : list A),
      Prefix l [] ->
      l = [].
  Proof using.
(* Goal: forall (x : A) (_ : @In A x (@cons A a0 l')), @In A x (@cons A a l) *)
    intros. destruct l.
    - reflexivity.
    - contradiction.
  Qed.

  Lemma Prefix_cons :
    forall (l l' : list A) a,
      Prefix l' l ->
      Prefix (a :: l') (a :: l).
  Proof using.
(* Goal: forall (l l' : list A) (a : A) (_ : @Prefix A l' l), @Prefix A (@cons A a l') (@cons A a l) *)
    simpl. intuition.
  Qed.

  Lemma Prefix_in :
    forall (l l' : list A),
      Prefix l' l ->
      forall x, In x l' -> In x l.
  Proof using.
(* Goal: forall (l l' : list A) (_ : @Prefix A l' l) (x : A) (_ : @In A x l'), @In A x l *)
    induction l; intros l' H.
    - find_apply_lem_hyp Prefix_nil. subst. contradiction.
    - destruct l'.
(* Goal: forall (x : A) (_ : @In A x (@nil A)), @In A x (@cons A a l) *)
      + contradiction.
(* Goal: forall (x : A) (_ : @In A x (@cons A a0 l')), @In A x (@cons A a l) *)
      + intros. simpl Prefix in *. break_and. subst. simpl in *. intuition.
(* Goal: or (@eq A a x) (@In A x l) *)
        right. eapply IHl; eauto.
  Qed.

  Lemma app_Prefix :
    forall (xs ys zs : list A),
      xs ++ ys = zs ->
      Prefix xs zs.
  Proof using.
(* Goal: @In A x (@cons A a l) *)
    induction xs; intros; simpl in *.
    - auto.
    - break_match.
      + discriminate.
(* Goal: @eq (list A) (@cons A a0 l) (@cons A a0 (@app A l1 x)) *)
      + subst. find_inversion. eauto.
  Qed.

  Lemma Prefix_In :
    forall (l : list A) l' x,
      Prefix l l' ->
      In x l ->
      In x l'.
  Proof using.
    induction l; intros; simpl in *; intuition;
(* Goal: or (@eq A a x) (@In A x l) *)
      subst; break_match; intuition; subst; intuition.
  Qed.

  Lemma Prefix_exists_rest :
    forall (l1 l2 : list A),
      Prefix l1 l2 ->
      exists rest,
        l2 = l1 ++ rest.
  Proof using.
(* Goal: @eq (list A) (@cons A a0 (@app A l1 x)) (@cons A a0 (@app A l1 x)) *)
    induction l1; intros; simpl in *; eauto.
(* Goal: or (@eq A a x) (@In A x l) *)
    break_match; intuition. subst.
(* Goal: @ex (list A) (fun rest : list A => @eq (list A) (@cons A a0 l) (@cons A a0 (@app A l1 rest))) *)
    find_apply_hyp_hyp.
(* Goal: @eq (list A) (@cons A a0 l) (@cons A a0 (@app A l1 x)) *)
    break_exists_exists. subst. auto.
  Qed.
End prefix.
