# Library Coqtail.Hierarchy.Type_class_definition_beta

Require Import Coq.Relations.Relation_Definitions.
Require Import SetoidClass.
Require Import Reals.

Open Scope R_scope.

Definition operation A := AAA.

Class Associative {A : Type} (P : AProp) (rel : relation A) (O : operation A) :=
op_assoc : x y z, P xP yP zrel (O x (O y z)) (O (O x y) z).

Class Commutative {A : Type} (P : AProp) (rel : relation A) (O : operation A) :=
op_comm : x y, P xP yrel (O x y) (O y x).

Definition scalar A B := ABB.

Definition value A := AR.

Class Morphism_value {A : Type} (rel : relation A) (abs : value A) :=
val_compat_eq : a a' : A, rel a a'(abs a) = (abs a').

Class Morphism_arit_2 {A : Type} {B : Type} (rel_a : relation A) (rel_b : relation B) (O : ABB) := {
op_compat_eq_l : a a' : A, b : B, rel_a a a'rel_b (O a b) (O a' b) ;
op_compat_eq_r : a : A, b b' : B, rel_b b b'rel_b (O a b) (O a b')
}.

Class Metric_Space (A : Type) (P : AProp) (eqA : relation A) (d : AAR) := {
metric_space_setoid :> Equivalence eqA ;
metric_space_positive : x y : A, P xP y → 0 d x y ;
metric_space_symmetry : x y : A, P xP yd x y = d y x ;
metric_space_separation : x y : A, P xP y(0 = d x yeqA x y) (eqA x y → 0 = d x y);
metric_space_triangular_inequality : x y z : A, P xP yP zd x z (d x y) + (d y z)
}.

Class Monoid (M : Type) (P : MProp) (eqM : relation M) (f : operation M) (eps : M) := {
monoid_setoid :> Equivalence eqM ;
monoid_eq_compat :> Morphism_arit_2 eqM eqM f ;
monoid_contains_eps : P eps ;
monoid_iden_l : x : M, P xeqM (f eps x) x ;
monoid_iden_r : x : M, P xeqM (f x eps) x ;
monoid_assoc :> Associative P eqM f
}.

Class Monoid_Commutative (M : Type) (P : MProp) (eqM : relation M) (f : operation M) (eps : M) := {
monoid_comm_monoid :> Monoid M P eqM f eps ;
monoid_comm :> Commutative P eqM f
}.

Class Group (G : Type) (P : GProp) (eqG : relation G) (f : operation G) (eps : G) := {
group_monoid :> Monoid G P eqG f eps;
group_reverse : x : G, P x y : G, (P y) (eqG (f x y) eps)
}.

Class Group_Commutative (G : Type) (P : GProp) (eqG : relation G) (f : operation G) (eps : G) := {
group_comm_group :> Group G P eqG f eps ;
group_comm :> Commutative P eqG f
}.
Class SemiRing (S : Type) (P : SProp) (eqS : relation S) (add : operation S) (mult : operation S) (eps0 : S) (eps1 : S) := {
semiring_monoid_comm :> Monoid_Commutative S P eqS add eps0 ;
semiring_monoid :> Monoid S P eqS mult eps1 ;
semiring_distributive_r : x y z : S, P xP yP zeqS (mult x (add y z)) (add (mult x y) (mult x z)) ;
semiring_distributive_l : x y z : S, P xP yP zeqS (mult (add x y) z) (add (mult x z) (mult y z)) ;
semiring_absorption_r : x : S, P xeqS (mult x eps0) eps0 ;
semiring_absorption_l : x : S, P xeqS (mult eps0 x) eps0
}.

Class SemiRing_Commutative (S : Type) (P : SProp) (eqS : relation S) (add : operation S) (mult : operation S) (eps0 : S) (eps1 : S) := {
semiring_comm_semiring :> SemiRing S P eqS add mult eps0 eps1 ;
semiring_comm :> Commutative P eqS mult
}.

Class Ring (R : Type) (P : RProp) (eqR : relation R) (add : operation R) (mult : operation R) (eps0 : R) (eps1 : R) := {
ring_group_comm :> Group_Commutative R P eqR add eps0 ;
ring_monoid :> Monoid R P eqR mult eps1 ;
ring_distributive_r : x y z : R, P xP yP zeqR (mult x (add y z)) (add (mult x y) (mult x z)) ;
ring_distributive_l : x y z : R, P xP yP zeqR (mult (add x y) z) (add (mult x z) (mult y z))
}.

Class Ring_Commutative (R : Type) (P : RProp) (eqR : relation R) (add : operation R) (mult : operation R) (eps0 : R) (eps1 : R) := {
ring_comm_ring :> Ring R P eqR add mult eps0 eps1 ;
ring_comm :> Commutative P eqR mult
}.

Class Field (F : Type) (P : FProp) (eqF : relation F) (add : operation F) (mult : operation F) (eps0 : F) (eps1 : F) := {
field_group_comm :> Group_Commutative F P eqF add eps0 ;
field_group_multiplicative :> Group F (fun x:F(P x)/\~(eqF x eps0)) eqF mult eps1 ;
field_distributive_r : x y z : F, P xP yP zeqF (mult x (add y z)) (add (mult x y) (mult x z)) ;
field_distributive_l : x y z : F, P xP yP zeqF (mult (add x y) z) (add (mult x z) (mult y z))
}.

Class Field_Commutative (F : Type) (P : FProp) (eqF : relation F) (add : operation F) (mult : operation F) (eps0 : F) (eps1 : F) := {
field_comm_field :> Field F P eqF add mult eps0 eps1 ;
field_comm :> Commutative P eqF mult
}.

Class Field_Valued (F : Type) (P : FProp) (eqF : relation F) (add : operation F) (mult : operation F) (eps0 : F) (eps1 : F) (abs : value F) := {
field_valued_field_commutative :> Field_Commutative F P eqF add mult eps0 eps1 ;
field_valued_eq_compat :> Morphism_value eqF abs ;
field_valued_positive : x : F, P x → 0 (abs x) ;
field_valued_separation : (abs eps0) = 0 x : F, P x(abs x) = 0 → eqF x eps0 ;
field_valued_triangular_inequality : x y : F, P xP yabs (add x y) (abs x) + (abs y);
field_valued_homogeneity : x y : F, P xP yabs (mult x y) = (abs x) × (abs y)
}.

Class Vector_Space (E : Type) (P : EProp) (eqE : relation E) (F : Type) (Q : FProp) (eqF : relation F)
(v_add : operation E) (v_mult : scalar F E)
(add : operation F) (mult : operation F)
(v_null : E)
(eps0 : F) (eps1 : F):= {
vector_space_field :> Field_Commutative F Q eqF add mult eps0 eps1 ;
vector_space_group_comm :> Group_Commutative E P eqE v_add v_null ;
vector_space_eq_compat :> Morphism_arit_2 eqF eqE v_mult ;
vector_space_distributive_r : a : F, x y : E, Q aP xP yeqE (v_mult a (v_add x y)) (v_add (v_mult a x) (v_mult a y)) ;
vector_space_distributive_l : a b : F, x : E, Q aQ bP xeqE (v_mult (add a b) x) (v_add (v_mult a x) (v_mult b x)) ;
vector_space_assoc : a b : F, x : E, Q aQ bP xeqE (v_mult (mult a b) x) (v_mult a (v_mult b x)) ;
vector_space_iden_l : a : F, x : E, Q aP xeqE (v_mult eps1 x) x
}.

Class Vector_Space_Normed (E : Type) (P : EProp) (eqE : relation E) (F : Type) (Q : FProp) (eqF : relation F)
(v_add : operation E) (v_mult : scalar F E)
(add : operation F) (mult : operation F)
(v_null : E)
(eps0 : F) (eps1 : F)
(norm: value E) (abs : value F) := {
vector_space_normed_field_valued :> Field_Valued F Q eqF add mult eps0 eps1 abs ;
vector_space_normed_vector_space :> Vector_Space E P eqE F Q eqF v_add v_mult add mult v_null eps0 eps1 ;
vector_space_normed_separation : v : E, P v(norm v) = 0 → eqE v v_null ;
vector_space_normed_triangular_inequality : v w : E, P vP wnorm (v_add v w) (norm v) + (norm w) ;
vector_space_normed_homogeneity : x : F, v : E, Q xP vnorm (v_mult x v) = (abs x) × (norm v)
}.