「代数的構造と Coq：破」のためのスクリプト(at Coq8.4pl6)

algebraic_structure_middle.v

Set Implicit Arguments.
Unset Strict Implicit.

Generalizable All Variables.

Require Export Basics Tactics Coq.Setoids.Setoid Morphisms.

Structure Setoid :=
  {
    carrier:> Type;
    equal: relation carrier;

    prf_Setoid:> Equivalence equal
  }.
Existing Instance prf_Setoid.
Notation Setoid_of eq := (@Build_Setoid _ eq _).

Notation "(== :> S )" := (equal (s:=S)).
Notation "(==)" := (== :> _).
Notation "x == y" := (equal x y) (at level 70, no associativity).
Notation "x == y :> S" := (equal (s:=S) x y)
  (at level 70, y at next level, no associativity).

Class isMap (X Y: Setoid)(f: X -> Y) :=
  map_subst:> Proper ((==) ==> (==)) f.

Structure Map (X Y: Setoid) :=
  {
    map_body:> X -> Y;

    prf_map:> isMap map_body
  }.
Existing Instance prf_map.
Notation makeMap f := (@Build_Map _ _ f _).
Notation "[ x .. y :-> p ]" := 
  (makeMap (fun x => .. (makeMap (fun y => p)) ..))
    (at level 200, x binder, y binder, right associativity,
     format "'[' [ x .. y :-> '/ ' p ] ']'").

Class isBinop (X: Setoid)(op: X -> X -> X) :=
  binop_subst:> Proper ((==) ==> (==) ==> (==)) op.

Structure Binop (X: Setoid) :=
  {
    binop:> X -> X -> X;
    prf_Binop:> isBinop binop
  }.
Existing Instance prf_Binop.


Class Associative `(op: Binop X): Prop :=
  associative:>
    forall (x y z: X), op x (op y z) == op (op x y) z.

Class LIdentical `(op: Binop X)(e: X): Prop :=
  left_identical:> forall x: X, op e x == x.

Class RIdentical `(op: Binop X)(e: X): Prop :=
  right_identical:> forall x: X, op x e == x.

Class Identical `(op: Binop X)(e: X): Prop :=
  {
    identical_l:> LIdentical op e;
    identical_r:> RIdentical op e
  }.
Existing Instance identical_l.
Existing Instance identical_r.
Coercion identical_l: Identical >-> LIdentical.
Coercion identical_r: Identical >-> RIdentical.

Class LInvertible `{Identical X op e}(inv: Map X X): Prop :=
  left_invertible:>
    forall (x: X), op (inv x) x == e.

Class RInvertible `{Identical X op e}(inv: Map X X): Prop :=
  right_invertible:>
    forall (x: X), op x (inv x) == e.

Class Invertible `{Identical X op e}(inv: Map X X): Prop :=
  {
    invertible_l:> LInvertible inv;
    invertible_r:> RInvertible inv
  }.
Coercion invertible_l: Invertible >-> LInvertible.
Coercion invertible_r: Invertible >-> RInvertible.

Class Divisible `(op: Binop X)(divL divR: Binop X): Prop :=
  {
    divisible_l:>
      forall (a b: X), op (divL a b) a == b;
    divisible_r:>
      forall (a b: X), op a (divR a b) == b
  }.

Class Commute `(op: Binop X): Prop :=
  commute:>
    forall a b, op a b == op b a.

Class Distributive (X: Setoid)(add mul: Binop X) :=
  {
    distributive_l:>
      forall a b c, mul a (add b c) = add (mul a b) (mul a c);

    distributive_r:>
      forall a b c, mul (add a b) c = add (mul a c) (mul b c)
  }.

Module Monoid.
  Class spec (M: Setoid)(op: Binop M)(e: M) :=
    proof {
        associative:> Associative op;
        identical:> Identical op e
      }.

  Structure type :=
    make {
        carrier: Setoid;
        op: Binop carrier;
        e: carrier;

        prf: spec op e
      }.

  Module Ex.
    Existing Instance associative.
    Existing Instance identical.
    Existing Instance prf.

    Notation isMonoid := spec.
    Notation Monoid := type.

    Coercion associative: isMonoid >-> Associative.
    Coercion identical: isMonoid >-> Identical.
    Coercion carrier: Monoid >-> Setoid.
    Coercion prf: Monoid >-> isMonoid.

    Delimit Scope monoid_scope with monoid.
    Notation "x * y" := (op _ x y) (at level 40, left associativity): monoid_scope.
    Notation "'1'" := (e _): monoid_scope.
  End Ex.

End Monoid.
Export Monoid.Ex.

Section MonoidProps.
  Variable (M: Monoid).
  Open Scope monoid_scope.

  Lemma left_op:
    forall x y z: M,
      y == z -> x * y == x * z.
  Proof.
    intros.
    now rewrite H.
  Qed.

  Lemma right_op:
    forall x y z: M,
      x == y -> x * z == y * z.
  Proof.
    intros.
    now rewrite H.
  Qed.


  Lemma commute_l:
    forall `{Commute M (Monoid.op M)}(x y z: M), x * (y * z) == y * (x * z).
  Proof.
    intros; repeat rewrite associative.
    now rewrite (commute x y).
  Qed.
