# Library prosa.util.rel

From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq.

In this section, we define the notion of monotonicity for functions.
Section MonotoneFunction.

Consider a type T, a relation R over type T, and a function f : T T.
Context {T : Type}.
Variable R : rel T.
Variable f : T T.

We say that function f is monotone with respect to relation R, iff R x y implies R (f x) (f y) for any x y : T.
Definition monotone :=
x y, R x y R (f x) (f y).

End MonotoneFunction.

In this section, we define some properties of relations on lists.
Section Order.

Consider a type T, a relation R over type T, and a sequence xs.
Context {T : eqType}.
Variable R : T T bool.
Variable xs : seq T.

Relation R is total over list xs, iff for any x1 x2 \in xs, either R x1 x2 or R x2 x1 holds.
Definition total_over_list :=
x1 x2,
x1 \in xs
x2 \in xs
R x1 x2 R x2 x1.

Relation R is antisymmetric over list xs, iff for any x1 x2 \in xs, R x1 x2 and R x2 x1 imply that x1 = x2.
Definition antisymmetric_over_list :=
x1 x2,
x1 \in xs
x2 \in xs
R x1 x2
R x2 x1
x1 = x2.

End Order.