Section Theory_of_semi_rings.
Variable A : Type.
Variable Aplus : A -> A -> A.
Variable Amult : A -> A -> A.
Variable Aone : A.
Variable Azero : A.
(* There is also a "weakly decidable" equality on A. That means
that if (A_eq x y)=true then x=y but x=y can arise when
(A_eq x y)=false. On an abstract ring the function [x,y:A]false
is a good choice. The proof of A_eq_prop is in this case easy. *)
Variable Aeq : A -> A -> bool.
Record Semi_Ring_Theory : Prop :=
{ SR_plus_sym : (n,m:A)[| n + m == m + n |];
SR_plus_assoc : (n,m,p:A)[| n + (m + p) == (n + m) + p |];
SR_mult_sym : (n,m:A)[| n*m == m*n |];
SR_mult_assoc : (n,m,p:A)[| n*(m*p) == (n*m)*p |];
SR_plus_zero_left :(n:A)[| 0 + n == n|];
SR_mult_one_left : (n:A)[| 1*n == n |];
SR_mult_zero_left : (n:A)[| 0*n == 0 |];
SR_distr_left : (n,m,p:A) [| (n + m)*p == n*p + m*p |];
SR_plus_reg_left : (n,m,p:A)[| n + m == n + p |] -> m==p;
SR_eq_prop : (x,y:A) (Is_true (Aeq x y)) -> x==y
}.
Section Theory_of_rings.
Variable A : Type.
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.
Record Ring_Theory : Prop :=
{ Th_plus_sym : (n,m:A)[| n + m == m + n |];
Th_plus_assoc : (n,m,p:A)[| n + (m + p) == (n + m) + p |];
Th_mult_sym : (n,m:A)[| n*m == m*n |];
Th_mult_assoc : (n,m,p:A)[| n*(m*p) == (n*m)*p |];
Th_plus_zero_left :(n:A)[| 0 + n == n|];
Th_mult_one_left : (n:A)[| 1*n == n |];
Th_opp_def : (n:A) [| n + (-n) == 0 |];
Th_distr_left : (n,m,p:A) [| (n + m)*p == n*p + m*p |];
Th_eq_prop : (x,y:A) (Is_true (Aeq x y)) -> x==y
}.