End MonoidProps.


Module Group.
  Class spec (G: Setoid)(op: Binop G)(e: G)(inv: Map G G) :=
    proof {
        identical: Identical op e;
        invertible: Invertible inv;
        associative: Associative op
      }.

  Structure type :=
    make {
        carrier: Setoid;
        op: Binop carrier;
        e: carrier;
        inv: Map carrier carrier;
        
        prf: spec op e inv
      }.

  Module Ex.
    Existing Instance associative.
    Existing Instance identical.
    Existing Instance invertible.
    Existing Instance prf.

    Notation isGroup := spec.
    Notation Group := type.

    Coercion associative: isGroup >-> Associative.
    Coercion identical: isGroup >-> Identical.
    Coercion invertible: isGroup >-> Invertible.
    Coercion carrier: Group >-> Setoid.
    Coercion prf: Group >-> isGroup.

    Delimit Scope group_scope with group.

    Notation "x * y" := (op _ x y) (at level 40, left associativity): group_scope.
    Notation "'1'" := (e _): group_scope.
    Notation "x ^-1" := (inv _ x) (at level 20, left associativity): group_scope.
  End Ex.

  Import Ex.
  
  Instance is_monoid (G: Group): isMonoid (op G) (e G).
  Proof.
    split; auto; apply G.
  Qed.

  Canonical Structure monoid (G: Group): Monoid := Monoid.make (is_monoid G).

End Group.
Export Group.Ex.
Coercion Group.monoid: Group >-> Monoid.

Section GroupProps.

  Variable (G: Group).
  Open Scope group_scope.
  
  Lemma inv_op:
    forall (x y: G),
      (x * y)^-1 == y^-1 * x^-1.
  Proof.
    intros.
    rewrite <- (left_identical ((y^-1 * x^-1))).
    rewrite <- (left_invertible (x * y)).
    repeat rewrite <- associative.
    rewrite (associative y).
    now rewrite right_invertible, left_identical, right_invertible, right_identical.
  Qed.

  Lemma inv_id:
    (1^-1 == 1 :> G)%group.
  Proof.
    intros.
    now rewrite <- (left_identical (1^-1)), right_invertible.
  Qed.  

  Lemma inv_inv:
    forall (x: G), x ^-1 ^-1 == x.
  Proof.
    intros.
    now rewrite <- (left_identical (x^-1^-1)), <- (right_invertible x), <- associative, right_invertible, right_identical.
  Qed.

End GroupProps.


Module Ring.
  Class spec (R: Setoid)(add: Binop R)(z: R)(inv: Map R R)(mul: Binop R)(e: R) :=
    proof {
        add_group: isGroup add z inv;
        add_commute: Commute add;
        mul_monoid: isMonoid mul e;

        distributive: Distributive add mul
      }.

  Structure type :=
    make {
        carrier: Setoid;

        add: Binop carrier;
        z: carrier;
        inv: Map carrier carrier;

        mul: Binop carrier;
        e: carrier;

        prf: spec add z inv mul e
      }.

  Module Ex.
    Existing Instance add_group.
    Existing Instance add_commute.
    Existing Instance mul_monoid.
    Existing Instance distributive.
    Existing Instance prf.

    Notation isRing := spec.
    Notation Ring := type.

    Coercion add_group: isRing >-> isGroup.
    Coercion add_commute: isRing >-> Commute.
    Coercion mul_monoid: isRing >-> isMonoid.
    Coercion distributive: isRing >-> Distributive.
    Coercion carrier: Ring >-> Setoid.
    Coercion prf: Ring >-> isRing.

    Delimit Scope ring_scope with rng.

    Notation "x + y" := (add _ x y): ring_scope.
    Notation "x * y" := (mul _ x y): ring_scope.
    Notation "'0'" := (z _): ring_scope.
    Notation "x ^-1" := (inv _ x) (at level 20, left associativity): ring_scope.
    Notation "x - y" := (add _ x (y^-1)%rng): ring_scope.
    Notation "'1'" := (e _): ring_scope.
  End Ex.
  Import Ex.

  Canonical Structure group (R: Ring) := Group.make (prf R).
  Canonical Structure monoid (R: Ring) := Monoid.make (prf R).

  Coercion group: Ring >-> Group.
  Coercion monoid: Ring >-> Monoid.

  Open Scope ring_scope.
  Definition add_id_l {R: Ring}(x: R) := (@left_identical R (add R) (z R) (add_group (spec:=R)) x).
  Definition add_id_r {R: Ring}(x: R) := (@right_identical R (add R) (z R) (add_group (spec:=R)) x).
  Definition add_inv_l {R: Ring}(x: R) := (@left_invertible R (add R) (z R) (add_group (spec:=R))
                                                            (inv R) (add_group (spec:=R)) x).
  Definition add_inv_r {R: Ring}(x: R) := (@right_invertible R (add R) (z R) (add_group (spec:=R))
                                                             (inv R) (add_group (spec:=R)) x).
  Definition add_inv_op {R: Ring}(x y: R) :=
    (inv_op (G:=Group.make (Ring.add_group (R:=R))) x y).
  Definition add_inv_id (R: Ring): 0^-1 == 0 := (inv_id R).
  Definition add_inv_inv {R: Ring}(x: R) := (inv_inv (G:=R) x).
  Definition add_commute_l {R: Ring}(x y z: R) := (commute_l (M:=Ring.group R) x y z).

  Definition mul_id_l {R: Ring}(x: R) := (@left_identical R (mul R) (e R) (mul_monoid (spec:=R)) x).
  Definition mul_id_r {R: Ring}(x: R) := (@right_identical R (mul R) (e R) (mul_monoid (spec:=R)) x).
  
