Built with Alectryon, running Coq+SerAPI v8.20.0+0.20.0. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
Serlib plugin: coq-elpi.elpi is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted.
[Loading ML file coq-elpi.elpi ... done]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]


(** 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 :=
    forall 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 :=
    forall 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 :=
    forall x1 x2,
      x1 \in xs ->
      x2 \in xs ->
      R x1 x2 ->
      R x2 x1 ->
      x1 = x2.

End Order.