Require Import Coq.Lists.List.
Require Coq.Classes.EquivDec.
Require Import ExtLib.Core.Type.
Require Import ExtLib.Core.RelDec.
Require Import ExtLib.Structures.Monoid.
Require Import ExtLib.Structures.Reducible.
Require ExtLib.Data.Nat.
Require Import ExtLib.Tactics.Consider.
Require Import ExtLib.Tactics.Injection.

Set Implicit Arguments.
Set Strict Implicit.

Section type.
  Variable T : Type.
  Context {type_T : type T}.

  Inductive list_eq : list T -> list T -> Prop :=
  | nil_eq : list_eq nil nil
  | cons_eq : forall x xs y ys, equal x y -> list_eq xs ys -> list_eq (x :: xs) (y :: ys).

  Instance type_list : type (list T) :=
(* Goal: iff (@Forall U P (@cons U (f a) (@map T U f ls))) (@Forall T (fun x : T => P (f x)) (@cons T a ls)) *)
  { equal := list_eq
  ; proper := Forall proper
  }.

  Context {typeOk_T : typeOk type_T}.

  Instance typeOk_list : typeOk type_list.
  Proof.
(* Goal: @well_founded (list T) (@R_list_len T) *)
    constructor.
(* Goal: iff (@Forall U P (@cons U (f a) (@map T U f ls))) (@Forall T (fun x : T => P (f x)) (@cons T a ls)) *)
    { intros. induction H.
(* Goal: @well_founded (list T) (@R_list_len T) *)
      { intuition; constructor. }
(* Goal: iff (@Forall U P (@cons U (f a) (@map T U f ls))) (@Forall T (fun x : T => P (f x)) (@cons T a ls)) *)
      { apply only_proper in H; auto. intuition; constructor; intuition. } }
(* Goal: iff (@Forall U P (@cons U (f a) (@map T U f ls))) (@Forall T (fun x : T => P (f x)) (@cons T a ls)) *)
    { intro. induction x; intros.
(* Goal: @well_founded (list T) (@R_list_len T) *)
      { constructor. }
(* Goal: iff (@Forall U P (@cons U (f a) (@map T U f ls))) (@Forall T (fun x : T => P (f x)) (@cons T a ls)) *)
      { inversion H; clear H; subst.
        constructor; auto.
        apply equiv_prefl; auto. apply IHx. apply H3. } }
(* Goal: iff (@Forall U P (@cons U (f a) (@map T U f ls))) (@Forall T (fun x : T => P (f x)) (@cons T a ls)) *)
    { intro. induction 1; constructor; auto.
      apply equiv_sym; auto. }
(* Goal: iff (@Forall U P (@cons U (f a) (@map T U f ls))) (@Forall T (fun x : T => P (f x)) (@cons T a ls)) *)
    { intro. do 3 intro.  revert z. induction H.
(* Goal: @well_founded (list T) (@R_list_len T) *)
      { remember nil. destruct 1; try congruence. constructor. }
(* Goal: iff (@Forall U P (@cons U (f a) (@map T U f ls))) (@Forall T (fun x : T => P (f x)) (@cons T a ls)) *)
      { remember (y :: ys). destruct 1; try congruence. inversion Heql; clear Heql; subst.
(* Goal: @well_founded (list T) (@R_list_len T) *)
        constructor. eapply equiv_trans; eauto. eapply IHlist_eq. apply H2. } }
  Qed.
End type.

Section EqDec.
  Variable T : Type.
  Variable EqDec_T : EquivDec.EqDec _ (@eq T).

  Global Instance EqDec_list : EquivDec.EqDec _ (@eq (list T)).
  Proof.
(* Goal: @EquivDec.EqDec (list T) (@eq (list T)) (@RelationClasses.eq_equivalence (list T)) *)
    red. unfold Equivalence.equiv, RelationClasses.complement.
(* Goal: forall (F : forall _ : T, Type) (val : list (F a)), @eq (list (F a)) val (@map (F a) (F a) (fun val0 : F a => val0) val) *)
    intros.
(* Goal: sumbool (@eq (list T) x y) (forall _ : @eq (list T) x y, False) *)
    change (x = y -> False) with (x <> y).
(* Goal: sumbool (@eq (list T) x y) (not (@eq (list T) x y)) *)
    decide equality. eapply EqDec_T.
  Qed.
End EqDec.

