(** {1 Basic Algebra Theories} *) (** {2 Associativity} *) theory Assoc type t function op t t : t axiom Assoc : forall x y z : t. op (op x y) z = op x (op y z) end (** {2 Commutativity} *) theory Comm type t function op t t : t axiom Comm : forall x y : t. op x y = op y x end (** {2 Associativity and Commutativity} *) theory AC clone export Assoc clone Comm with type t = t, function op = op meta AC function op (*, prop Assoc.Assoc, prop Comm.Comm*) end (** {2 Monoids} *) theory Monoid clone export Assoc constant unit : t axiom Unit_def_l : forall x:t. op unit x = x axiom Unit_def_r : forall x:t. op x unit = x end (** {2 Commutative Monoids} *) theory CommutativeMonoid clone export Monoid clone Comm with type t = t, function op = op meta AC function op (*, prop Assoc.Assoc, prop Comm.Comm*) end (** {2 Groups} *) theory Group clone export Monoid function inv t : t axiom Inv_def_l : forall x:t. op (inv x) x = unit axiom Inv_def_r : forall x:t. op x (inv x) = unit (*** lemma Inv_unit : forall x y:t. op x (inv y) = unit -> x = y *) end (** {2 Commutative Groups} *) theory CommutativeGroup clone export Group clone Comm with type t = t, function op = op meta AC function op (*, prop Assoc.Assoc, prop Comm.Comm*) end (** {2 Rings} *) theory Ring type t constant zero : t function (+) t t : t function (-_) t : t function (*) t t : t clone CommutativeGroup with type t = t, constant unit = zero, function op = (+), function inv = (-_) clone Assoc with type t = t, function op = (*) axiom Mul_distr_l : forall x y z : t. x * (y + z) = x * y + x * z axiom Mul_distr_r : forall x y z : t. (y + z) * x = y * x + z * x function (-) (x y : t) : t = x + -y end (** {2 Commutative Rings} *) theory CommutativeRing clone export Ring clone Comm with type t = t, function op = (*) meta AC function (*) (*, prop Assoc.Assoc, prop Comm.Comm*) end (** {2 Commutative Rings with Unit} *) theory UnitaryCommutativeRing clone export CommutativeRing constant one : t axiom Unitary : forall x:t. one * x = x axiom NonTrivialRing : zero <> one end (** {2 Ordered Commutative Rings} *) theory OrderedUnitaryCommutativeRing clone export UnitaryCommutativeRing predicate (<=) t t predicate (>=) (x y : t) = y <= x clone export relations.TotalOrder with type t = t, predicate rel = (<=) axiom ZeroLessOne : zero <= one axiom CompatOrderAdd : forall x y z : t. x <= y -> x + z <= y + z axiom CompatOrderMult : forall x y z : t. x <= y -> zero <= z -> x * z <= y * z end (** {2 Field theory} *) theory Field clone export UnitaryCommutativeRing function inv t : t axiom Inverse : forall x:t. x <> zero -> x * inv x = one function (/) (x y : t) : t = x * inv y lemma add_div : forall x y z : t. z <> zero -> (x+y)/z = x/z + y/z lemma sub_div : forall x y z : t. z <> zero -> (x-y)/z = x/z - y/z lemma neg_div : forall x y : t. y <> zero -> (-x)/y = -(x/y) lemma assoc_mul_div: forall x y z:t. (* todo: discard the hypothesis ? *) z <> zero -> (x*y)/z = x*(y/z) lemma assoc_div_mul: forall x y z:t. (* todo: discard the hypothesis ? *) y <> zero /\ z <> zero -> (x/y)/z = x/(y*z) lemma assoc_div_div: forall x y z:t. (* todo: discard the hypothesis ? *) y <> zero /\ z <> zero -> x/(y/z) = (x*z)/y end (** {2 Ordered Fields} *) theory OrderedField clone export Field predicate (<=) t t predicate (>=) (x y : t) = y <= x clone export relations.TotalOrder with type t = t, predicate rel = (<=) axiom ZeroLessOne : zero <= one axiom CompatOrderAdd : forall x y z : t. x <= y -> x + z <= y + z axiom CompatOrderMult : forall x y z : t. x <= y -> zero <= z -> x * z <= y * z end (*** to be discussed: should we add the following lemmas, and where lemma InvMult : forall x y : t. (-x) * y = - (x * y) = x * (-y) lemma InvSquare : forall x : t. x * x = (-x) * (-x) lemma ZeroMult : forall x : t. x * zero = zero = zero * x lemma SquareNonNeg1 : forall x : t. x <= zero -> zero <= x * x lemma SquareNonNeg : forall x : t. zero <= x * x *)