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

Require Export Prelude.Basics.
Require Import Prelude.Properties.

Class Monoid (m : Setoid) := {
  mempty : m ;
  mappend : m ---> m ---> m ;

  mappend_mempty_left :> left_neutral mappend mempty ;
  mappend_mempty_right :> right_neutral mappend mempty ;

  mappend_assoc :> associative  mappend
}.

Notation " x <+> y " := (mappend x y) (right associativity, at level 20) : monoid.
Notation ε := mempty.

Arguments Scope Monoid [ type_scope _ _ ].

Hint Unfold left_neutral right_neutral associative : monoid.
(* Hint Rewrite @mappend_mempty_left @mappend_mempty_right @mappend_assoc : monoid. *)
(* Hint Rewrite @left_neutrality @right_neutrality @associativity : monoid. *)
Hint Rewrite (@mappend_mempty_left : forall (m : Setoid) (Monoid : Monoid m) (x : m),
                mappend ε x === x) : monoid.
Hint Rewrite (@mappend_mempty_right : forall (m : Setoid) (Monoid : Monoid m) (x : m),
                mappend x ε === x) : monoid.
Hint Rewrite (@mappend_assoc : forall `(M : Monoid m) (x₁ x₂ x₃ : m),
                mappend x₁ (mappend x₂ x₃) === mappend (mappend x₁ x₂) x₃) : monoid.

Require Import Plus.

Program Instance nat_monoid : Monoid (eq_setoid nat) :=
{ mempty := 0 ; mappend := mkMap2 plus }.

  Next Obligation.
    program_simpl; repeat intro; auto.
  Qed.

  Solve Obligations using red ; program_simpl ; autorewrite with monoid ;
    red ; auto with arith.


Require Import Product.

Program Instance prod_monoid `{Monoid A} `{Monoid B} : Monoid (prod_setoid A B) := {
  mempty := pairS mempty mempty ;
  mappend := mkMap2
    (fun x y =>
      let (xl, xr) := x in
      let (yl, yr) := y in
        (mappend xl yl, mappend xr yr))
}.

  Next Obligation.
    repeat intro. program_simpl. destruct H1. destruct H2. 
    constructor; simpl in *; [rewrite H1, H2 | rewrite H3, H4]; reflexivity.
  Qed.

  Solve Obligations using red ; program_simpl ; autorewrite with monoid ; reflexivity.