End Ring.
Export Ring.Ex.
Coercion Ring.group: Ring >-> Group.
Coercion Ring.monoid: Ring >-> Monoid.


Section RingProps.
  Variable (R: Ring).
  Open Scope ring_scope.

  Lemma ring_mul_0_l:
    forall (x: R),
      (0 * x == 0)%rng.
  Proof.
    intros.
    assert (H: 0 * x == 0 * x + 0 * x :> R).
    {
      rewrite <- (Ring.add_inv_l 0) at 1.
      rewrite (Ring.add_inv_id R); simpl.
      now rewrite (distributive_r).
    }
    apply symmetry.
    generalize (left_op (M:=Ring.group R) ((0*x)^-1) H); simpl.
    now rewrite Ring.add_inv_l, associative, Ring.add_inv_l, Ring.add_id_l.
  Qed.
  
  Lemma ring_mul_0_r:
    forall (x: R),
      (x * 0 == 0)%rng.
  Proof.
    intros.
    assert (H: x * 0 == x * 0 + x * 0 :> R).
    {
      rewrite <- (Ring.add_inv_l 0) at 1.
      rewrite (Ring.add_inv_id R); simpl.
      now rewrite (distributive_l).
    }
    apply symmetry.
    generalize (left_op (M:=Ring.group R) ((x*0)^-1) H); simpl.
    now rewrite Ring.add_inv_l, associative, Ring.add_inv_l, Ring.add_id_l.
  Qed.

  Lemma ring_minus_mul_l:
    forall x: R, 1^-1 * x == x^-1.
  Proof.
    intros x.
    rewrite <- (Ring.add_id_l).
    rewrite <- (Ring.add_inv_l x), <- associative.
    rewrite <- (Ring.mul_id_l x) at 2.
    now rewrite <- distributive_r, Ring.add_inv_r, ring_mul_0_l, Ring.add_id_r.
  Qed.

  Lemma ring_minus_mul_r:
    forall x: R, x * 1^-1 == x^-1.
  Proof.
    intros x.
    rewrite <- (Ring.add_id_r).
    rewrite <- (Ring.add_inv_r x), associative.
    rewrite <- (Ring.mul_id_r x) at 2.
    now rewrite <- distributive_l, Ring.add_inv_l, ring_mul_0_r, Ring.add_id_l.
  Qed.

  Lemma ring_mul_inv_l:
    forall x y: R,
      (x^-1) * y == (x * y)^-1.
  Proof.
    intros.
    rewrite <- (Ring.add_id_l).
    rewrite <- (Ring.add_inv_l (x*y)), <- associative.
    now rewrite <- distributive_r, Ring.add_inv_r, ring_mul_0_l, Ring.add_id_r.
  Qed.

  Lemma ring_mul_inv_r:
    forall x y: R,
      x * (y^-1) == (x * y)^-1.
  Proof.
    intros.
    rewrite <- (Ring.add_id_l).
    rewrite <- (Ring.add_inv_l (x*y)), <- associative.
    now rewrite <- distributive_l, Ring.add_inv_r, ring_mul_0_r, Ring.add_id_r.
  Qed.

  Lemma ring_mul_inv_inv:
    forall x y: R,
      (x^-1) * (y^-1) == x * y.
  Proof.
    intros.
    now rewrite ring_mul_inv_l, ring_mul_inv_r, (Ring.add_inv_inv (x*y)).
  Qed.
End RingProps.


(* Example *)
Require Import ZArith.
Open Scope Z_scope.

Canonical Structure positive_setoid := Setoid_of (@eq positive).
Canonical Structure Z_setoid := Setoid_of (@eq Z).
Instance Zneg_Proper : Proper ((==:>positive_setoid) ==> ((==:>Z_setoid))) Zneg.
Proof.
  now intros p q Heq; simpl in *; subst.
Qed.

Instance Zpos_Proper : Proper ((==:>positive_setoid) ==> ((==:>Z_setoid))) Zpos.
Proof.
  now intros p q Heq; simpl in *; subst.
Qed.

(* Group of '+' *)
Program Instance Zplus_is_binop: isBinop (X:=Z_setoid) Zplus.
Canonical Structure Zplus_binop := Build_Binop Zplus_is_binop.

Program Instance Zinv_is_map: isMap (X:=Z_setoid) Zopp.

Canonical Structure Zinv_map: Map Z_setoid Z_setoid := Build_Map Zinv_is_map.

Program Instance Zplus_is_group: isGroup Zplus_binop 0 Zinv_map.
Next Obligation.
  repeat split.
  - intros x; simpl.
    apply Zplus_0_r.