(* Specialized induction rules *)
Lemma list_ind_singleton
(* Goal: iff (@Forall U P (@cons U (f a) (@map T U f ls))) (@Forall T (fun x : T => P (f x)) (@cons T a ls)) *)
: forall {T : Type} (P : list T -> Prop)
         (Hnil : P nil)
         (Hsingle : forall t, P (t :: nil))
         (Hcons : forall t u us, P (u :: us) -> P (t :: u :: us)),
    forall ls, P ls.
Proof.
(* Goal: forall (T : Type) (P : forall _ : list T, Prop) (_ : P (@nil T)) (_ : forall t : T, P (@cons T t (@nil T))) (_ : forall (t u : T) (us : list T) (_ : P (@cons T u us)), P (@cons T t (@cons T u us))) (ls : list T), P ls *)
  induction ls; eauto.
(* Goal: P (@cons T a ls) *)
  destruct ls. eauto. eauto.
Qed.

Lemma list_rev_ind
  : forall T (P : list T -> Prop),
    P nil ->
    (forall l ls, P ls -> P (ls ++ l :: nil)) ->
    forall ls, P ls.
Proof.
(* Goal: forall (F : forall _ : T, Type) (val : list (F a)), @eq (list (F a)) val (@map (F a) (F a) (fun val0 : F a => val0) val) *)
  clear. intros. rewrite <- rev_involutive.
(* Goal: P (@rev T (@rev T ls)) *)
  induction (rev ls).
(* Goal: P (@rev T (@nil T)) *)
(* Goal: P (@rev T (@cons T a l)) *)
  apply H.
(* Goal: P (@rev T (@cons T a l)) *)
  simpl. auto.
Qed.

Section AllB.
  Variable T : Type.
  Variable p : T -> bool.

  Fixpoint allb (ls : list T) : bool :=
    match ls with
      | nil => true
      | l :: ls =>
        if p l then allb ls else false
    end.

  Fixpoint anyb (ls : list T) : bool :=
    match ls with
      | nil => false
      | l :: ls =>
        if p l then true else anyb ls
    end.
End AllB.

Lemma Forall_map
: forall T U (f : T -> U) P ls,
    Forall P (List.map f ls) <-> Forall (fun x => P (f x)) ls.
Proof.
(* Goal: P (@rev T (@cons T a l)) *)
  induction ls; simpl.
(* Goal: @well_founded (list T) (@R_list_len T) *)
  { split; intros; constructor. }
(* Goal: iff (@Forall U P (@cons U (f a) (@map T U f ls))) (@Forall T (fun x : T => P (f x)) (@cons T a ls)) *)
  { split; inversion 1; intros; subst; constructor; auto.
    apply IHls. auto. apply IHls. auto. }
Qed.

Lemma Forall_cons_iff : forall (T : Type) (P : T -> Prop) a b,
    Forall P (a :: b) <-> (P a /\ Forall P b).
(* Goal: forall (T : Type) (P : forall _ : T, Prop), iff (@Forall T P (@nil T)) True *)
Proof. clear. split.
(* Goal: forall _ : @eq (list T) (@nil T) (@nil T), True *)
       inversion 1; auto.
       destruct 1; constructor; auto.
Qed.

Lemma Forall_nil_iff : forall (T : Type) (P : T -> Prop),
    Forall P nil <-> True.
Proof.
(* Goal: forall (T : Type) (P : forall _ : T, Prop), iff (@Forall T P (@nil T)) True *)
  clear. split; auto.
Qed.


(* Goal: iff (@Forall U P (@cons U (f a) (@map T U f ls))) (@Forall T (fun x : T => P (f x)) (@cons T a ls)) *)
Global Instance Foldable_list {T} : Foldable (list T) T :=
  fun _ f x ls => fold_right f x ls.

Require Import ExtLib.Structures.Traversable.
Require Import ExtLib.Structures.Functor.
Require Import ExtLib.Structures.Monad.
Require Import ExtLib.Structures.Applicative.

Section traversable.
(* Goal: iff (@Forall U P (@cons U (f a) (@map T U f ls))) (@Forall T (fun x : T => P (f x)) (@cons T a ls)) *)
  Polymorphic Context {F : Type -> Type}.
(* Goal: iff (@Forall U P (@cons U (f a) (@map T U f ls))) (@Forall T (fun x : T => P (f x)) (@cons T a ls)) *)
  Polymorphic Context {Applicative_F : Applicative F}.
