(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(* Certified Haskell Prelude.
 * Author: Matthieu Sozeau
 * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
 *              91405 Orsay, France *)

(* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)

Require Import Prelude.Basics.
Require Import Prelude.Functor.
Require Import Datatypes.

Require Export Coq.Lists.List.
Require Export Coq.Lists.SetoidList.

Open Local Scope list_scope.

Hint Unfold id compose : list.
Hint Unfold map : list.

Obligation Tactic := try typeclasses eauto || simpl_relation ||
  program_simpl.

Print Hint Equivalence.
  
Instance cons_mor `{E : Equivalence α eqα} : Proper (eqα ==> eqlistA eqα ==> eqlistA eqα) cons.
Proof. intros. simpl_morph. constructor ; auto. Qed.

Program Definition list_setoid (α : Setoid) : Setoid :=
  mkSetoid _ (eqlistA (@Basics.seq α)) _.

Instance map_morphism `(Equivalence A eqA, Equivalence B eqB) :
  Proper ((eqA ==> eqB) ==> eqlistA eqA ==> eqlistA eqB) (@map A B).
Proof.
  intros. do 3 red. intros f g Hfg.
  induction 1 ; simpl ; intros ; constructor ; auto.
Qed.

Implicit Arguments map [[A] [B]].
Typeclasses Opaque map.

Lemma map_id {A} l : map (@id A) l = l.
Proof. intros A l. induction l. simpl. reflexivity.
  simpl. rewrite IHl. reflexivity.
Qed.

Lemma map_compose {A B C} (g : B -> C) (f : A -> B) l : map (g ∘ f) l = (map g ∘ map f) l.
Proof. intros A B C g f l. induction l. simpl. reflexivity.
  simpl. rewrite IHl. reflexivity.
Qed.

Program Instance list_functor : Functor list_setoid :=
  { fmap α β := mkMap2 map }.

  Next Obligation.
  Proof. simpl in *. rewrite H, H0 ; reflexivity. Qed.

  Next Obligation.
  Proof. rewrite map_compose. reflexivity. Qed.
    
  Next Obligation.
  Proof. now rewrite map_id. Qed.

Implicit Arguments app [[A]].

Instance app_morphism `(E : Equivalence A eqA) :
  Proper (eqlistA eqA ==> eqlistA eqA ==> eqlistA eqA) app.
Proof.
  intros. do 3 red.
  induction 1 ; simpl ; auto.
Qed.

Instance app_ass A : Associative eq (@app A).
Proof. red. intros. induction x ; simpl ; auto with list.
  reflexivity.
  rewrite IHx. reflexivity.
Qed.

Instance app_rn : Neutral eq app (@nil A).
Proof. constructor ; simpl ; auto. 
  reduce. reflexivity.
  do 3 red. intros. induction x ; simpl.
  reflexivity.
  unfold flip, const in *. simpl.
  rewrite IHx. reflexivity.
Qed.

Require Import Equations.

Equations(nocomp) concat {A} (l : list (list A)) : list A :=
concat A nil := nil ;
concat A (cons x xs) := x ++ concat xs.

(* Fixpoint concat {A} (l : list (list A)) : list A := *)
(*   match l with *)
(*     | hd :: tl => app hd (concat tl) *)
(*     | nil => nil *)
(*   end. *)

Instance concat_morphism `{E : Equivalence A eqA} :
  Proper (eqlistA (eqlistA eqA) ==> eqlistA eqA) concat.
Proof.
  intros. do 2 red. induction 1; simp concat ; auto.

  now rewrite IHeqlistA, H.
Qed.

Program Definition concatS {A} : list_setoid (list_setoid A) --> list_setoid A := mkMap concat.
 
  Next Obligation. simpl in *. now rewrite H. Qed.

Lemma concat_app : forall `{E : Equivalence A eqA}  (l l' : list (list A)), 
  concat (l ++ l') === concat l ++ concat l'.
Proof.
  induction l ; simpl; intros; simp concat ; auto.
  reflexivity.   unfold Equivalence.equiv in *.
  rewrite (IHl l').
  setoid_rewrite (assoc (f:=app)). reflexivity.
Qed.
    
Program Definition concat_map {A B} (f : A --> list_setoid B) := concatS ∘ fmap f.

Hint Unfold concat_map : datatypes.

Ltac tc tac :=
  tac ; eauto with typeclass_instances.

Tactic Notation "rew" ident(t) :=
  tc ltac:(setoid_rewrite @t).

Open Local Scope signature_scope.

(* Program Instance equiv_refl [ sa : Equivalence A ] : Reflexive Equivalence.equiv. *)

Lemma map_app {A} `{Equivalence B eqB} (f : A -> B) (l l' : list A) : map f (l ++ l') === map f l ++ map f l'.
Proof.
  intros until l.
  induction l; simpl ; auto.

  reflexivity.

  intros.
  constructor ; try reflexivity ; auto.
  apply IHl.
Qed.

Hint Unfold concat_map : list.
Hint Unfold concat : list.

Definition tip {A} (x : A) : list A :=
  x :: nil.

Instance tip_proper {A : Setoid} : Proper (A ==> list_setoid A) (@tip A).
Proof. intros. unfold tip. simpl_morph. Qed.

Program Definition tipS {A} : A ---> list_setoid A := mkMap (@tip A).

Program Instance list_pointed : ! Pointed list_setoid :=
  { point α := tipS }.
  
  Next Obligation.
  Proof. reflexivity. Qed.