Library prosa.util.rel

From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq.

(* In this section, we define some properties of relations
   that are important for fixed-point iterations. *)

Section Relations.

  Context {T: Type}.
  Variable R: rel T.
  Variable f: T T.

  Definition monotone (R: rel T) :=
     x y, R x y R (f x) (f y).

End Relations.

Section Order.

  Context {T: eqType}.
  Variable rel: T T bool.
  Variable l: seq T.

  Definition total_over_list :=
     x1 x2,
      x1 \in l
      x2 \in l
      (rel x1 x2 rel x2 x1).

  Definition antisymmetric_over_list :=
     x1 x2,
      x1 \in l
      x2 \in l
      rel x1 x2
      rel x2 x1
      x1 = x2.

End Order.