Why3 Standard Library index

Basic Algebra Theories

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

```

Commutativity

```theory Comm

type t
function op t t : t
axiom Comm : forall x y : t. op x y = op y x

end

```

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

```

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

```

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

```

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

end

```

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

```

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

```

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

```

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

```

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

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

```

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

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

```

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

```

Generated by why3doc 0.87.3