Qed.
Next Obligation.
  repeat split.
  - intros x; simpl.
    apply Z.add_opp_diag_l.
  - intros x; simpl.
    apply Z.add_opp_diag_r.
Qed.
Next Obligation.
  intros x y z; simpl.
  apply Zplus_assoc.
Qed.
Canonical Structure Zgroup_monoid := Group.make Zplus_is_group.

(* Monoid of '*' *)
Instance Zmult_is_binop: isBinop (X:=Z_setoid) Zmult.
Proof.
  intros x y Heq z w Heq'; simpl in *; subst; auto.
Qed.
Canonical Structure Zmult_binop := Build_Binop Zmult_is_binop.

Program Instance Zmult_is_monoid: isMonoid Zmult_binop 1.
Next Obligation.
  intros x y z; simpl.
  apply Zmult_assoc.
Qed.
Next Obligation.
  repeat split.
  - intros x; simpl.
    destruct x; auto.
  - intros x; simpl.
    apply Zmult_1_r.
Qed.
Canonical Structure Zmult_monoid := Monoid.make Zmult_is_monoid.

(* Ring of '+' & '*' *)
Program Instance Z_is_ring: isRing Zplus_binop 0 Zinv_map Zmult_binop 1.
Next Obligation.
  intros x y; simpl.
  apply Zplus_comm.
Qed.
Next Obligation.
  split; simpl; intros.
  - apply Z.mul_add_distr_l.
  - apply Z.mul_add_distr_r.
Qed.
Canonical Structure Z_ring := Ring.make Z_is_ring.

Compute (1 * 2 + 3).
     (* = 5 *)
     (* : Z *)

Open Scope ring_scope.
Compute (1 * 2 + 3).


Module MonoidHom.
  Open Scope monoid_scope.

  Class spec (M N: Monoid)(f: Map M N) :=
    proof {
        binop: forall x y, f (x * y) == f x * f y;
        ident: f 1 == 1
      }.

  Class type (M N: Monoid) :=
    make {
        map: Map M N;
        prf: spec map
      }.

  Module Ex.
    Existing Instance prf.

    Notation isMonoidHom := spec.
    Notation MonoidHom := type.

    Coercion map: MonoidHom >-> Map.
    Coercion prf: MonoidHom >-> isMonoidHom.
  End Ex.
End MonoidHom.
Export MonoidHom.Ex.

Module GroupHom.
  Open Scope group_scope.

  Class spec (G H: Group)(f: Map G H) :=
    proof {
        binop: forall x y, f (x * y) == f x * f y;
        ident: f 1 == 1;
        inv: forall x, f(x^-1) == (f x)^-1
      }.

  Class type (G H: Group) :=
    make {
        map: Map G H;
        prf: spec map
      }.

  Module Ex.
    Existing Instance prf.

    Notation isGroupHom := spec.
    Notation GroupHom := type.

    Coercion map: GroupHom >-> Map.
    Coercion prf: GroupHom >-> isGroupHom.
  End Ex.
End GroupHom.
Export GroupHom.Ex.

