(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)


(* Contribution to the Coq Library   V6.3 (July 1999)                    *)


(* ---                        monoid.v                                  --- *)
(*                                                                          *)
(* Author: Pierre Casteran.                                                 *)
(*    LABRI, URA CNRS 1304,                                                 *)
(*    Departement d'Informatique, Universite Bordeaux I,                    *)
(*    33405 Talence CEDEX,                                                  *)
(*    e-mail:  casteran@labri.u-bordeaux.fr                                 *)


(* 
 A monoid on some M:Set is a structure composed of a binary
 associative operation o:M->M->M, and a neutral element u:M
 for o.
*)


Require Import Arith.
Require Import Constants.


Section monoid_def.

Variable M : Set.

Record monoid : Set := mkmonoid
  {u : M;
   o : M -> M -> M;
   point_assoc : forall a b c : M, o a (o b c) = o (o a b) c;
   u_neutral_l : forall a : M, o u a = a;
   u_neutral_r : forall a : M, o a u = a}.

Hint Resolve point_assoc u_neutral_r u_neutral_l: arith.

Variable MO : monoid.
Let u' := u MO.
Let o' := o MO.
Remark o'_assoc : forall a b c : M, o' a (o' b c) = o' (o' a b) c.
(* Goal: forall a b c : M, @eq M (o' a (o' b c)) (o' (o' a b) c) *)
exact (point_assoc MO).
Qed.
Hint Resolve o'_assoc: arith.

Remark u'_neutral_l : forall a : M, o' u' a = a.
(* Goal: forall a : M, @eq M (o' u' a) a *)
exact (u_neutral_l MO).
Qed.
Hint Resolve u'_neutral_l: arith.

Remark u'_neutral_r : forall a : M, o' a u' = a.
(* Goal: forall a : M, @eq M (o' a u') a *)
exact (u_neutral_r MO).
Qed.
Hint Resolve u'_neutral_r: arith.


(* powering 
************)
Fixpoint power (x : M) (n : nat) {struct n} : M :=
  match n with
  | O => u'
  | S n => o' x (power x n)
  end.
                                     


(* some lemmas on powering *)
(***************************)

Lemma power_u : forall m : nat, power u' m = u'.
(******************************)
Proof.
(* Goal: forall m : nat, @eq M (power u' m) u' *)
 simple induction m; simpl in |- *.
(* Goal: @eq M (o' (power (power m b) q) (power m r)) (o' (power (power m b) q) (power m r)) *)
 auto with arith.
(* Goal: forall (a : M) (n p : nat), @eq M (o' (power a n) (power a p)) (o' (power a p) (power a n)) *)
 intros.
(* Goal: @eq M (o' (power (power m b) q) (power m r)) (o' (power (power m b) q) (power m r)) *)
 rewrite H; auto with arith.
Qed.
Hint Resolve power_u: arith.


Lemma power_plus :
 forall (a : M) (n p : nat), power a (n + p) = o' (power a n) (power a p).
(****************************************************)
Proof.
(* Goal: forall (a : M) (n p : nat), @eq M (power a (Init.Nat.add n p)) (o' (power a n) (power a p)) *)
 simple induction n; simpl in |- *; [ auto with arith | intros ].
(* Goal: @eq M (o' (power (power m b) q) (power m r)) (o' (power (power m b) q) (power m r)) *)
 rewrite (H p); auto with arith.
Qed.
Hint Resolve power_plus: arith.



Lemma power_1 : forall a : M, power a 1 = a.
(***********************************)
Proof.
(* Goal: @eq M (o' (power (power m b) q) (power m r)) (o' (power (power m b) q) (power m r)) *)
 intro; simpl in |- *; auto with arith.
Qed.

Lemma power_sym :
 forall (a : M) (n p : nat),
 o' (power a n) (power a p) = o' (power a p) (power a n).
(*************************************************************)
Proof.
(* Goal: forall (a : M) (n p : nat), @eq M (o' (power a n) (power a p)) (o' (power a p) (power a n)) *)
 intros.
(* Goal: @eq M (power a (Init.Nat.add n p)) (o' (power a p) (power a n)) *)
 rewrite <- power_plus.
(* Goal: @eq M (power a (Init.Nat.add n p)) (o' (power a p) (power a n)) *)
 rewrite <- power_plus.
(* Goal: @eq M (o' (power (power m b) q) (power m r)) (o' (power (power m b) q) (power m r)) *)
 rewrite plus_comm; auto with arith.
Qed.
Hint Resolve power_sym: arith.


Lemma power_mult :
 forall (a : M) (n p : nat), power a (p * n) = power (power a n) p.
(*****************************************************)
Proof.
(* Goal: forall (a : M) (n p : nat), @eq M (power a (Init.Nat.mul p n)) (power (power a n) p) *)
 simple induction p; simpl in |- *.
(* Goal: @eq M (o' (power (power m b) q) (power m r)) (o' (power (power m b) q) (power m r)) *)
 auto with arith.
(* Goal: forall (n0 : nat) (_ : @eq M (power a (Init.Nat.mul n0 n)) (power (power a n) n0)), @eq M (power a (Init.Nat.add n (Init.Nat.mul n0 n))) (o' (power a n) (power (power a n) n0)) *)
 intros n0 H.
(* Goal: @eq M (power a (Init.Nat.add n (Init.Nat.mul n0 n))) (o' (power a n) (power (power a n) n0)) *)
 rewrite power_plus.
(* Goal: @eq M (o' (power (power m b) q) (power m r)) (o' (power (power m b) q) (power m r)) *)
 elim H; auto with arith.
Qed.
Hint Resolve power_mult: arith.



Lemma a2x : forall (a : M) (x : nat), power (o' a a) x = power a (x + x).
(***************************************************************)
Proof.
(* Goal: forall (a : M) (x : nat), @eq M (power (o' a a) x) (power a (Init.Nat.add x x)) *)
 simple induction x; simpl in |- *.
(* Goal: @eq M (o' (power (power m b) q) (power m r)) (o' (power (power m b) q) (power m r)) *)
 auto with arith.
(* Goal: forall (n : nat) (_ : @eq M (power (o' a a) n) (power a (Init.Nat.add n n))), @eq M (o' (o' a a) (power (o' a a) n)) (o' a (power a (Init.Nat.add n (S n)))) *)
 intros; simpl in |- *.
(* Goal: @eq M (o' (o' a a) (power (o' a a) n)) (o' a (power a (Init.Nat.add n (S n)))) *)
 rewrite <- plus_n_Sm.
(* Goal: @eq M (o' (o' a a) (power (o' a a) n)) (o' a (power a (S (Init.Nat.add n n)))) *)
 simpl in |- *.
(* Goal: @eq M (o' (power (power m b) q) (power m r)) (o' (power (power m b) q) (power m r)) *)
 rewrite o'_assoc; elim H; auto with arith.
Qed.

Lemma power_eucl :
 forall (m : M) (b q r : nat),
 power m (q * b + r) = o' (power (power m b) q) (power m r).
(*************************************************************)
Proof.
(* Goal: @eq M (power a (Init.Nat.add n (Init.Nat.mul n0 n))) (o' (power a n) (power (power a n) n0)) *)
 intros; rewrite power_plus.
(* Goal: @eq M (o' (power m (Init.Nat.mul q b)) (power m r)) (o' (power (power m b) q) (power m r)) *)
 rewrite power_mult.
(* Goal: @eq M (o' (power (power m b) q) (power m r)) (o' (power (power m b) q) (power m r)) *)
 auto with arith.
Qed.
Hint Resolve power_eucl: arith.


End monoid_def.











