Why3 Standard Library index

# Basic Algebra Theories

## Associativity

```module 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

```module Comm

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

end

```

## Associativity and Commutativity

```module AC

clone export Assoc with axiom Assoc
clone export Comm with type t = t, function op = op, axiom Comm
meta AC function op

end

```

## Monoids

```module Monoid

clone export Assoc with axiom 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

```module CommutativeMonoid

clone export Monoid with axiom Assoc, axiom Unit_def_l, axiom Unit_def_r
clone export Comm with type t = t, function op = op, axiom Comm
meta AC function op

end

```

## Groups

```module Group

clone export Monoid with axiom Assoc, axiom Unit_def_l, axiom Unit_def_r
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

```module CommutativeGroup

clone export Group with axiom .
clone export Comm with type t = t, function op = op, axiom Comm
meta AC function op

end

```

## Rings

```module Ring

type t
constant zero : t
function (+) t t : t
function (-_) t : t
function (*) t t : t

clone export CommutativeGroup with type t = t,
constant unit = zero,
function op = (+),
function inv = (-_),
axiom .

clone Assoc as MulAssoc with type t = t, function op = (*), axiom Assoc

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

end

```

## Commutative Rings

```module CommutativeRing

clone export Ring with axiom .
clone Comm as MulComm with type t = t, function op = (*), axiom Comm
meta AC function (*)

end

```

## Commutative Rings with Unit

```module UnitaryCommutativeRing

clone export CommutativeRing with axiom .
constant one : t
axiom Unitary : forall x:t. one * x = x
axiom NonTrivialRing : zero <> one

end

```

## Ordered Commutative Rings

```module OrderedUnitaryCommutativeRing

clone export UnitaryCommutativeRing with axiom .

predicate (<=) t t

clone export relations.TotalOrder with
type t = t, predicate rel = (<=), axiom .

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

```module Field

clone export UnitaryCommutativeRing with axiom .

function inv t : t

axiom Inverse : forall x:t. x <> zero -> x * inv x = one

function (-) (x y : t) : t = x + -y
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

```module OrderedField

clone export Field with axiom .

predicate (<=) t t

clone export relations.TotalOrder with
type t = t, predicate rel = (<=), axiom .

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 1.5.0