(***********************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
(*   \VV/  *************************************************************)
(*    //   *      This file is distributed under the terms of the      *)
(*         *       GNU Lesser General Public License Version 2.1       *)
(***********************************************************************)

(* $Id$ *)

Require Export Bool.
Require Export Setoid.

Set Implicit Arguments.

Grammar ring formula : constr :=
  formula_expr [ expr($p) ] -> [$p]
| formula_eq [ expr($p) "==" expr($c) ] -> [ (Aequiv $p $c) ]

with expr : constr :=
  RIGHTA
    expr_plus [ expr($p) "+" expr($c) ] -> [ (Aplus $p $c) ]
  | expr_expr1 [ expr1($p) ] -> [$p]

with expr1 : constr :=
  RIGHTA
    expr1_plus [ expr1($p) "*" expr1($c) ] -> [ (Amult $p $c) ]
  | expr1_final [ final($p) ] -> [$p]

with final : constr :=
  final_var [ prim:var($id) ] -> [ $id ]
| final_constr [ "[" constr:constr($c) "]" ] -> [ $c ]
| final_app [ "(" application($r) ")" ] -> [ $r ]
| final_0 [ "0" ] -> [ Azero ]
| final_1 [ "1" ] -> [ Aone ]
| final_uminus [ "-" expr($c) ] -> [ (Aopp $c) ]

with application : constr :=
  LEFTA
    app_cons [ application($p) application($c1) ] -> [ ($p $c1) ]
  | app_tail [ expr($c1) ] -> [ $c1 ].

Grammar constr constr0 :=
  formula_in_constr [ "[" "|" ring:formula($c) "|" "]" ] -> [ $c ].

Section Setoid_rings.

Variable A : Type.
Variable Aequiv : A -> A -> Prop.

Variable S : (Setoid_Theory A Aequiv).

Add Setoid A Aequiv S.

Variable Aplus : A -> A -> A.
Variable Amult : A -> A -> A.
Variable Aone : A.
Variable Azero : A.
Variable Aopp : A -> A.
Variable Aeq : A -> A -> bool.

Variable plus_morph : (a,a0,a1,a2:A)
 (Aequiv a a0)->(Aequiv a1 a2)->(Aequiv (Aplus a a1) (Aplus a0 a2)).
Variable mult_morph : (a,a0,a1,a2:A)
 (Aequiv a a0)->(Aequiv a1 a2)->(Aequiv (Amult a a1) (Amult a0 a2)).
Variable opp_morph : (a,a0:A)
 (Aequiv a a0)->(Aequiv (Aopp a) (Aopp a0)).

Add Morphism Aplus : Aplus_ext.
Exact plus_morph.
Save.

Add Morphism Amult : Amult_ext.
Exact mult_morph.
Save.

Add Morphism Aopp : Aopp_ext.
Exact opp_morph.
Save.

Section Theory_of_semi_setoid_rings.

Record Semi_Setoid_Ring_Theory : Prop :=
{ SSR_plus_sym  : (n,m:A) [| n + m == m + n |];
  SSR_plus_assoc : (n,m,p:A) [| n + (m + p) == (n + m) + p |];
  SSR_mult_sym : (n,m:A) [| n*m == m*n |];
  SSR_mult_assoc : (n,m,p:A) [| n*(m*p) == (n*m)*p |];
  SSR_plus_zero_left :(n:A) [| 0 + n == n|];
  SSR_mult_one_left : (n:A) [| 1*n == n |];
  SSR_mult_zero_left : (n:A) [| 0*n == 0 |];
  SSR_distr_left : (n,m,p:A) [| (n + m)*p == n*p + m*p |];
  SSR_plus_reg_left : (n,m,p:A)[| n + m == n + p |] -> (Aequiv m p);
  SSR_eq_prop : (x,y:A) (Is_true (Aeq x y)) -> (Aequiv x y)
}.

Variable T : Semi_Setoid_Ring_Theory.

Local plus_sym  := (SSR_plus_sym T).
Local plus_assoc := (SSR_plus_assoc T).
Local mult_sym  := ( SSR_mult_sym T).
Local mult_assoc := (SSR_mult_assoc T).
Local plus_zero_left := (SSR_plus_zero_left T).
Local mult_one_left := (SSR_mult_one_left T). 
Local mult_zero_left := (SSR_mult_zero_left T).
Local distr_left := (SSR_distr_left T).
Local plus_reg_left := (SSR_plus_reg_left T).
Local equiv_refl := (Seq_refl A Aequiv S).
Local equiv_sym := (Seq_sym A Aequiv S).
Local equiv_trans := (Seq_trans A Aequiv S).

Hints Resolve plus_sym plus_assoc mult_sym mult_assoc
  plus_zero_left mult_one_left mult_zero_left distr_left
  plus_reg_left equiv_refl (*equiv_sym*).
Hints Immediate equiv_sym.

(* Lemmas whose form is x=y are also provided in form y=x because
  Auto does not symmetry *) 
Lemma SSR_mult_assoc2 : (n,m,p:A)[| (n * m) * p == n * (m * p) |].
Auto. Save.

Lemma SSR_plus_assoc2 : (n,m,p:A)[| (n + m) + p == n + (m + p) |].
Auto. Save.

Lemma SSR_plus_zero_left2 : (n:A)[| n == 0 + n |].
Auto. Save.

Lemma SSR_mult_one_left2 : (n:A)[| n == 1*n |].
Auto. Save.

Lemma SSR_mult_zero_left2 : (n:A)[| 0 == 0*n |].
Auto. Save.

Lemma SSR_distr_left2 : (n,m,p:A)[| n*p + m*p  == (n + m)*p |].
Auto. Save.

Lemma SSR_plus_permute : (n,m,p:A)[| n+(m+p) == m+(n+p) |].
Intros.
Rewrite (plus_assoc n m p).
Rewrite (plus_sym n m).
Rewrite <- (plus_assoc m n p).
Trivial.
Save.

Lemma SSR_mult_permute : (n,m,p:A) [| n*(m*p) == m*(n*p) |].
Intros.
Rewrite (mult_assoc n m p).
Rewrite (mult_sym n m).
Rewrite <- (mult_assoc m n p).
Trivial.
Save.

Hints Resolve SSR_plus_permute SSR_mult_permute.

Lemma SSR_distr_right : (n,m,p:A) [| n*(m+p) == (n*m) + (n*p) |].
Intros.
Rewrite (mult_sym n (Aplus m p)).
Rewrite (mult_sym n m).
Rewrite (mult_sym n p).
Auto.
Save.

Lemma SSR_distr_right2 : (n,m,p:A) [| (n*m) + (n*p) == n*(m + p) |].
Intros.
Apply equiv_sym.
Apply SSR_distr_right.
Save.

Lemma SSR_mult_zero_right : (n:A)[|  n*0 == 0|].
Intro; Rewrite (mult_sym n Azero); Auto.
Save.

Lemma SSR_mult_zero_right2 : (n:A)[| 0 == n*0 |].
Intro; Rewrite (mult_sym n Azero); Auto.
Save.

Lemma SSR_plus_zero_right :(n:A)[| n + 0 == n |].
Intro; Rewrite (plus_sym n Azero); Auto.
Save.

Lemma SSR_plus_zero_right2 :(n:A)[| n == n + 0 |].
Intro; Rewrite (plus_sym n Azero); Auto.
Save.

Lemma SSR_mult_one_right : (n:A)[| n*1 == n |].
Intro; Rewrite (mult_sym n Aone); Auto.
Save.

Lemma SSR_mult_one_right2 : (n:A)[| n == n*1 |].
Intro; Rewrite (mult_sym n Aone); Auto.
Save.

Lemma SSR_plus_reg_right : (n,m,p:A) [| m+n == p+n |] -> [| m==p |].
Intros n m p; Rewrite (plus_sym m n); Rewrite (plus_sym p n).
Intro; Apply plus_reg_left with n; Trivial.
Save.

End Theory_of_semi_setoid_rings.

Section Theory_of_setoid_rings.

Record Setoid_Ring_Theory : Prop :=
{ STh_plus_sym  : (n,m:A)[| n + m == m + n |];
  STh_plus_assoc : (n,m,p:A)[| n + (m + p) == (n + m) + p |];
  STh_mult_sym : (n,m:A)[| n*m == m*n |];
  STh_mult_assoc : (n,m,p:A)[| n*(m*p) == (n*m)*p |];
  STh_plus_zero_left :(n:A)[| 0 + n == n|];
  STh_mult_one_left : (n:A)[| 1*n == n |];
  STh_opp_def : (n:A) [| n + (-n) == 0 |];
  STh_distr_left : (n,m,p:A) [| (n + m)*p == n*p + m*p |];
  STh_eq_prop : (x,y:A) (Is_true (Aeq x y)) -> (Aequiv x y)
}.

Variable T : Setoid_Ring_Theory.

Local plus_sym  := (STh_plus_sym T).
Local plus_assoc := (STh_plus_assoc T).
Local mult_sym  := (STh_mult_sym T).
Local mult_assoc := (STh_mult_assoc T).
Local plus_zero_left := (STh_plus_zero_left T).
Local mult_one_left := (STh_mult_one_left T). 
Local opp_def := (STh_opp_def T).
Local distr_left := (STh_distr_left T).
Local equiv_refl := (Seq_refl A Aequiv S).
Local equiv_sym := (Seq_sym A Aequiv S).
Local equiv_trans := (Seq_trans A Aequiv S).

Hints Resolve plus_sym plus_assoc mult_sym mult_assoc
  plus_zero_left mult_one_left opp_def distr_left
  equiv_refl equiv_sym.

(* Lemmas whose form is x=y are also provided in form y=x because Auto does
  not symmetry *)

Lemma STh_mult_assoc2 : (n,m,p:A)[| (n * m) * p == n * (m * p) |].
Auto. Save.

Lemma STh_plus_assoc2 : (n,m,p:A)[| (n + m) + p == n + (m + p) |].
Auto. Save.

Lemma STh_plus_zero_left2 : (n:A)[| n == 0 + n |].
Auto. Save.

Lemma STh_mult_one_left2 : (n:A)[| n == 1*n |].
Auto. Save.

Lemma STh_distr_left2 : (n,m,p:A) [| n*p + m*p  == (n + m)*p |].
Auto. Save.

Lemma STh_opp_def2 : (n:A) [| 0 == n + (-n) |].
Auto. Save.

Lemma STh_plus_permute : (n,m,p:A)[| n + (m + p) == m + (n + p) |].
Intros.
Rewrite (plus_assoc n m p).
Rewrite (plus_sym n m).
Rewrite <- (plus_assoc m n p).
Trivial.
Save.

Lemma STh_mult_permute : (n,m,p:A) [| n*(m*p) == m*(n*p) |].
Intros.
Rewrite (mult_assoc n m p).
Rewrite (mult_sym n m).
Rewrite <- (mult_assoc m n p).
Trivial.
Save.

Hints Resolve STh_plus_permute STh_mult_permute.

Lemma Saux1 : (a:A) [| a + a == a |] -> [| a == 0 |].
Intros.
Rewrite <- (plus_zero_left a).
Rewrite (plus_sym Azero a).
Setoid_replace (Aplus a Azero) with (Aplus a (Aplus a (Aopp a))); Auto.
Rewrite (plus_assoc a a (Aopp a)).
Rewrite H.
Apply opp_def.
Save.

Lemma STh_mult_zero_left :(n:A)[| 0*n == 0 |].
Intros.
Apply Saux1.
Rewrite <- (distr_left Azero Azero n).
Rewrite (plus_zero_left Azero).
Trivial.
Save.
Hints Resolve STh_mult_zero_left.

Lemma STh_mult_zero_left2 : (n:A)[| 0 == 0*n |].
Auto.
Save.

Lemma Saux2 : (x,y,z:A) [|x+y==0|] -> [|x+z==0|] -> (Aequiv y z). 
Intros.
Rewrite <- (plus_zero_left y).
Rewrite <- H0.
Rewrite <- (plus_assoc x z y).
Rewrite (plus_sym z y).
Rewrite (plus_assoc x y z).
Rewrite H.
Auto.
Save.

Lemma STh_opp_mult_left : (x,y:A)[| -(x*y) == (-x)*y |].
Intros.
Apply Saux2 with (Amult x y); Auto.
Rewrite <- (distr_left x (Aopp x) y).
Rewrite (opp_def x).
Auto.
Save.
Hints Resolve STh_opp_mult_left.

Lemma STh_opp_mult_left2 : (x,y:A)[| (-x)*y == -(x*y)  |].
Auto.
Save.

Lemma STh_mult_zero_right : (n:A)[| n*0 == 0|].
Intro; Rewrite (mult_sym n Azero); Auto.
Save.

Lemma STh_mult_zero_right2 : (n:A)[| 0 == n*0 |].
Intro; Rewrite (mult_sym n Azero); Auto.
Save.

Lemma STh_plus_zero_right :(n:A)[| n + 0 == n |].
Intro; Rewrite (plus_sym n Azero); Auto.
Save.

Lemma STh_plus_zero_right2 :(n:A)[| n == n + 0 |].
Intro; Rewrite (plus_sym n Azero); Auto.
Save.

Lemma STh_mult_one_right : (n:A)[| n*1 == n |].
Intro; Rewrite (mult_sym n Aone); Auto.
Save.

Lemma STh_mult_one_right2  : (n:A)[| n == n*1 |].
Intro; Rewrite (mult_sym n Aone); Auto.
Save.

Lemma STh_opp_mult_right : (x,y:A)[| -(x*y) == x*(-y) |].
Intros.
Rewrite (mult_sym x y).
Rewrite (mult_sym x (Aopp y)).
Auto.
Save.

Lemma STh_opp_mult_right2 : (x,y:A)[| x*(-y) == -(x*y) |].
Intros.
Rewrite (mult_sym x y).
Rewrite (mult_sym x (Aopp y)).
Auto.
Save.

Lemma STh_plus_opp_opp : (x,y:A)[| (-x) + (-y) == -(x+y) |].
Intros.
Apply Saux2 with (Aplus x y); Auto.
Rewrite (STh_plus_permute (Aplus x y) (Aopp x) (Aopp y)).
Rewrite <- (plus_assoc x y (Aopp y)).
Rewrite (opp_def y); Rewrite (STh_plus_zero_right x).
Rewrite (STh_opp_def2 x); Trivial.
Save.

Lemma STh_plus_permute_opp: (n,m,p:A)[| (-m)+(n+p) == n+((-m)+p) |].
Auto.
Save.

Lemma STh_opp_opp : (n:A)[| -(-n) == n |].
Intro.
Apply Saux2 with (Aopp n); Auto.
Rewrite (plus_sym (Aopp n) n); Auto.
Save.
Hints Resolve STh_opp_opp.

Lemma STh_opp_opp2 : (n:A)[| n == -(-n) |].
Auto.
Save.

Lemma STh_mult_opp_opp : (x,y:A)[| (-x)*(-y) == x*y |].
Intros.
Rewrite (STh_opp_mult_left2 x (Aopp y)).
Rewrite (STh_opp_mult_right2 x y).
Trivial.
Save.

Lemma STh_mult_opp_opp2 : (x,y:A)[| x*y == (-x)*(-y) |].
Intros.
Apply equiv_sym.
Apply STh_mult_opp_opp.
Save.

Lemma STh_opp_zero :[| -0 == 0 |].
Rewrite <- (plus_zero_left (Aopp Azero)).
Trivial.
Save.

Lemma STh_plus_reg_left : (n,m,p:A)[| n+m == n+p |] -> [|m==p|].
Intros.
Rewrite <- (plus_zero_left m).
Rewrite <- (plus_zero_left p).
Rewrite <- (opp_def n).
Rewrite (plus_sym n (Aopp n)).
Rewrite <- (plus_assoc (Aopp n) n m).
Rewrite <- (plus_assoc (Aopp n) n p).
Auto.
Save.

Lemma STh_plus_reg_right : (n,m,p:A)[| m+n == p+n |] -> [|m==p|].
Intros.
Apply STh_plus_reg_left with n.
Rewrite (plus_sym n m); Rewrite (plus_sym n p);
Assumption.
Save.

Lemma STh_distr_right : (n,m,p:A)[|n*(m+p) == (n*m)+(n*p)|].
Intros.
Rewrite (mult_sym n (Aplus m p)).
Rewrite (mult_sym n m).
Rewrite (mult_sym n p).
Trivial.
Save.

Lemma STh_distr_right2 : (n,m,p:A)(Aequiv (Aplus (Amult n m) (Amult n p)) (Amult n (Aplus m p))).
Intros.
Apply equiv_sym.
Apply STh_distr_right.
Save.

End Theory_of_setoid_rings.

Hints Resolve STh_mult_zero_left STh_plus_reg_left : core.

Unset Implicit Arguments.

Definition Semi_Setoid_Ring_Theory_of :
  Setoid_Ring_Theory -> Semi_Setoid_Ring_Theory.
Intros until 1; Case H.
Split; Intros; Simpl; EAuto.
Defined.

Coercion Semi_Setoid_Ring_Theory_of :
  Setoid_Ring_Theory >-> Semi_Setoid_Ring_Theory.



Section product_ring.

End product_ring.

Section power_ring.

End power_ring.

End Setoid_rings.