Library additions.Monoid_def

From Coq Require Import RelationClasses Relations Morphisms String.

Set Implicit Arguments.

The Monoid type class (with Operational Type Classes)

Declare Scope M_scope.

Class Mult_op (A:Type) := mult_op : A → A → A.

Print Mult_op.

Print mult_op.

Goal ∀ A (op : Mult_op A ), @mult_op A op = op.

Delimit Scope M_scope with M.
Infix "×" := mult_op : M_scope.
Open Scope M_scope.

Module Demo.

  #[local] Instance nat_mult_op : Mult_op nat := Nat.mul.

  Set Printing All.

  Check 3 × 4.

   Unset Printing All.

End Demo.

#[ global ] Instance string_op : Mult_op string := append.
Open Scope string_scope.

Example ex_string : "ab" × "cde" = "abcde".

#[ global ] Instance bool_and_binop : Mult_op bool := andb.

Example ex_bool : true × false = false.

within M_scope, a term of the form (x * y) is an abbreviation of (mult_op A op x y) where op : Mult_op A and x, y : A.

Class Monoid {A:Type}(op : Mult_op A)(one : A) : Prop :=
{
    op_assoc : ∀ x y z, x × (y × z ) = x × y × z;
    one_left : ∀ x, one × x = x;
    one_right : ∀ x, x × one = x
}.

Exercice

Define a class for semi-groups, and re-define monoids as semi-groups with a neutral element

Monoids and Equivalence Relations

In some situations, the previous definition may be too restrictive. For instance, consider the computation of where and are positive integers, and .

Although it could possible to compute with values of the dependent type {n:N | n < m}, it looks simpler to compute with numbers of type N, and consider the multiplication .

It is easy to prove that this operation is associative, using library . Unfortunately, it is not possible to prove the following proposition, required for building an instance of Monoid:

∀ x:N, 1 × x mod m = x.

Thus, we define a more general class, parameterized by an equivalence relation Aeq on type A, compatible with the multiplication . The laws of associativity and neutral element are not expressed as Leibniz equalities but as equivalence statements:

Class Equiv A := equiv : relation A.

Infix "==" := equiv (at level 70) : type_scope.

Class EMonoid (A:Type)(E_op : Mult_op A)(E_one : A)
      (E_eq: Equiv A): Prop :=
  {
    Eq_equiv :> Equivalence equiv;
    Eop_proper : Proper (equiv ==> equiv ==> equiv) E_op;
    Eop_assoc : ∀ x y z, x × (y × z ) == x × y × z;
    Eone_left : ∀ x, E_one × x == x;
    Eone_right : ∀ x, x × E_one == x
  }.

#[ global ] Instance Equiv_Equiv (A:Type)(E_op : Mult_op A)(E_one : A)
      (E_eq: Equiv A)(M :EMonoid E_op E_one E_eq) :
   Equivalence E_eq.
Qed.

#[ global ] Instance Equiv_Refl (A:Type)(E_op : Mult_op A)(E_one : A)
      (E_eq: Equiv A)(M :EMonoid E_op E_one E_eq) :
   Reflexive E_eq.
Qed.

#[ global ] Instance Equiv_Sym (A:Type)(E_op : Mult_op A)(E_one : A)
      (E_eq: Equiv A)(M :EMonoid E_op E_one E_eq) :
   Symmetric E_eq.
Qed.

#[ global ] Instance Equiv_Trans (A:Type)(E_op : Mult_op A)(E_one : A)
      (E_eq: Equiv A)(M :EMonoid E_op E_one E_eq) :
   Transitive E_eq.
Qed.

Generalizable All Variables.

Coercion from Monoid to EMonoid

Every instance of class Monoid can be transformed into an instance of EMonoid, considering Leibniz' equality eq.

#[global] Instance eq_equiv {A} : Equiv A := eq.

#[global] Instance Monoid_EMonoid `(M:@Monoid A op one) :
EMonoid op one eq_equiv.

We can now register Monoid_EMonoid as a coercion:

Coercion Monoid_EMonoid : Monoid >-> EMonoid.

Commutative Monoids

The following type class definitions allow to take advantage of the possible commutativity of the operation

Class Abelian_EMonoid `(M:@EMonoid A op one Aeq ):= {
  Eop_comm : ∀ x y, op x y == op y x}.

Class Abelian_Monoid `(M:Monoid ):= {
  op_comm : ∀ x y, op x y = op y x}.

Ltac add_op_proper M H :=
let h := fresh H in
   generalize (@Eop_proper _ _ _ _ M); intro h.