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 \in xs, either R or R holds.
  Definition total_over_list :=
    ∀ x1 x2,
       \in xs →
       \in xs →
      R ∨ R .

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

End Order.