Require Import Program.
Require Import Setoid.
Require Import Prelude.Basics.

Open Local Scope equiv_scope.

Open Local Scope signature_scope.

Class SemiRing (α : Setoid) := {
  plus : α -> α -> α ;  
  plus_mor :> Proper (seq ==> seq ==> seq) plus ;

  mult : α -> α -> α ;
  mult_mor :> Proper (seq ==> seq ==> seq) mult ;
   
  zero : α ;
  one : α ;
  
  plus_assoc :> Associative seq plus ;
  mult_assoc :> Associative seq mult ;

  plus_comm :> Commutative seq plus ;
  
  mult_plus :> Distributive seq mult plus ;
  
  plus_zero :> Neutral seq plus zero ;

  mult_one :> Neutral seq mult one ;
  mult_zero :> Absorbant seq mult zero }.

Class Ring α := {
  SR :> SemiRing α ;
  opp : α -> α ; 
  opp_mor :> Proper (seq ==> seq) opp ;

  opp_inverse :> Inverse seq plus opp zero }.

Class CommutativeRing α := {
  R :> Ring α ;
  mult_comm :> Commutative seq mult }.

Notation "- x" := (opp x).
Infix "+" := plus.
Infix "*" := mult.
Notation "0" := zero.
Notation "1" := one.

Definition minus `{ R : Ring α } (x y : α) : α := x + - y.
Infix "-" := minus.

Class Field α := {
  CR :> CommutativeRing α ;
  inv : α -> α ;
  inv_mor :> Proper (seq ==> seq) inv ;
  
  two_elems : ~ 1 === 0 ;

  inv_inverse : Π x, ~ x === 0 -> x * inv x === 1 }.

Notation " / x " := (inv x).
Definition div `{ F : Field α } (x y : α) : α := x * / y.
Infix " / " := div.

Typeclasses Opaque plus opp minus mult inv div.

