ring.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.

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.

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.

Module Group.
  Class spec (G: Setoid)(op: Binop G)(e: G)(inv: Map G G) :=
    proof {
        is_monoid:> isMonoid op e;
        invertible: Invertible inv
      }.

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

  Module Ex.
    Existing Instance is_monoid.
    Existing Instance invertible.
    Existing Instance prf.

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

    Coercion is_monoid: isGroup >-> isMonoid.
    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.
End Group.
Export Group.Ex.


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 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 "'1'" := (e _): ring_scope.
  End Ex.
  Import Ex.

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


Require Import ZArith.
Open Scope Z_scope.

Print Z.
(* Inductive Z : Set :=  Z0 : Z | Zpos : positive -> Z | Zneg : positive -> Z *)

(* For Zpos: Argument scope is [positive_scope] *)
(* For Zneg: Argument scope is [positive_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 Zplus_is_monoid: isMonoid Zplus_binop 0.
Next Obligation.
  intros x y z; simpl.
  apply Zplus_assoc.
Qed.
Next Obligation.
  repeat split.
  intros x; simpl.
  apply Zplus_0_r.
Qed.
Canonical Structure Zplus_monoid := Monoid.make Zplus_is_monoid.

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 Z.add_opp_diag_l.
  - intros x; simpl.
    apply Z.add_opp_diag_r.
Qed.
Canonical Structure Zgroup_monoid := Group.make Zplus_is_group.

Program Instance Zplus_commute: Commute Zplus_binop.
Next Obligation.
  apply Zplus_comm.
Qed.

(* 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.
  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).
     (* = 5 *)
     (* : Z_ring *)