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.