(************************************************************************)
(*  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 $ *)

Set Implicit Arguments.
Unset Strict Implicit. 
Unset Printing Implicit Defensive.

Require Import Prelude.Basics.
Require Import Prelude.Functor.
Require Import RelationClasses.

Reserved Notation "f <*> e" (at level 65, left associativity).

Print point.
Print composeS.
  
Class Applicative `(F : Pointed f) := {
  
  ap : Π {α β}, f (α ---> β) ---> f α ---> f β where "f <*> e" := (ap f e);

  (* Properties *)
  applicative_functor : Π α β (f : α ---> β),
    fmap f == ap (point f) ;

  applicative_composition : Π α β δ
    (u : f (β ---> δ)) (v : f (α ---> β)) (w : f α),
    point composeM <*> u <*> v <*> w == u <*> (v <*> w) ;

  applicative_homomorphism : Π α β (f : α ---> β) x,
    point f <*> point x == point (f x) ;

  applicative_interchange : Π α β (u : f (α ---> β)) x,
    u <*> point x ==  point (applyM x) <*> u }.

Notation " f <*> e " := (ap f e).

Notation "'pure'" := point : applicative.
Open Local Scope applicative.

Lemma applicative_identity `{Applicative ν} {α} : ap (point idS) == (@idS (ν α)).
Proof.
  intros.
  setoid_rewrite <- applicative_functor.
  apply @fmap_id. 
Qed.

(* Instance pointwise_is_eq A B (R : relation B) : *)
(*   subrelation (@eq A ==> R)%signature (pointwise_relation R) | 5. *)
(* Proof. reduce. unfold pointwise_relation in *. subst ; apply H. reflexivity. Qed. *)

(* Instance eq_is_pointwise A B (R : relation B) : *)
(*   subrelation (pointwise_relation R) (@eq A ==> R)%signature | 5. *)
(* Proof. reduce. unfold pointwise_relation in *. subst ; apply H. Qed. *)

(* Instance eq_reflexive_subrelation `{Reflexive A R} : *)
(*   subrelation eq R. *)
(* Proof. simpl_relation. Qed. *)

Infix "<$>" := fmap (at level 50).

Print const.

Definition replace `{Functor f} {a b : Setoid} : a ---> f b ---> f a := 
  fmap ∙ constS.

Infix "<$" := replace (at level 50).

Section Applicative.
  Context `{applicative : Applicative f}.

  Section Lifts.

    Variable a b c d : Setoid.
    
    Definition liftA (g : a ---> b) (x : f a) : f b :=
      g <$> x.
    
    Definition liftA2 (g : a ---> b ---> c) (x : f a) (y : f b) : f c :=
      g <$> x <*> y.
    
    Definition liftA3 (g : a ---> b ---> c ---> d) (x : f a) (y : f b) (z : f c) : f d :=
      g <$> x <*> y <*> z.

  End Lifts.

  Variable a b : Setoid.

  Definition sequence_second : f a -> f b -> f b :=
    liftA2 (constS idS).

  Definition sequence_first : f a -> f b -> f a :=
    liftA2 constS.

  Definition reverse_ap : f a -> f (a ---> b) -> f b :=
    liftA2 applyM.

End Applicative.

Infix "*>" := sequence_second (at level 20).
Infix "<*" := sequence_first (at level 20).
Infix "<**>" := reverse_ap (at level 60).