(* Goal: iff (@Forall U P (@cons U (f a) (@map T U f ls))) (@Forall T (fun x : T => P (f x)) (@cons T a ls)) *)
  Polymorphic Context {A B : Type}.
  Polymorphic Variable f : A -> F B.

  Polymorphic Fixpoint mapT_list (ls : list A) : F (list B) :=
    match ls with
      | nil => pure nil
      | l :: ls => ap (ap (pure (@cons B)) (f l)) (mapT_list ls)
    end.
End traversable.

Global Instance Traversable_list : Traversable list :=
(* Goal: iff (@Forall U P (@cons U (f a) (@map T U f ls))) (@Forall T (fun x : T => P (f x)) (@cons T a ls)) *)
{ mapT := @mapT_list }.

Global Instance Monad_list : Monad list :=
(* Goal: iff (@Forall U P (@cons U (f a) (@map T U f ls))) (@Forall T (fun x : T => P (f x)) (@cons T a ls)) *)
{ ret  := fun _ x => x :: nil
; bind := fun _ _ x f =>
  List.fold_right (fun x acc => f x ++ acc) nil x
}.



Section list.
(* Goal: iff (@Forall U P (@cons U (f a) (@map T U f ls))) (@Forall T (fun x : T => P (f x)) (@cons T a ls)) *)
  Inductive R_list_len {T} : list T -> list T -> Prop :=
  | R_l_len : forall n m, length n < length m -> R_list_len n m.

  Theorem wf_R_list_len T : well_founded (@R_list_len T).
  Proof.
(* Goal: @well_founded (list T) (@R_list_len T) *)
    constructor. intros.
    refine (@Fix _ _ Nat.wf_R_lt (fun n : nat => forall ls : list T, n = length ls -> Acc R_list_len ls)
      (fun x rec ls pfls => Acc_intro _ _)
      _ _ refl_equal).
    refine (
      match ls as ls return x = length ls -> forall z : list T, R_list_len z ls -> Acc R_list_len z with
        | nil => fun (pfls : x = 0) z pf => _
        | cons l ls => fun pfls z pf =>
          rec _ (match pf in R_list_len xs ys return x = length ys -> Nat.R_nat_lt (length xs) x with
                   | R_l_len n m pf' => fun pf_eq => match eq_sym pf_eq in _ = x return Nat.R_nat_lt (length n) x with
                                                     | refl_equal => Nat.R_lt pf'
                                                   end
                 end pfls) _ eq_refl
      end pfls).
(* Goal: @Acc (list T) (@R_list_len T) z *)
    clear - pf; abstract (inversion pf; subst; simpl in *; inversion H).
  Defined.
End list.

(* Goal: iff (@Forall U P (@cons U (f a) (@map T U f ls))) (@Forall T (fun x : T => P (f x)) (@cons T a ls)) *)
Definition Monoid_list_app {T} : Monoid (list T) :=
(* Goal: iff (@Forall U P (@cons U (f a) (@map T U f ls))) (@Forall T (fun x : T => P (f x)) (@cons T a ls)) *)
{| monoid_plus := @List.app _
 ; monoid_unit := @nil _
 |}.

Section ListEq.
  Variable T : Type.
  Variable EDT : RelDec (@eq T).

  Fixpoint list_eqb (ls rs : list T) : bool :=
    match ls , rs with
      | nil , nil => true
      | cons l ls , cons r rs =>
        if l ?[ eq ] r then list_eqb ls rs else false
      | _ , _ => false
    end.

  (** Specialization for equality **)
  Global Instance RelDec_eq_list : RelDec (@eq (list T)) :=
(* Goal: iff (@Forall U P (@cons U (f a) (@map T U f ls))) (@Forall T (fun x : T => P (f x)) (@cons T a ls)) *)
  { rel_dec := list_eqb }.

  Variable EDCT : RelDec_Correct EDT.

  Global Instance RelDec_Correct_eq_list : RelDec_Correct RelDec_eq_list.
  Proof.
    constructor; induction x; destruct y; split; simpl in *; intros;
      repeat match goal with
               | [ H : context [ rel_dec ?X ?Y ] |- _ ] =>
                 consider (rel_dec X Y); intros; subst
               | [ |- context [ rel_dec ?X ?Y ] ] =>
                 consider (rel_dec X Y); intros; subst
             end; try solve [ auto | exfalso; clear - H; inversion H ].
    - f_equal. eapply IHx. eapply H0.
    - inversion H. subst. eapply IHx. reflexivity.
    - inversion H. exfalso. eapply H0. assumption.
  Qed.

