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.