適当に同値関係定めればいけそうだけど面倒になりそう… うまくやる方法があるのかな

8.v

Module Q36.
Require Import ZArith.

Section Principal_Ideal.
  Variable a : Z.

  Definition pi : Set := { x : Z | ( a | x )%Z }.

  Program Definition plus(a b : pi) : pi := (a + b)%Z.
  Next Obligation.
    destruct a0,b; simpl. apply Z.divide_add_r; assumption.
  Qed.

  Program Definition mult(a : Z) (b : pi) : pi := (a * b)%Z.
  Next Obligation.
    destruct b; simpl. apply Z.divide_mul_r; assumption.
  Qed.
End Principal_Ideal.
End Q36.

Module Q37.
Require Import SetoidClass.
Require Import Omega.

Record int := {
  Ifst : nat;
  Isnd : nat
}.

Program Instance ISetoid : Setoid int := {|
  equiv x y := Ifst x + Isnd y = Ifst y + Isnd x
|}.
Next Obligation.
Proof.
  constructor; intro; intros;
  destruct x; try (destruct y; try (destruct z)); simpl in *.
  reflexivity. rewrite H. reflexivity. omega.
Qed.

Definition zero : int := {|
  Ifst := 0;
  Isnd := 0
|}.

Definition int_minus(x y : int) : int := {|
  Ifst := Ifst x + Isnd y;
  Isnd := Isnd x + Ifst y
|}.

Lemma int_sub_diag : forall x, int_minus x x == zero.
Proof.
  destruct x. simpl. omega.
Qed.

(* まず、int_minus_compatを証明せずに、下の2つの証明を実行して、どちらも失敗することを確認せよ。*)
(* 次に、int_minus_compatを証明し、下の2つの証明を実行せよ。 *)

Instance int_minus_compat : Proper (equiv ==> equiv ==> equiv) int_minus.
Proof.
  unfold Proper, respectful. intros. destruct x,y,x0,y0. simpl in *. omega.
Qed.

Goal forall x y, int_minus x (int_minus y y) == int_minus x zero.
Proof.
  intros x y.
  rewrite int_sub_diag.
  reflexivity.
Qed.

Goal forall x y, int_minus x (int_minus y y) == int_minus x zero.
Proof.
  intros x y.
  setoid_rewrite int_sub_diag.
  reflexivity.
Qed.

End Q37.

Module Q38.
(* モノイド *)
Class Monoid(T:Type) := {
  mult : T -> T -> T
    where "x * y" := (mult x y);
  one : T
    where "1" := one;
  mult_assoc x y z : x * (y * z) = (x * y) * z;
  mult_1_l x : 1 * x = x;
  mult_1_r x : x * 1 = x
}.

Delimit Scope monoid_scope with monoid.
Local Open Scope monoid_scope.

Notation "x * y" := (mult x y) : monoid_scope.
Notation "1" := one : monoid_scope.

(* モノイドのリストの積。DefinitionをFixpointに変更するなどはOK *)
Definition product_of{T:Type} {M:Monoid T} : list T -> T :=
  list_rect (fun _ => T) 1 (fun m _ acc => m * acc).

Require Import Arith.

(* 自然数の最大値関数に関するモノイド。
 * InstanceをProgram Instanceにしてもよい *)
Instance MaxMonoid : Monoid nat := {
  mult := max;
  one := 0
}.
Proof.
  apply Max.max_assoc. apply Max.max_0_l. apply Max.max_0_r.
Defined.

Require Import List.

Eval compute in product_of (3 :: 2 :: 6 :: 4 :: nil). (* => 6 *)
Eval compute in product_of (@nil nat). (* => 0 *)
End Q38.

Module Q39.
(* bindの記法を予約 *)
Reserved Notation "x >>= y" (at level 110, left associativity).

(* モナド *)
Class Monad(M:Type -> Type) := {
  bind {A B} : M A -> (A -> M B) -> M B
    where "x >>= f" := (bind x f);
  ret {A} : A -> M A;
  bind_ret_l : forall A B (a:A) (f : A -> M B), (ret a >>= f) = f a;
  bind_ret_r : forall A (m : M A), (m >>= ret) = m;
  bind_assoc : forall A B C (m : M A) (f : A -> M B) (g : B -> M C),
    (m >>= (fun a => f a >>= g)) = ((m >>= f) >>= g)
}.

Notation "x >>= f" := (@bind _ _ _ _ x f).

Require Import List.

Program Instance ListMonad : Monad list := {|
  bind A B m f := flat_map f m;
  ret A x := x :: nil
|}.
Next Obligation.
  apply app_nil_r.
Qed.
(* 以下、ListMonadが定義できるまでNext Obligation -> Qed を繰り返す *)
Next Obligation.
  induction m; simpl. reflexivity. rewrite IHm. reflexivity.
Qed.
Next Obligation.
  induction m; simpl. reflexivity. rewrite IHm.
  assert (H : forall xs ys,
    flat_map g xs ++ flat_map g ys = flat_map g (xs ++ ys)).
    intros. induction xs; simpl. reflexivity.
    rewrite <- app_assoc. rewrite IHxs. reflexivity.
  rewrite H. reflexivity.
