# Library Coqtail.Hierarchy.Type_class_definition

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

Open Scope R_scope.

Definition operation A := AAA.

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

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

Definition scalar A B := ABB.

Definition value A := AR.

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

Class Monoid (M : Type) (eqM : relation M) (f : operation M) (eps : M) := {
monoid_setoid :> Equivalence eqM ;
monoid_iden_l : x : M, eqM (f eps x) x ;
monoid_iden_r : x : M, eqM (f x eps) x ;
monoid_assoc :> Associative eqM f;
monoid_eq_compat_l : x y z : M, eqM y zeqM (f x y) (f x z);
monoid_eq_compat_r: x y z : M, eqM x yeqM (f x z) (f y z)
}.

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

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

Class Group_Commutative (G : Type) (eqG : relation G) (f : operation G) (eps : G) := {
group_comm_group :> Group G eqG f eps ;
group_comm :> Commutative eqG f
}.

Class Group_Multiplicative (G : Type) (eqG : relation G) (mult : operation G) (eps0 : G) (eps1 : G) := {
group_setoid :> Equivalence eqG ;
group_multiplicative_iden_l : x : G, eqG (mult eps1 x) x ;
group_multiplicative_iden_r : x : G, eqG (mult x eps1) x ;
group_multiplicative_reverse : x : G, ~(eqG x eps0)sig (fun yeqG (mult x y) eps1);
group_multiplicative_assoc :> Associative eqG mult;
group_multiplicative_eq_compat_l : x y z : G, eqG y zeqG (mult x y) (mult x z);
group_multiplicative_eq_compat_r: x y z : G, eqG x yeqG (mult x z) (mult y z)
}.

Class SemiRing (S : Type) (eqS : relation S) (add : operation S) (mult : operation S) (eps0 : S) (eps1 : S) := {
semiring_monoid_comm :> Monoid_Commutative S eqS add eps0 ;
semiring_monoid :> Monoid S eqS mult eps1 ;
semiring_distributive_r : x y z : S, eqS (mult x (add y z)) (add (mult x y) (mult x z)) ;
semiring_distributive_l : x y z : S, eqS (mult (add x y) z) (add (mult x z) (mult y z)) ;
semiring_absorption_r : x : S, eqS (mult x eps0) eps0 ;
semiring_absorption_l : x : S, eqS (mult eps0 x) eps0
}.

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

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

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

Class Field (F : Type) (eqF : relation F) (add : operation F) (mult : operation F) (eps0 : F) (eps1 : F) := {
field_group_comm :> Group_Commutative F eqF add eps0 ;
field_group_multiplicative :> Group_Multiplicative F eqF mult eps0 eps1 ;
field_distributive_r : x y z : F, eqF (mult x (add y z)) (add (mult x y) (mult x z)) ;
field_distributive_l : x y z : F, eqF (mult (add x y) z) (add (mult x z) (mult y z))
}.

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

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

Class Vector_Space (E : Type) (eqE : relation E) (F : Type) (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 eqF add mult eps0 eps1 ;
vector_space_group_comm :> Group_Commutative E eqE v_add v_null ;
vector_space_distributive_r : a : F, x y : E, eqE (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, eqE (v_mult (add a b) x) (v_add (v_mult a x) (v_mult b x)) ;
vector_space_assoc : a b : F, x : E, eqE (v_mult (mult a b) x) (v_mult a (v_mult b x)) ;
vector_space_iden_l : a : F, x : E, eqE (v_mult eps1 x) x;
vector_space_eq_compat_l : a : F, x y :E, eqE x yeqE (v_mult a x) (v_mult a y);
vector_space_eq_compat_r : a b : F, x : E, eqF a b → (eqE (v_mult a x) (v_mult b x))
}.

Class Vector_Space_Normed (E : Type) (eqE : relation E) (F : Type) (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 eqF add mult eps0 eps1 abs ;
vector_space_normed_vector_space :> Vector_Space E eqE F eqF v_add v_mult add mult v_null eps0 eps1 ;
vector_space_normed_separation : v : E, (norm v) = 0 → eqE v v_null ;
vector_space_normed_triangular_inequality : v w : E, norm (v_add v w) (norm v) + (norm w) ;
vector_space_normed_homogeneity : x : F, v : E, norm (v_mult x v) = (abs x) × (norm v)
}.

Close Scope R_scope.