35がわからない

7.v

Module Q31.

(* Section     *)

Section Poslist.
  (*             A              *)
  Variable A : Type.
  (*        *)
  Inductive poslist : Type :=
      pnil  : A -> poslist
    | pcons : A -> poslist -> poslist.

  Section Fold.
    (*      *)
    Variable g : A -> A -> A.

   (* g         
    *                       
    *       :     [a; b; c]      (a * b) * c       
    *       :     [a; b; c]      a * (b * c)       
    *)
    (*   *)
    Definition fold : poslist -> A :=
      poslist_rect (fun _ => A) (fun a => a) (fun a _ b => g a b).
    (* Definition Fixpoint             *)
  End Fold.
End Poslist.
(* Poslist           poslist   A               *)

(*          map   *)
Section PoslistMap.
  Variable A B : Type.
  Variable f : A -> B.

  Definition map : poslist A -> poslist B := poslist_rect _ (fun _ => poslist B)
    (fun a => pnil _ (f a)) (fun a _ l => pcons _ (f a) l).
End PoslistMap.

(*                        *)

End Q31.

Module Q32.
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.

Module NatMult_SemiGroup <: SemiGroup.
  Definition G := nat.
  Definition mult := mult.
  Definition mult_assoc := mult_assoc.
End NatMult_SemiGroup.

Module NatMax_SemiGroup <: SemiGroup.
  Definition G := nat.
  Definition mult := max.
  Definition mult_assoc := Max.max_assoc.
End NatMax_SemiGroup.

Module SemiGroup_Product (G0 G1:SemiGroup) <: SemiGroup.
  Definition G := (G0.G * G1.G)%type.
  Definition mult (x y : G) :=
    let (x0,x1) := x in
    let (y0,y1) := y in
    (G0.mult x0 y0, G1.mult x1 y1).
  Lemma mult_assoc : forall x y z, mult x (mult y z) = mult (mult x y) z.
  Proof.
    destruct x,y,z. simpl. rewrite G0.mult_assoc. rewrite G1.mult_assoc.
    reflexivity.
  Qed.
End SemiGroup_Product.

End Q32.

Module Q33.

Module Type Monoid.
  Parameter M : Type.
  Parameter e : M.
  Parameter mult : M -> M -> M.
  Axiom mult_unit_l : forall x : M, mult e x = x.
  Axiom mult_unit_r : forall x : M, mult x e = x.
  Axiom mult_assoc :
    forall x y z : M, mult x (mult y z) = mult (mult x y) z.
End Monoid.

Require Import List.

Module list_bool_Monoid <: Monoid.
  Definition M := list bool.
  Definition e := @nil bool.
  Definition mult := @app bool.
  Definition mult_unit_l := @app_nil_l bool.
  Definition mult_unit_r := @app_nil_r bool.
  Definition mult_assoc := @app_assoc bool.
End list_bool_Monoid.

Module Monoid_pow (M : Monoid).
  Fixpoint mpow (m : M.M) (n : nat) :=
    match n with
    | O => M.e
    | S n' => M.mult m (mpow m n')
    end.
  Lemma exponential_law :
    forall (x:M.M) (m n:nat), mpow x (m+n) = M.mult (mpow x m) (mpow x n).
  Proof.
    induction m; intros; simpl.
    - rewrite M.mult_unit_l. reflexivity.
    - rewrite <- M.mult_assoc. rewrite IHm. reflexivity.
  Qed.
End Monoid_pow.

Module list_bool_pow := list_bool_Monoid <+ Monoid_pow.

End Q33.

Module Q34_35.
Require Import Structures.Equalities.

Module Type SemiGroup (Import E:EqualityType').
  Parameter mult : t -> t -> t.
  Infix "*" := mult.
  Axiom mult_assoc :
    forall x y z : t, x * (y * z) == (x * y) * z.
  Axiom mult_well_defined :
    forall x y z w : t, x == y -> z == w -> x * z == y * w.
End SemiGroup.
End Q34_35.