# Library Exercise_3_1_1_7

Require Import Utf8 Setoid.
Require Import Monoid Notations.

Set Implicit Arguments.

Generalizable All Variables.

Definition smallest_monoid : Monoid unit.
eexists (@Build_ComputationalMonoid _ tt (fun _ _tt)).
split;
repeat intros [];
reflexivity.
Defined.

Lemma no_smaller_monoid : Monoid False.
intro M.
destruct (@id _ M).
Qed.

Inductive two := twoa | twob.

Inductive three := one | zeroa | zerob.

Definition f : threethreethree :=
fun x ymatch (x, y) with
| (one, z)z
| (z, one)z
| (zeroa, _)zeroa
| (zerob, _)zerob
end.

Definition three_monoid : Monoid three.
eexists (@Build_ComputationalMonoid _ one f).
split; repeat intros []; reflexivity.
Defined.

Lemma two_monoid_is_commutative (M : Monoid two) : is_commutative M.
repeat intro;
pose proof (@left_id _ _ M);
pose proof (@right_id _ _ M);
set (i := @id _ M) in *; clearbody i;
hnf in *;
repeat match goal with
| [ H := _ |- _ ] ⇒ subst H
| [ H : two |- _ ] ⇒ destruct H
| [ H : _ |- _ ] ⇒ rewrite H
end;
try reflexivity.
Qed.