task36.v

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.
    apply (Z.divide_add_r a (proj1_sig a0) (proj1_sig b)).
    apply (proj2_sig a0).
    apply (proj2_sig b).
  Qed.

  Program Definition mult(a : Z) (b : pi) : pi := (a * b)%Z.
  Next Obligation.
    apply (Z.divide_mul_r a a0 (proj1_sig b)).
    apply (proj2_sig b).
  Qed.
End Principal_Ideal.

task37.v

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.
  apply Build_Equivalence.
  auto.
  auto.
  unfold Transitive.
  intros.
  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.
  intros.
  simpl.
  omega.
Qed.

Instance int_minus_compat : Proper (equiv ==> equiv ==> equiv) int_minus.
Proof.
  unfold Proper.
  unfold respectful.
  intros.
  simpl.
  simpl in H0.
  simpl in H.
  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.

task38.v

(* モノイド *)
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 :=
  fix fp (lt:list T) : T :=
    match lt with
    | nil => one
    | cons x xs => mult x (fp xs)
    end.

Require Import Arith.

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

Require Import List.

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