| Time-stamp: "02/08/09 12:45:03 maggesi" |
Require Export misc.
Implicit Arguments On.
Record Monoid_Theory [A:Type; op:A->A->A; id:A] : Prop := {
monoid_assoc : (x,y,z:A)(op x (op y z))==(op (op x y) z);
monoid_sx_id : (x:A)(op id x)==x;
monoid_dx_id : (x:A)(op x id)==x
}.
Hints Resolve Build_Monoid_Theory : mnd.
Record Monoid_Morph_Theory [
A:Type; Aop:A->A->A; Aid:A;
B:Type; Bop:B->B->B; Bid:B; f:A->B] : Prop := {
monoid_morph_op : (x,y:A)(f (Aop x y))==(Bop (f x) (f y));
monoid_morph_id : (f Aid)==Bid
}.
Record Monoid_Data : Type := {
monoid_carrier :> Type;
mop : monoid_carrier->monoid_carrier->monoid_carrier;
mid : monoid_carrier
}.
Syntactic Definition is_a_monoid := [MD:Monoid_Data]
(Monoid_Theory (!mop MD) (mid MD)).
Record Monoid : Type := {
monoid_data :> Monoid_Data;
monoid_theory :> (is_a_monoid monoid_data)
}.
Hints Resolve monoid_theory : mnd.
Syntactic Definition is_a_monoid_morph := [AD,BD:Monoid_Data; f:AD->BD]
(Monoid_Morph_Theory (!mop AD) (mid AD) (!mop BD) (mid BD) f).
Record Monoid_Morph [A,B:Monoid_Data] : Type := {
monoid_morph_carrier :> A->B;
monoid_morph_theory : (is_a_monoid_morph A B monoid_morph_carrier)
}.
Hints Resolve monoid_morph_theory : mnd.