Section Ring. 
  Context `{ R : Ring α }.

  Global Instance minus_mor : Proper (seq ==> seq ==> seq) minus.
  Proof. simpl_relation. unfold minus. rewrite H, H0. reflexivity. Qed.
    
  Lemma plus_left (x y : α) : x === y -> Π z, z + x === z + y.
  Proof.
    intros. rewrite H. reflexivity.
  Qed.
  
  Lemma plus_right (x y : α) : x === y -> Π z, x + z === y + z.
  Proof.
    intros. rewrite H. reflexivity.
  Qed.

  Lemma minus_refl (x : α) : x - x === 0.
  Proof.
    intros. unfold minus. rewrite (right_inverse x). reflexivity.
  Qed.

  Lemma plus_cancel_left (x y : α) : Π z, z + x === z + y -> x === y.
  Proof.
    intros. setoid_replace x with ((z - z) + x). setoid_replace y with ((z - z) + y).
    unfold minus. setoid_rewrite <- (assoc (f:=plus)) at 1 2.
    setoid_rewrite (commutative (f:=plus)) at 2 4. setoid_rewrite (assoc (f:=plus)) at 1 2.
    rewrite H. reflexivity.
    
    rewrite minus_refl. rewrite (left_neutral (f:=plus)). reflexivity.
    rewrite minus_refl. rewrite (left_neutral (f:=plus)). reflexivity.
  Qed.

  Lemma plus_cancel_right (x y : α) : Π z, x + z === y + z -> x === y.
  Proof.
    intros. apply plus_cancel_left with z. setoid_rewrite (commutative (f:=plus)). assumption.
  Qed.

(*
Instance mult_zero [ Ring α ] : Absorbant mult zero.
Proof. intros. 
  constructor ; red ; intros.
  assert(0 * x + 0 * x === 0 * x). 
  rewrite <- (right_distributive (f:=mult)).
  rewrite (left_neutral (f:=plus)). reflexivity.

  apply plus_cancel_right with (0 * x - 0 * x).
  unfold minus at 1. rewrite (assoc (f:=plus)).
  rewrite (left_neutral (f:=plus)). 
  rewrite H. reflexivity.

  red ; intros.
  assert(x * 0 + x * 0 === x * 0). 
  rewrite <- (left_distributive (f:=mult)).
  rewrite (right_neutral (f:=plus)). reflexivity.

  unfold flip.
  apply plus_cancel_right with (x * 0 - x * 0).
  unfold minus at 1. rewrite (assoc (f:=plus)).
  rewrite (left_neutral (f:=plus)). 
  rewrite H. reflexivity.
Qed.
*)

  Lemma mult_minus_l (x y : α) : - x * y === - (x * y).
  Proof.
    intros. apply plus_cancel_left with (x * y).
    fold (x * y - x * y). rewrite minus_refl.
    setoid_rewrite <- (right_distributive (f:=mult) (g:=plus)).
    rewrite (minus_refl x). rewrite (left_absorbant (f:=mult)). reflexivity.
  Qed.
  
  Lemma mult_minus_1 (x : α) : - (1) * x === - x.
  Proof. intros. rewrite mult_minus_l. 
    rewrite (left_neutral (f:=mult) x). reflexivity.
  Qed.
  
  Lemma zero_opp_zero : 0 === - 0.
  Proof. intros. rewrite <- mult_minus_1.
    rewrite (right_absorbant (f:=mult)). reflexivity.
  Qed.

  Lemma mult_minus_r (x y : α) : x * - y === - (x * y).
  Proof.
    intros. apply plus_cancel_left with (x * y).
    fold (x * y - x * y). rewrite minus_refl.
    setoid_rewrite <- (left_distributive (f:=mult) (g:=plus)).
    rewrite (minus_refl y). rewrite (right_absorbant (f:=mult)). reflexivity.
  Qed.

  Lemma minus_plus (x y : α) : - (x + y) === - x + - y.
  Proof.
    intros. apply plus_cancel_left with (x + y).
    fold (x + y - (x + y)). rewrite minus_refl.
    rewrite (assoc (f:=plus)). rewrite (commutative (f:=plus)).
    rewrite (assoc (f:=plus)). rewrite (commutative (f:=plus) x). 
    do 2 rewrite <- (assoc (f:=plus)). rewrite (right_inverse x).
    rewrite (right_neutral (f:=plus) y). rewrite left_inverse. reflexivity.
  Qed.

End Ring.

Require Import Arith.

Definition natS := eq_setoid nat.

Canonical Structure natS.

Program Instance nat_num : SemiRing natS := {
  plus := Peano.plus ;
  mult := Peano.mult ;
  zero := 0%nat ;
  one := 1%nat }.

  Solve Obligations using try constructor ; reduce ; unfold flip ; auto with arith.

  Next Obligation. constructor ; repeat (red ; intros) ; unfold flip ; try ring. Qed.

Require Import ZArith.

Definition ZS := eq_setoid Z.

Canonical Structure ZS.

Program Instance Z_semiring : SemiRing ZS := {
  plus := Zplus ;
  mult := Zmult ;
  zero := Z0 ;
  one := 1%Z }.

  Solve Obligations using try typeclasses eauto.
  Solve Obligations using try constructor ; reduce ; unfold const, flip, id ; auto with zarith.

Program Instance Z_ring : Ring ZS := {
  opp := Zopp }.

  Solve Obligations using try constructor ; reduce ; unfold flip ; auto with zarith.

Require Import QArith.

Definition Q_setoid : Setoid := mkSetoid Q Qeq Q_Setoid.

Hint Unfold make_infix.

Tactic Notation "ring" "*" := autounfold with typeclass_instances; ring.

Program Instance Q_semiring : SemiRing Q_setoid := {
  plus := Qplus ;
  mult := Qmult ;
  zero := 0%Q ;
  one := 1%Q }.

  Solve Obligations using try constructor ; reduce ; unfold const, flip, id ; auto with qarith ; try red ; try ring*.

  Next Obligation. apply* Qplus_assoc. Qed.
  Next Obligation. apply* Qmult_assoc. Qed.
  Next Obligation. apply* Qplus_comm. Qed.

  Next Obligation. 
    constructor. apply* Qmult_plus_distr_r. 
    do 2 red. intros. apply Qmult_plus_distr_l.
  Qed.

  Next Obligation. 
    constructor ; red ; unfold LeftNeutral, LeftLaw, flip, id, const; intros; red; try ring*.
  Qed.

  Next Obligation. 
    constructor ; do 2 red ; intros ; 
      unfold LeftLaw, make_infix, flip, const, id, Equivalence.equiv ; intros ; try ring*.
  Qed.

  Next Obligation. 
    constructor ; do 2 red ; intros ; 
      unfold LeftLaw, make_infix, flip, const, id, Equivalence.equiv ; intros ; try ring*.
  Qed.

Program Instance Q_ring : Ring Q_setoid := {
  opp := Qopp }.

  Solve Obligations using try constructor ; reduce ; unfold flip ; auto with qarith.

  Next Obligation.
    constructor ; do 2 red ; intros ; 
      unfold LeftLaw, make_infix, flip, const, id, Equivalence.equiv ; intros ; try ring*.
  Qed.

Program Instance Q_commring : CommutativeRing Q_setoid.

  Next Obligation. apply* Qmult_comm. Qed.

Close Scope Q_scope.

Canonical Structure Q_setoid.

(* Require Import Reals. *)

(* Program Instance R_semiring : SemiRing (@eq_equivalence R) := *)
(*   plus := Rplus ; *)
(*   mult := Rmult ; *)
(*   zero := 0%R ; *)
(*   one := 1%R. *)

(*   Solve Obligations using try constructor ; reduce ; unfold flip ; auto with real. *)

(*   Next Obligation. typeclasses eauto. Qed. *)
(*   Next Obligation. typeclasses eauto. Qed. *)
(*   Next Obligation.  *)
(*     constructor; do 2 red ; unfold flip ; intros; try red; ring.  *)
(*   Qed. *)

(* Program Instance R_ring : Ring R_semiring := *)
(*   opp := Ropp. *)

(*   Solve Obligations using try constructor ; reduce ; unfold flip ; auto with real. *)

(* Program Instance R_commring : CommutativeRing R_ring. *)

(*   Solve Obligations using try constructor ; reduce ; unfold flip ; auto with real. *)

Check (fun x : Z => x + 1 * 1).
Check (fun x : Q => x + 1 * 1).

Eval compute in (0 + 1 * 1 : Q).

Require Import Ring.

Definition semi_ring_of_SemiRing `(SemiRing α, ! Commutative seq mult) : semi_ring_theory 0 1 plus mult (==).
Proof. constructor.
  destruct plus_zero ; intuition.
  intros. rewrite <- (commutative (f:=plus)). reflexivity.
  intros. rewrite <- (assoc (f:=plus)). reflexivity.
  destruct mult_one. intuition.
  destruct mult_zero. intuition.
  
  apply (commutative (f:=mult)). 
  intros. apply (assoc (f:=mult)). 
  intros.
  unfold flip in *. rewrite <- right_distributive.
  reflexivity.