Qed.
(* モナドの使用例 *)

Definition foo : list nat := 1 :: 2 :: 3 :: nil.

(* 内包記法もどき *)
(*
  do x <- foo
     y <- foo
     (x, y)
*)
Definition bar := Eval lazy in
  foo >>= (fun x =>
  foo >>= (fun y =>
  ret (x, y))).

Print bar.
End Q39.

Module Q40.
Require Import SetoidClass.

(* モノイド *)
Class Monoid(T:Type) := {
  monoid_setoid : Setoid T;
  mult : T -> T -> T
    where "x * y" := (mult x y);
  mult_proper : Proper (equiv ==> equiv ==> equiv) mult;
  one : T
    where "1" := one;
  mult_assoc x y z : x * (y * z) == (x * y) * z;
  mult_1_l x : 1 * x == x;
  mult_1_r x : x * 1 == x
}.

Existing Instance monoid_setoid.
Existing Instance mult_proper.

Delimit Scope monoid_scope with monoid.
Local Open Scope monoid_scope.

Notation "x * y" := (mult x y) : monoid_scope.
Notation "1" := one : monoid_scope.

(* モノイド準同型 *)
Class MonoidHomomorphism{A B:Type}
  {monoid_A : Monoid A} {monoid_B : Monoid B}
  (f : A -> B) : Prop := {
  monoid_homomorphism_proper : Proper (equiv ==> equiv) f;
  monoid_homomorphism_preserves_mult x y:
    f (x * y) == f x * f y;
  monoid_homomorphism_preserves_one:
    f 1 == 1
}.

Existing Instance monoid_homomorphism_proper.

(* モノイドの直和 *)
Section MonoidCoproduct.
  (* A, B : モノイド *)
  Variable A B : Type.
  Context {monoid_A : Monoid A} {monoid_B : Monoid B}.

  (* AとBのモノイド直和の台集合 *)
  Definition MonoidCoproduct : Type := list (A+B)%type.

  (* モノイド直和の二項演算 *)
  Definition MCmult : MonoidCoproduct -> MonoidCoproduct -> MonoidCoproduct
    := @app _.

  Definition MC1 : MonoidCoproduct := nil.

  Require Import List.

  (* MonoidCoproductの同値関係 *)
  Definition MonoidEqual : MonoidCoproduct -> MonoidCoproduct -> Prop
    := .

  (* 以上がモノイドになっていること *)
  Program Instance MonoidCoproductMonoid : Monoid MonoidCoproduct := {|
    monoid_setoid := {|
      equiv := MonoidEqual
    |};
    mult := MCmult;
    one := MC1
  |}.
  Next Obligation.
  Qed.

  (* A, Bから直和への標準的な埋め込み射 *)
  Definition emb_l : A -> MonoidCoproduct
    := fun a => inl a :: nil.
  Definition emb_r : B -> MonoidCoproduct
    := fun b => inr b :: nil.

  (* emb_lがモノイド準同型であること *)
  Instance emb_l_homomorphism : MonoidHomomorphism emb_l.
  Proof.
  Qed.

  (* emb_rがモノイド準同型であること *)
  Instance emb_r_homomorphism : MonoidHomomorphism emb_r.
  Proof.
    (* ここを埋める *)
  Qed.

  (* 普遍性 *)
  (* Universal Mapping Property *)
  Section UMP.
    (* X : モノイド *)
    Variable X : Type.
    Context {monoid_X : Monoid X}.
    (* f, g : モノイド準同型 *)
    Variable f : A -> X.
    Variable g : B -> X.
    Context {homomorphism_f : MonoidHomomorphism f}.
    Context {homomorphism_g : MonoidHomomorphism g}.

    (* 図式を可換にする射の存在 *)
    Section Existence.
      (* 図式を可換にする射 *)
      Definition h : MonoidCoproduct -> X := (* ここを埋める *) .

      (* hがモノイド準同型であること *)
      Instance homomorphism_h : MonoidHomomorphism h.
      Proof.
        (* ここを埋める *)
      Qed.

      (* hの可換性1 *)
      Lemma h_commute_l : forall a, h (emb_l a) == f a.
      Proof.
        (* ここを埋める *)
      Qed.

      (* hの可換性2 *)
      Lemma h_commute_r : forall a, h (emb_r a) == g a.
      Proof.
        (* ここを埋める *)
      Qed.
    End Existence.

    (* 図式を可換にする射の一意性 *)
    Section Uniqueness.
      (* h' : モノイド準同型 *)
      Variable h' : MonoidCoproduct -> X.
      Context {homomorphism_h' : MonoidHomomorphism h'}.

      (* h' は上のhと同じ可換性をもつ *)
      Hypothesis h'_commute_l : forall a, h' (emb_l a) == f a.
      Hypothesis h'_commute_r : forall b, h' (emb_r b) == g b.

      (* このようなh'は結局hと同一である *)
      Lemma uniqueness : forall c, h' c == h c.
      Proof.
        (* ここを埋める *)
      Qed.
    End Uniqueness.
  End UMP.
End MonoidCoproduct.
End Q40.