(************************************************************************)
(*  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é Paris Sud
 *              91405 Orsay, France *)

(** Standard instances for the cartesian product.*)

Require Export Coq.Program.Basics.
Require Import Prelude.Functor.

Definition prod_eq (A B : Setoid) : relation (A * B) :=
  fun x y => fst x == fst y /\ snd x == snd y.

Program Instance: Equivalence (prod_eq A B).

  Next Obligation.
    constructor; reflexivity.
  Qed.
  Next Obligation.
    constructor; destruct H; symmetry; auto.
  Qed.
  Next Obligation.
    intros x y z Hxy Hyz.
    destruct Hxy; destruct Hyz; constructor;
      [transitivity (fst y) | transitivity (snd y)]; auto.
  Qed.

Program Definition prod_setoid (A B : Setoid) : Setoid :=
  {| car := A * B ; seq := prod_eq A B |}.

Instance pair_morphism (A B : Setoid) : Proper (A ==> B ==> (prod_setoid A B)) (@pair A B).
Proof. intros. simpl_morph. firstorder. Qed.

Program Definition pairS {A B:Setoid} : A ---> B ---> (prod_setoid A B) :=
  mkMap2 (@pair _ _).

Program Definition fstS {A B:Setoid} : (prod_setoid A B) ---> A :=
  mkMap (@fst _ _).

Program Definition sndS {A B:Setoid} : (prod_setoid A B) ---> B :=
  mkMap (@snd _ _).

Solve All Obligations using (program_simpl; intros x y H; destruct H; auto).

Program Instance prod_functor L : Functor (prod_setoid L) := {
  fmap A B := mkMap2 (fun f x => pairS (fstS x) (f (sndS x)))
}.

  Next Obligation.
    intros f g H_fun x y H.
    destruct H as [Hfst Hsnd]; constructor; auto; simpl.
    rewrite <- Hsnd; auto.
  Qed.

  Next Obligation.
    intro; destruct a as (x, y); reflexivity.
  Qed.
  Next Obligation.
    intro; destruct a as (x, y); reflexivity.
  Qed.

Require Import Prelude.CoMonad.

Program Instance prod_copointed L : CoPointed (prod_setoid L) := {
  extract α := sndS }.

  Next Obligation.
  Proof. intros [a b]. reflexivity. Qed.

Program Instance prod_comonad : CoMonad (prod_setoid A) := {
  duplicate α := mkMap (fun x =>
    let (l, r) := x in
      pairS l (pairS l r))
}.

  Next Obligation.
  Proof with simpl. 
    simpl_morph. destruct x as [x₁ x₂] ; destruct y as [y₁ y₂].
    red... firstorder.
  Qed.

  Next Obligation.
  Proof with simpl.
    simpl_morph. red. destruct x as [x₁ x₂]...
    firstorder auto with *.
  Qed.

  Next Obligation.
  Proof with simpl ; auto with *.
    intros [x₁ x₂]... red...
  Qed.

  Next Obligation.
  Proof with simpl ; auto with *.
    intros [x₁ x₂]... red...
  Qed.

  Next Obligation.
  Proof with simpl ; auto with *.
    intros [x₁ x₂]... unfold prod_eq...
    unfold prod_eq...
  Qed.

Definition askP {A B} : prod_setoid A B ---> A := fstS.

Program Definition localP {A B}
  : (A ---> A) ---> prod_setoid A B ---> prod_setoid A B :=
  mkMap2 (fun g x => (g (fst x), snd x)).

  Next Obligation.
    intros f g Hfun x y H.
    destruct x as [x1 x2]; destruct y as [y1 y2]; destruct H as [Hfst Hsnd].
    simpl in *.
    constructor; simpl; repeat (rewrite Hfst || rewrite Hsnd || rewrite Hfun);
      reflexivity.
  Qed.