End ListEq.

Global Instance Injective_cons T (a : T) b c d : Injective (a :: b = c :: d).
(* Goal: iff (@Forall U P (@cons U (f a) (@map T U f ls))) (@Forall T (fun x : T => P (f x)) (@cons T a ls)) *)
refine {| result := a = c /\ b = d |}.
(* Goal: forall _ : @eq (list T) (@nil T) (@nil T), True *)
inversion 1; auto.
Defined.

Global Instance Injective_cons_nil T (a : T) b : Injective (a :: b = nil).
(* Goal: iff (@Forall U P (@cons U (f a) (@map T U f ls))) (@Forall T (fun x : T => P (f x)) (@cons T a ls)) *)
refine {| result := False |}.
(* Goal: forall _ : @eq (list T) (@nil T) (@nil T), True *)
inversion 1; auto.
Defined.

Global Instance Injective_nil_cons T (a : T) b : Injective (nil = a :: b).
(* Goal: iff (@Forall U P (@cons U (f a) (@map T U f ls))) (@Forall T (fun x : T => P (f x)) (@cons T a ls)) *)
refine {| result := False |}.
(* Goal: forall _ : @eq (list T) (@nil T) (@nil T), True *)
inversion 1; auto.
Defined.

Global Instance Injective_nil_nil T : Injective (nil = @nil T).
(* Goal: iff (@Forall U P (@cons U (f a) (@map T U f ls))) (@Forall T (fun x : T => P (f x)) (@cons T a ls)) *)
refine {| result := True |}.
(* Goal: forall _ : @eq (list T) (@nil T) (@nil T), True *)
auto.
Defined.

(* Goal: iff (@Forall U P (@cons U (f a) (@map T U f ls))) (@Forall T (fun x : T => P (f x)) (@cons T a ls)) *)
Global Instance Injective_app_cons {T} (a : list T) b c d
: Injective (a ++ b :: nil = (c ++ d :: nil)).
Proof.
(* Goal: iff (@Forall U P (@cons U (f a) (@map T U f ls))) (@Forall T (fun x : T => P (f x)) (@cons T a ls)) *)
refine {| result := a = c /\ b = d |}.
(* Goal: forall _ : @eq (list T) (@app T a (@cons T b (@nil T))) (@app T c (@cons T d (@nil T))), and (@eq (list T) a c) (@eq T b d) *)
eapply app_inj_tail.
Defined.

(* Goal: iff (@Forall U P (@cons U (f a) (@map T U f ls))) (@Forall T (fun x : T => P (f x)) (@cons T a ls)) *)
Global Instance Injective_app_same_L {T} (a : list T) b c
: Injective (b ++ a = b ++ c).
Proof.
(* Goal: iff (@Forall U P (@cons U (f a) (@map T U f ls))) (@Forall T (fun x : T => P (f x)) (@cons T a ls)) *)
refine {| result := a = c |}.
(* Goal: forall _ : @eq (list T) (@app T b a) (@app T b c), @eq (list T) a c *)
apply app_inv_head.
Defined.

(* Goal: iff (@Forall U P (@cons U (f a) (@map T U f ls))) (@Forall T (fun x : T => P (f x)) (@cons T a ls)) *)
Global Instance Injective_app_same_R {T} (a : list T) b c
: Injective (a ++ b = c ++ b).
Proof.
(* Goal: iff (@Forall U P (@cons U (f a) (@map T U f ls))) (@Forall T (fun x : T => P (f x)) (@cons T a ls)) *)
refine {| result := a = c |}.
(* Goal: forall _ : @eq (list T) (@app T a b) (@app T c b), @eq (list T) a c *)
apply app_inv_tail.
Defined.


Lemma eq_list_eq
: forall T (a b : T) (pf : a = b) (F : _ -> Type) val,
    match pf in _ = x return list (F x) with
      | eq_refl => val
    end = map (fun val => match pf in _ = x return F x with
                            | eq_refl => val
                          end) val.
Proof.
(* Goal: forall (F : forall _ : T, Type) (val : list (F a)), @eq (list (F a)) val (@map (F a) (F a) (fun val0 : F a => val0) val) *)
  destruct pf. intros. rewrite map_id. reflexivity.
Qed.
Hint Rewrite eq_list_eq : eq_rw.

Export Coq.Lists.List.
