Monoid type class and its instances.

reduce.v

Require Import List Arith ZArith Program.

Class Monoid {A} (dot : A -> A -> A) (zero : A) := {
  monoid_1st_law : forall a, dot a zero = a;
  monoid_2nd_law : forall a, dot zero a = a;
  monoid_3rd_law : forall a b c, dot (dot a b) c = dot a (dot b c)
}.

Instance nat_plus_Monoid : Monoid plus 0.
  split; auto with arith.
Qed.

Instance Z_mult_Monoid : Monoid Zmult 1%Z.
  split; auto with zarith.
Qed.

Instance bool_all_Monoid : Monoid andb true.
  split.
    intro a. case a; auto.
    intro a. case a; auto.
    intros a b c. case a, b, c; auto.
Qed.

Instance list_app_Monoid {A} : Monoid (fun (xs ys : list A) => app xs ys) [].
  split; auto with datatypes.
Qed.

Definition reduce {A} `{Monoid A} (xs : list A) := fold_left dot xs zero.

Eval compute in reduce [1; 2; 3; 4].
Eval compute in reduce [1; 2; 3; 4]%Z.
Eval compute in reduce [true; true].
Eval compute in reduce [true; false].
Eval compute in reduce [[1]; [2; 3]; [4; 5; 6]].

z

$ coqtop -l reduce.v                
Welcome to Coq 8.4 (September 2012)
     = 10
     : nat
     = 24%Z
     : Z
     = true
     : bool
     = false
     : bool
     = [1; 2; 3; 4; 5; 6]
     : list nat

Coq <