Module RingHom.
  Open Scope ring_scope.

  Class spec (R S: Ring)(f: Map R S) :=
    proof {
        add_group_hom: isGroupHom (G:=Ring.group R)(H:=Ring.group S) f;
        mul_monoid_hom: isMonoidHom (M:=Ring.monoid R)(N:=Ring.monoid S) f
      }.

  Class type (R S: Ring) :=
    make {
        map: Map R S;
        prf: spec map
      }.

  Module Ex.
    Existing Instance add_group_hom.
    Existing Instance mul_monoid_hom.
    Existing Instance prf.

    Notation isRingHom := spec.
    Notation RingHom := type.

    Coercion map: RingHom >-> Map.
    Coercion prf: RingHom >-> isRingHom.
    Coercion add_group_hom: isRingHom >-> isGroupHom.
    Coercion mul_monoid_hom: isRingHom >-> isMonoidHom.
  End Ex.
  Import Ex.

  Canonical Structure group_hom `(f: RingHom R R') := GroupHom.make f.
  Canonical Structure monoid_hom `(f: RingHom R R') := MonoidHom.make f.

  Open Scope ring_scope.
  Definition add_binop `(f: RingHom R R')(x y: R): f (x + y) == f x + f y
    := (GroupHom.binop (f:=group_hom f) x y).
  Definition add_ident `(f: RingHom R R'): f 0 == 0
    := (GroupHom.ident (f:=group_hom f)).
  Definition add_inv `(f: RingHom R R')(x: R): f (x^-1) == f x^-1
    := (GroupHom.inv (f:=group_hom f) x).
  Definition mul_binop `(f: RingHom R R')(x y: R): f (x * y) == f x * f y
    := (MonoidHom.binop (f:=monoid_hom f) x y).
  Definition mul_ident `(f: RingHom R R'): f 1 == 1
    := (MonoidHom.ident (f:=monoid_hom f)).

  Definition equal {R S: Ring}(f g: RingHom R S) := forall x, f x == g x.
End RingHom.
Export RingHom.Ex.

Program Definition id_map (X: Setoid): Map X X := [x :-> x].
Next Obligation.
  now intros x y Heq.
Qed.

Program Definition comp_map {X Y Z: Setoid}(f: Map X Y)(g: Map Y Z): Map X Z :=
  [x :-> g (f x)].
Next Obligation.
  now intros x y H; rewrite H.
Qed.


Section RingHomProps.
  
  Program Instance id_is_rhom (R: Ring): isRingHom (R:=R) (id_map R).
  Next Obligation.
    split; simpl; intros; try now idtac.
  Qed.
  Next Obligation.
    split; simpl; intros; try now idtac.
  Qed.
  Definition id_rhom R := RingHom.make (id_is_rhom R).

  Program Instance comp_is_rhom (R S T: Ring)(f: RingHom R S)(g: RingHom S T): isRingHom (comp_map f g).
  Next Obligation.
    split; simpl; intros.
    - now rewrite !RingHom.add_binop.
    - now rewrite !RingHom.add_ident.
    - now rewrite !RingHom.add_inv.
  Qed.
  Next Obligation.
    split; simpl; intros.
    - now rewrite !RingHom.mul_binop.
    - now rewrite !RingHom.mul_ident.
  Qed.

  Definition comp_rhom R S T f g := RingHom.make (comp_is_rhom R S T f g).

  Definition equiv_ring (R S: Ring) :=
    exists (f: RingHom R S)(g: RingHom S R),
      RingHom.equal (comp_rhom f g) (id_rhom R) /\  RingHom.equal (comp_rhom f g) (id_rhom R).
End RingHomProps.

(* Initial Arrow of Ring *)
Section FromZ.
  Variable (R: Ring).
  Existing Instance Ring.prf.
  Open Scope ring_scope.

  Fixpoint rep_aux (p: positive): R :=
    match p with
    | xH => Ring.e R
    | xO p' => let x := rep_aux p' in x + x
    | xI p' => let x := rep_aux p' in 1 + x + x
    end.
  Arguments rep_aux _%positive.

  Lemma rep_aux_succ:
    forall p: positive,
      rep_aux (Pos.succ p) == 1 + rep_aux p.
  Proof.
    induction p; simpl in *.
    - rewrite IHp.
      rewrite associative.
      rewrite (commute (1 + rep_aux p)).
      now rewrite <- associative.
    - now rewrite associative.
    - reflexivity.
  Qed.

  Lemma rep_aux_add:
    forall p q,
      rep_aux (p + q) == rep_aux p + rep_aux q.
  Proof.
    induction p; simpl; destruct q; simpl.
    - simpl.
      rewrite Pos.add_carry_spec.
      rewrite (rep_aux_succ (p + q)).
      rewrite IHp.
      repeat rewrite <- associative.
      rewrite (Ring.add_commute_l (rep_aux q) 1 _).
      rewrite (Ring.add_commute_l (rep_aux q) (rep_aux p) _).
      now rewrite (Ring.add_commute_l 1 (rep_aux p) (rep_aux q + _)).
    - simpl.
      rewrite IHp.
      repeat rewrite <- associative.
      now rewrite (Ring.add_commute_l (rep_aux q)).
    - simpl.
      rewrite rep_aux_succ.
      repeat rewrite <- associative.
      now rewrite (Ring.add_commute (_ p) 1).
    - rewrite IHp.
      rewrite <- (associative 1 (rep_aux q) _).
      rewrite (Ring.add_commute_l (rep_aux p + rep_aux p) 1).
      repeat rewrite <- associative.
      now rewrite (Ring.add_commute_l (rep_aux q)).
    - rewrite IHp.
      repeat rewrite <- associative.
      now rewrite (Ring.add_commute_l (rep_aux q)).
    - now rewrite (Ring.add_commute _ 1), associative.
    - rewrite (rep_aux_succ q).
      rewrite <- associative.
      rewrite (Ring.add_commute_l (rep_aux q)).
      now rewrite <- associative.
    - now rewrite associative.
    - reflexivity.
  Qed.

  Lemma rep_aux_pred_double:
    forall p,
      rep_aux (Pos.pred_double p) == rep_aux p + rep_aux p + 1 ^-1.
  Proof.
    induction p; simpl; intros.
    - repeat rewrite <- associative.
      rewrite (Ring.add_commute _ (1^-1)).
      rewrite (Ring.add_commute_l (rep_aux p) (1^-1)); simpl.
      now rewrite (associative _ (1^-1)), Ring.add_inv_r, Ring.add_id_l.
    - rewrite IHp.
      rewrite (Ring.add_commute _ (1^-1)) at 1.
      now rewrite (associative 1), Ring.add_inv_r, Ring.add_id_l, associative.
    - now rewrite <- associative, Ring.add_inv_r, Ring.add_id_r.
  Qed.
  
  Program Canonical Structure rep_aux_map: Map positive_setoid R := makeMap rep_aux.
  Next Obligation.
    now intros p q Heq; simpl in *; subst.
  Qed.
  
  Definition rep (z: Z): R :=
    match z with
    | Z0 => 0
    | Zpos p => rep_aux p
    | Zneg p => (rep_aux p)^-1
    end.
  Arguments rep _%Z.

  Program Canonical Structure rep_map: Map Z_ring R := makeMap rep.
  Next Obligation.
    now intros p q Heq; simpl in *; subst.
  Qed.

  Lemma rep_double:
    forall p,
      rep (Z.double p) == rep p + rep p.
  Proof.
    destruct p; simpl.
    - now rewrite Ring.add_id_l.
    - reflexivity.
    - now rewrite (inv_op (G:=Ring.group R)); simpl.
  Qed.
  
  Lemma rep_succ_double:
    forall p,
      rep (Z.succ_double p) == 1 + rep p + rep p.
  Proof.
    destruct p; simpl.
    - now repeat rewrite Ring.add_id_r.
    - reflexivity.
    - rewrite rep_aux_pred_double.
      repeat rewrite (inv_op (G:=R)); simpl.
      now rewrite (inv_inv (G:=R)), associative.
  Qed.

  Lemma rep_pred_double:
    forall p,
      rep (Z.pred_double p) == 1^-1 + rep p + rep p.
  Proof.
    destruct p; simpl.
    - now repeat rewrite Ring.add_id_r.
    - now rewrite rep_aux_pred_double, commute, <- associative.
    - repeat rewrite (inv_op (G:=R)); simpl.
      now rewrite (commute), (commute _ (1^-1)).
  Qed.

  Lemma rep_pos_sub:
    forall p q,
      rep (Z.pos_sub p q) == rep_aux p + (rep_aux q)^-1.
  Proof.
    induction p, q; simpl.
    - rewrite rep_double, IHp.
      repeat rewrite (inv_op (G:=Ring.group R)); simpl.
      repeat rewrite <- associative.
      rewrite (Ring.add_commute _ (1^-1)).
      rewrite (Ring.add_commute_l (rep_aux q ^-1) (1^-1)); simpl.
      do 2 rewrite (Ring.add_commute_l (rep_aux p) (1^-1)); simpl.
      rewrite (associative 1 _).
      rewrite Ring.add_inv_r, Ring.add_id_l.
      now rewrite (Ring.add_commute_l _ (rep_aux p)).
    - rewrite rep_succ_double, IHp.
      rewrite (inv_op (G:=R)); simpl.
      repeat rewrite <- associative.
      now rewrite (Ring.add_commute_l (rep_aux q^-1) (rep_aux p)).
    - rewrite (Ring.add_commute _ (1^-1)), <- associative, (associative _ 1).
      now rewrite Ring.add_inv_l, Ring.add_id_l.
    - rewrite rep_pred_double, IHp, !(inv_op (G:=R)); simpl.
      repeat rewrite <- associative.
      repeat rewrite (Ring.add_commute_l _ (rep_aux p)).
      rewrite (Ring.add_commute_l _ (rep_aux q^-1)); simpl.
      now rewrite (Ring.add_commute (1^-1)).
    - rewrite rep_double, IHp.
      repeat rewrite (inv_op (G:=Ring.group R)); simpl.
      repeat rewrite <- associative.
      now rewrite (Ring.add_commute_l _ (rep_aux p)).
    - apply rep_aux_pred_double.
    - repeat rewrite (inv_op (G:=R)); simpl.
      rewrite (commute _ (1^-1)).
      rewrite !(Ring.add_commute_l (R:=R) _ (1^-1)), associative; simpl.
      now rewrite Ring.add_inv_l, Ring.add_id_l.
    - now rewrite rep_aux_pred_double, (inv_op (G:=R)), (inv_inv (G:=R)); simpl.
    - now rewrite Ring.add_inv_r.
  Qed.
  
  Lemma rep_add:
    forall p q: Z,
      rep (p + q) == rep p + rep q.
  Proof.
    intros [|p|p] [|q|q]; simpl; try (now rewrite ?Ring.add_id_l, ?Ring.add_id_r).
    - now apply rep_aux_add.
    - now apply rep_pos_sub.
    - now rewrite rep_pos_sub, commute.
    - now rewrite rep_aux_add, (inv_op (G:=R)), commute; simpl.
  Qed.

  Lemma rep_aux_mul:
    forall p q,
      rep_aux (p * q) == rep_aux p * rep_aux q.
  Proof.
    induction p; simpl.
    - intros q.
      rewrite rep_aux_add; simpl.
      rewrite !distributive_r.
      rewrite (distributive_r _ _ (rep_aux q)), Ring.mul_id_l.
      now repeat rewrite <- associative, <- IHp.
    - intros.
      now rewrite !distributive_r, <- IHp.
    - intros.
      now rewrite Ring.mul_id_l.
  Qed.
    
  Lemma rep_mul:
    forall p q,
      rep (p * q) == rep p * rep q.
  Proof.
    intros [|p|p] [|q|q]; simpl; try (now rewrite ?ring_mul_0_l, ?ring_mul_0_r).
    - now apply rep_aux_mul.
    - now rewrite rep_aux_mul, <- ring_mul_inv_r.
    - now rewrite rep_aux_mul, <- ring_mul_inv_l.
    - now rewrite rep_aux_mul, <- ring_mul_inv_inv.
  Qed.

  Program Instance rep_is_ring_hom: isRingHom rep_map.
  Next Obligation.
    split; simpl; intros.
    - apply rep_add.
    - reflexivity.
    - destruct x as [|p|p]; simpl.
      + now rewrite (inv_id R).
      + reflexivity.
      + now rewrite (inv_inv (G:=R)).
  Qed.
  Next Obligation.
    split; simpl; intros.
    - apply rep_mul.
    - reflexivity.
  Qed.

  Definition rep_ring_hom: RingHom Z_ring R := RingHom.make rep_is_ring_hom.

  Eval simpl in (rep_ring_hom 0).
     (*   = 0 *)
     (* : R *)
  Eval simpl in (rep_ring_hom 1).
     (* = 1 *)
     (* : R *)
  Eval simpl in (rep_ring_hom 2).
     (* = 1 + 1 *)
     (* : R *)
  Eval simpl in (rep_ring_hom 4).
     (* = 1 + 1 + (1 + 1) *)
     (* : R *)
  Eval simpl in (rep_ring_hom 10).
     (* = 1 + (1 + 1) + (1 + 1) + (1 + (1 + 1) + (1 + 1)) *)
     (* : R *)
  Eval simpl in (rep_ring_hom 33).
     (*   = 1 + *)
     (*   (1 + 1 + (1 + 1) + (1 + 1 + (1 + 1)) + *)
     (*    (1 + 1 + (1 + 1) + (1 + 1 + (1 + 1)))) + *)
     (*   (1 + 1 + (1 + 1) + (1 + 1 + (1 + 1)) + *)
     (*    (1 + 1 + (1 + 1) + (1 + 1 + (1 + 1)))) *)
     (* : R *)
  Eval simpl in (rep_ring_hom 100).
     (* = 1 + (1 + 1 + 1 + (1 + 1 + 1) + (1 + 1 + 1 + (1 + 1 + 1))) + *)
     (*   (1 + 1 + 1 + (1 + 1 + 1) + (1 + 1 + 1 + (1 + 1 + 1))) + *)
     (*   (1 + (1 + 1 + 1 + (1 + 1 + 1) + (1 + 1 + 1 + (1 + 1 + 1))) + *)
     (*    (1 + 1 + 1 + (1 + 1 + 1) + (1 + 1 + 1 + (1 + 1 + 1)))) + *)
     (*   (1 + (1 + 1 + 1 + (1 + 1 + 1) + (1 + 1 + 1 + (1 + 1 + 1))) + *)
     (*    (1 + 1 + 1 + (1 + 1 + 1) + (1 + 1 + 1 + (1 + 1 + 1))) + *)
     (*    (1 + (1 + 1 + 1 + (1 + 1 + 1) + (1 + 1 + 1 + (1 + 1 + 1))) + *)
     (*     (1 + 1 + 1 + (1 + 1 + 1) + (1 + 1 + 1 + (1 + 1 + 1))))) *)
     (* : R *)
End FromZ.

Canonical Structure bool_setoid := Setoid_of (@eq bool).
Coercion bT (b: bool): Prop := b == true.
Arguments bT b /.

Module Ideal.
  Open Scope ring_scope.

  Class spec (R: Ring)(P: R -> Prop) :=
    proof {
        contain_subst: Proper ((==) ==> flip impl) P;
        add_close:
          forall x y,
            P x -> P y -> P (x + y);

        inv_close:
          forall x,
            P x -> P (x^-1);

        z_close:
          P 0;

        mul_close:
          forall x y,
            P x -> P y -> P (x * y);

        left_mul:
          forall a x,
            P x -> P (a * x);

        right_mul:
          forall a x,
            P x -> P (x * a)
      }.

  Structure type (R: Ring) :=
    make {
        contain: R -> Prop;

        prf: spec contain
      }.

  Module Ex.
    Existing Instance prf.
    Existing Instance contain_subst.

    Notation isIdeal := spec.
    Notation Ideal := type.
    
    Coercion prf: Ideal >-> isIdeal.
    Arguments isIdeal (R P): clear implicits.
  End Ex.
End Ideal.
Export Ideal.Ex.

Section Zn.
  Instance Zn_is_ideal (n: Z): isIdeal Z_ring `((x mod n) = 0).
  Proof.
    split.
    - intros x y Heq; simpl in *.
      now intro; rewrite Heq.
    - intros x y; simpl.
      rewrite Zplus_mod.
      now intros H H'; rewrite H, H'.
    - intros x; simpl.
      now apply Z_mod_zero_opp_full.
    - now idtac.
    - intros x y; simpl.
      rewrite Zmult_mod; intros.
      now rewrite H, H0; simpl.
    - intros a x H; simpl.
      now rewrite Zmult_mod, H, Zmult_comm.
    - intros a x H; simpl.
      now rewrite Zmult_mod, H.
  Qed.
  Definition Zn_ideal (n: Z) := Ideal.make (Zn_is_ideal n).

  Goal Ideal.contain (Zn_ideal 2) 10.
  Proof. now idtac. Qed.             
  
  Goal forall n,
      Ideal.contain (Zn_ideal 2) (n * 2).
  Proof.
    simpl; intros.
    now rewrite Zmult_mod, Zmult_comm; simpl.
  Qed.             
  
  Goal forall n,
      ~ Ideal.contain (Zn_ideal 2) (n * 2 + 1).
  Proof.
    intros n H; simpl in H.
    rewrite Zplus_mod in H.
    rewrite Zmult_comm, Zmult_mod in H; simpl.
    compute in H.
    inversion H.
  Qed.
End Zn.

(*
Section Zn.
  Instance Zn_is_ideal (n: Z): isIdeal Z_ring `(Zeq_bool (x mod n) 0).
  Proof.
    split.
    - intros x y Heq; simpl in *.
      now rewrite Heq; auto.
    - intros x y; simpl.
      rewrite Zplus_mod.
      rewrite <- !Zeq_is_eq_bool; intros.
      now rewrite H, H0; simpl.
    - intros x; simpl.
      rewrite <- !Zeq_is_eq_bool; intros.
      now apply Z_mod_zero_opp_full.
    - now simpl.
    - intros x y; simpl.
      rewrite Zmult_mod.
      rewrite <- !Zeq_is_eq_bool; intros.
      now rewrite H, H0; simpl.
    - intros a x; simpl.
      rewrite <- !Zeq_is_eq_bool; intros.
      now rewrite Zmult_mod, H, Zmult_comm.
    - intros a x; simpl.
      rewrite <- !Zeq_is_eq_bool; intros.
      now rewrite Zmult_mod, H.
  Qed.
  Definition Zn_ideal (n: Z) := Ideal.make (Zn_is_ideal n).

  Goal Ideal.contain (Zn_ideal 2) 10.
  Proof. now idtac. Qed.
  
  Goal forall n,
      Ideal.contain (Zn_ideal 2) (n * 2).
  Proof.
    simpl; intros.
    rewrite <- !Zeq_is_eq_bool.
    now rewrite Zmult_mod, Zmult_comm; simpl.
  Qed.
  
  Goal forall n,
      ~ Ideal.contain (Zn_ideal 2) (n * 2 + 1).
  Proof.
    intros n H; simpl in H.
    rewrite <-!Zeq_is_eq_bool, Zplus_mod in H.
    rewrite Zmult_comm, Zmult_mod in H; simpl.
    compute in H.
    inversion H.
  Qed.
End Zn.
*)

Section IdealQuotient.
  Close Scope Z_scope.
  Open Scope ring_scope.

  Definition Ideal_equal (R: Ring)(I: Ideal R): R -> R -> Prop :=
    fun x y => Ideal.contain I (x - y).
  Arguments Ideal_equal R I x y /.

  Program Instance Ideal_equiv `(I: Ideal R): Equivalence (Ideal_equal I).
  Next Obligation.
    intros x; simpl; simpl.
    rewrite Ring.add_inv_r.
    apply Ideal.z_close.
  Qed.
  Next Obligation.
    intros x y Heq; simpl in *.
    rewrite <- (Ring.add_inv_inv (y + x^-1)); simpl.
    apply Ideal.inv_close.
    now rewrite (Ring.add_inv_op y), (Ring.add_inv_inv x); simpl.
  Qed.
  Next Obligation.
    intros x y z Hxy Hyz.
    simpl in *.
    rewrite <- (Ring.add_id_l (z^-1)).
    rewrite <- (Ring.add_inv_l y).
    rewrite !associative.
    rewrite <- (associative (x + y^-1)).
    now apply Ideal.add_close; auto.
  Qed.

  Definition IdealQuotient `(I: Ideal R) := Build_Setoid (Ideal_equiv I).
End IdealQuotient.

Section RingKernel.
  Open Scope ring_scope.
  Variables (R S: Ring)(f: RingHom R S).

  Definition RKernel_spec (x: R) := f x == 0.
  Arguments RKernel_spec x /.
  Definition RKernel := { x | RKernel_spec x }.

  Program Instance RKernel_is_ideal: isIdeal R RKernel_spec.
  Next Obligation.
    intros x y Heq P; simpl in *.
    now rewrite Heq.
  Qed.
  Next Obligation.
    now rewrite RingHom.add_binop, H, H0, Ring.add_id_l.
  Qed.
  Next Obligation.
    now rewrite RingHom.add_inv, H, (Ring.add_inv_id S).
  Qed.
  Next Obligation.
    now rewrite RingHom.add_ident.
  Qed.
  Next Obligation.
    now rewrite RingHom.mul_binop, H, H0, ring_mul_0_r.
  Qed.
  Next Obligation.
    now rewrite RingHom.mul_binop, H, ring_mul_0_r.
  Qed.
  Next Obligation.
    now rewrite RingHom.mul_binop, H, ring_mul_0_l.
  Qed.

  Definition RKernel_ideal := Ideal.make RKernel_is_ideal.

End RingKernel.

Definition ideal_RKernel
           `(I: Ideal R)
           (H: forall x, {Ideal.contain I x} + {~Ideal.contain I x})
           (x: R): R :=
  match H x with
  | left _ => 0
  | right _ => x
  end.


Lemma ideal_RKernel_valid:
  forall `(I: Ideal R)(H: forall x, {Ideal.contain I x} + {~Ideal.contain I x})(x: R),
    Ideal.contain I x <-> ideal_RKernel H x == 0.
Proof.
  intros; split; intros H'; unfold ideal_RKernel in *; destruct (H x); try now auto.
  rewrite H'.
  apply Ideal.z_close.
Qed.