(* -*- coq-prog-args: ("-emacs-U" "-R" "../monads" "); compile-command: "./makedoc.sh" -*- *)
(* begin hide *)
Set Implicit Arguments.
Unset Strict Implicit.
Require Export MyPrelude.
(* end hide *)
(** printing epsilon $\varepsilon$ *)(** printing cdot $\cdot$ *)
(** We first introduce the monoid laws we just described.
We will use the section mechanism of Coq extensively in the following.
Sections permit to write a bunch of definitions which are parameterized by some variables,
e.g. for types and operations.
When closing a section, every definition inside it is quantified over the variables it used.
*)
Section Monoid_Laws.
(** The carrier [m] type may be any type. *)
Variable m : Type.
(** The identity element [mempty] and the operation [mappend]. *)
Variables (mempty : m) (mappend : m -> m -> m).
(** We define fancy notations for the element and operation. *)
Notation epsilon := mempty.
Infix "cdot" := mappend (right associativity, at level 20).
(** We now state the properties. *)
Definition monoid_id_l_t : Prop := forall x, epsilon cdot x = x.
Definition monoid_id_r_t := forall x, x cdot epsilon = x.
Definition monoid_assoc_t := forall x y z, (x cdot y) cdot z = x cdot y cdot z.
End Monoid_Laws.
(** Every variable in [Monoid_Laws] has been discharged by now, so we must apply each definition
to particular [mempty] and [mappend] objects.
We can finally define the dependent record which represents monoids on [m]:
%\label{def:monoid}%
*)
Record monoid (m : Type) : Type := mkMonoid
{ mempty : m ; mappend : m -> m -> m
; monoid_id_l : monoid_id_l_t mempty mappend
; monoid_id_r : monoid_id_r_t mempty mappend
; monoid_assoc : monoid_assoc_t mappend }.
(* begin hide *)
(* Notation " x 'cdot' y " := (monoid_append _ x y) (right associativity, at level 20). *)
(* Notation " 'varepsilon' " := (monoid_empty _) (no associativity, at level 20). *)
Hint Unfold monoid_id_l_t monoid_id_r_t monoid_assoc_t.
Require Import Plus.
Ltac monoid_tac_in H := repeat rewrite monoid_id_r in H ; repeat rewrite monoid_id_l in H ; repeat rewrite monoid_assoc in H.
Ltac monoid_tac := repeat rewrite monoid_id_r ; repeat rewrite monoid_id_l ; repeat rewrite monoid_assoc.
(* end hide *)