(*
COSC 5V90 - Test 2.

Consider the following declarations of classes for monoids.
*)

Class MonoidSig (A : Type) := {
  op : A -> A -> A;
  e : A
}.

Infix "**" := op (at level 50).

Class Monoid (A : Type) := {
  mSig :> MonoidSig A;
  assoc : forall (x y z : A), x ** (y ** z) = (x ** y) ** z;
  id_r : forall (x : A), x ** e = x;
  id_l : forall (x : A), e ** x = x
}.

(*
Question 1:
a) (3 marks) Define a function nmult that takes a natural number n and a monoid element x and computes
x ** x ** x ** ... ** x
-----------|----------- 
           n-times
Hint (IMPORTANT): Use x ** (nmult n x) in the recursive case (NOT (nmult n x) ** x). 
*)

Fixpoint nmult `{M : Monoid} (n : nat) (x : A) : A :=
  match n with
    | 0 => e
    | S n => x ** nmult n x
  end.

(*
b) (6 marks) Prove the following lemma by induction on m.
*)

Lemma nmult_distr_l `{M : Monoid} : forall (m n: nat) (x : A), nmult m x ** nmult n x = nmult (m+n) x.
Proof.
induction m; intros; simpl.
apply id_l.
rewrite <- assoc.
rewrite IHm; trivial.
Qed.

(*
Question 2:
a) (4 marks) Define a class AbelianMonoid A for abelian monoids on type A. This class should have a monoid as substructure 
(i.e. M :> Monoid A) and should require the commutative law: x ** y = y ** x.
*)

Class AbelianMonoid (A : Type) := {
  M :> Monoid A;
  comm :  forall x y, x ** y = y ** x
}.

(*
b) (7 marks) Prove the following lemma by induction on n.
*)

Lemma nmult_distr_r `{M : AbelianMonoid} : forall (n: nat) (x y : A), nmult n x ** nmult n y = nmult n (x ** y).
Proof.
induction n; intros; simpl.
apply id_l.
rewrite <- assoc, (assoc _ y), (comm _ y), <- assoc, assoc.
rewrite IHn; trivial.
Qed.

(*
Consider the following classes for preordered types and the definition of a preorder (i.e. instance declaration)
for monoids. 
*)

Class PreOrderSig (A : Type) := {
  leqq : A -> A -> Prop
}.

Infix "<~" := (leqq) (at level 60).

Class PreOrder (A : Type) := {
  pSig :> PreOrderSig A;
  refl : forall (x : A), x <~ x;
  trans : forall (x y z : A), x <~ y -> y <~ z -> x <~ z
}.

Instance MonoidPreOrderSig `{M : Monoid} : PreOrderSig A := {|
  leqq := fun (x y : A) => exists (z : A), z ** x = y
|}.

(*
Question 3:
(10 marks) Make any instance of Monoid also an instance of PreOrder.
*)

Instance MonoidPreOrder `{M : Monoid} : PreOrder A := {|
  pSig := @MonoidPreOrderSig _ M;
|}.
Proof.
intros; simpl.
exists e.
apply id_l.
intros; simpl in *.
destruct H, H0.
exists (x1 ** x0).
rewrite <- assoc.
rewrite H; trivial.
Qed.

(*
The following two lemmas are for your interest only. They were not part of the actual test.
*)

Require Import PeanoNat.
Import Nat.

Lemma nmult_mono_l `{M : AbelianMonoid} : forall (m n : nat) (x : A), m <= n -> nmult m x <~ nmult n x.
Proof.
induction m; intros; simpl in *.
exists (nmult n x).
apply id_r.
destruct n.
apply nle_succ_0 in H; contradiction.
apply le_S_n in H.
apply (IHm _ x) in H.
destruct H.
exists x0.
rewrite assoc, (comm x0), <- assoc.
rewrite H; simpl; trivial.
Qed.

Lemma nmult_mono_r `{M : AbelianMonoid} : forall (n : nat) (x y : A), x <~ y -> nmult n x <~ nmult n y.
Proof.
induction n; intros; simpl in *.
exists e.
apply id_l.
assert (H0 := H); destruct H0.
apply IHn in H.
destruct H.
exists (x0 ** x1).
rewrite <- assoc, (assoc x1), (comm x1), <- assoc.
rewrite H, assoc.
rewrite H0; trivial.
Qed.