coq_practice_32.v

Require Import Arith.

Module Type SemiGroup.
  Parameter G : Type.
  Parameter mult : G -> G -> G.
  Axiom mult_assoc :
    forall x y z : G, mult x (mult y z) = mult (mult x y) z.
End SemiGroup.
Print SemiGroup.
Module NatMult_SemiGroup <: SemiGroup.
  (* ここを埋める *)
  Definition G := nat.
  Definition mult := mult.
  Lemma mult_assoc : forall x y z : G, mult x (mult y z) = mult (mult x y) z.
  Proof.
    unfold G.
    unfold mult.
    intros.
    ring.
  Qed.
End NatMult_SemiGroup.


Module NatMax_SemiGroup <: SemiGroup.
  (* ここを埋める *)
  Definition G := nat.
  Definition mult := min.
  Lemma mult_assoc : forall x y z : G, mult x (mult y z) = mult (mult x y) z.
  Proof.
    unfold G.
    unfold mult.
    intro.
    induction x.
    simpl.
    reflexivity.
    induction y.
    simpl.
    reflexivity.
    induction z.
    simpl.
    reflexivity.
    simpl.
    apply eq_S.
    apply IHx.
  Qed.
End NatMax_SemiGroup.


Module SemiGroup_Product (G0 G1:SemiGroup) <: SemiGroup.
  Definition G := (prod G0.G G1.G).
  Definition mult := 
    fun p q => (G0.mult (fst p) (fst q), G1.mult (snd p) (snd q)).
  Lemma mult_assoc : forall x y z: G, mult x (mult y z) = mult (mult x y) z.
    unfold mult.
    intros.
    simpl.
    assert ((G0.mult (fst x) (G0.mult (fst y) (fst z))) = (G0.mult (G0.mult (fst x) (fst y)) (fst z))).
    apply G0.mult_assoc.
    assert ((G1.mult (snd x) (G1.mult (snd y) (snd z))) = (G1.mult (G1.mult (snd x) (snd y)) (snd z))).
    apply G1.mult_assoc.
    rewrite H.
    rewrite H0.
    reflexivity.
  Qed.
End SemiGroup_Product.