Qed.

(* Definition SemiRing_of_semi_ring (α : Setoid) (zero : α) one plus mult equiv : *)
(*   semi_ring_theory zero one plus mult equiv -> SemiRing α. *)
(* Proof. intros.  *)
(*   destruct H. *)
(*   econstructor. plus0. apply  *)
(*   destruct plus_zero ; intuition. *)
(*   intros. rewrite <- (commutative (f:=plus)). reflexivity. *)
(*   intros. rewrite <- (assoc (f:=plus)). reflexivity. *)
(*   destruct mult_one. intuition. *)
(*   destruct mult_zero. intuition. *)
  
(*   apply (commutative (f:=mult)).  *)
(*   intros. apply (assoc (f:=mult)).  *)
(*   intros. *)
(*   unfold flip in *. rewrite <- right_distributive. *)
(*   reflexivity. *)
(* Qed. *)

Typeclasses Transparent make_infix.

Definition ring_of_CommutativeRing `(CommutativeRing α) : 
  ring_theory 0 1 plus mult minus opp (@seq α).
Proof with typeclasses eauto || (try reflexivity). 
  intros. constructor ; intros.
  apply left_neutral. apply commutative. apply assoc. apply left_neutral.
  apply commutative. apply assoc. apply right_distributive. 
  unfold minus. reflexivity. apply right_inverse.
Qed.

Require Import Field.

Definition field_of_Field `(Field α) :
  field_theory 0 1 plus mult minus opp div inv (==).
Proof with try typeclasses eauto. 
  intros. constructor ; intros. apply @ring_of_CommutativeRing.
  apply (two_elems (α:=α)). 
  intros. unfold div. reflexivity.
  intros. setoid_rewrite @commutative at 2... apply (inv_inverse p). 
  assumption.
Qed.

(* Definition Field_of_field {α : Setoid} (zero : α) one plus mult minus opp div inv equiv :  *)
(*   field_theory zero one plus mult minus opp div inv equiv -> Field α. *)
(* Proof with try typeclasses eauto.  *)
(*   intros. red. constructor. ; intros. apply @ring_of_CommutativeRing. *)
(*   apply (two_elems (α:=α)).  *)
(*   intros. unfold div. reflexivity. *)
(*   intros. setoid_rewrite @commutative at 2... apply (inv_inverse p).  *)
(*   assumption. *)
(* Qed. *)


Fixpoint from_natural `{SemiRing α} (n : nat) : α :=
  match n with
    | 0 => 0
    | S n' => 1 + from_natural n'
  end.

Definition from_Z `{Ring α} (z : Z) : α :=
  match z with
    | Z0 => 0
    | Zpos p => from_natural (nat_of_P p)
    | Zneg p => - (from_natural (nat_of_P p))
  end.