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

Fixpoint before_all {A : Type} (x : A) y l : Prop :=
  match l with
    | [] => True
    | a :: l' => 
      ~ In x l' \/ 
      (y <> a /\ before_all x y l')
  end.

Section before_all.
  Variable A : Type.

  Lemma before_all_head_not_in :
    forall l (x y : A),
      x <> y ->
      before_all x y (y :: l) ->
      ~ In x l.
  Proof using.
(* Goal: forall (x y : A) (_ : not (@In A y (@cons A a l))), @before_all A x y (@cons A a l) *)
    intros.
(* Goal: @before_all A x y (@cons A a l) *)
    simpl in *.
(* Goal: False *)
    break_or_hyp; auto.
(* Goal: or (not (@In A x (@app A l (@cons A a0 (@nil A))))) (and (not (@eq A y a)) (@before_all A x y (@app A l (@cons A a0 (@nil A))))) *)
    break_and. auto.
  Qed.

  Lemma before_all_neq_append : 
  forall l (x y a : A),
    a <> x ->
    before_all x y l ->
    before_all x y (l ++ [a]).
  Proof using.
(* Goal: forall (l : list A) (x y : A) (_ : not (@In A y l)), @before_all A x y l *)
  induction l.
(* Goal: True *)
  - intros; left; auto.
  - intros;
(* Goal: @before_all A x y (@cons A a l) *)
    simpl in *.
(* Goal: or (not (@In A x (@app A l (@cons A a0 (@nil A))))) (and (not (@eq A y a)) (@before_all A x y (@app A l (@cons A a0 (@nil A))))) *)
    break_or_hyp.
    * left.
(* Goal: not (@In A x (@app A l (@cons A a0 (@nil A)))) *)
      intro H_in.
(* Goal: False *)
      do_in_app.
(* Goal: False *)
      break_or_hyp; auto.
(* Goal: @before_all A x y (@cons A a l) *)
      simpl in *.
(* Goal: False *)
      break_or_hyp; auto.
(* Goal: or (not (@In A x (@app A l (@cons A a0 (@nil A))))) (and (not (@eq A y a)) (@before_all A x y (@app A l (@cons A a0 (@nil A))))) *)
    * break_and.
(* Goal: or (not (@In A x (@app A l (@cons A a0 (@nil A))))) (and (not (@eq A y a)) (@before_all A x y (@app A l (@cons A a0 (@nil A))))) *)
      right.
(* Goal: True *)
      split; auto.
  Qed.

  Lemma before_all_not_in_1 :
    forall l (x y : A),
      ~ In x l ->
      before_all x y l.
  Proof using.
(* Goal: forall (x y : A) (_ : not (@In A y (@cons A a l))), @before_all A x y (@cons A a l) *)
    intros.
(* Goal: True *)
    destruct l; simpl in *; auto.
  Qed.

  Lemma before_all_not_in_2 :
    forall l (x y : A),
      ~ In y l ->
      before_all x y l.
  Proof using.
(* Goal: forall (l : list A) (x y : A) (_ : not (@In A y l)), @before_all A x y l *)
    induction l.
(* Goal: forall (x y : A) (_ : not (@In A y (@cons A a l))), @before_all A x y (@cons A a l) *)
    - intros. simpl in *. auto.
(* Goal: forall (x y : A) (_ : not (@In A y (@cons A a l))), @before_all A x y (@cons A a l) *)
    - intros. simpl in *.
(* Goal: True *)
      assert (H_neq: y <> a); auto.
(* Goal: True *)
      assert (H_in: ~ In y l); auto.
   Qed.
End before_all.
