# Library prosa.util.supremum

From mathcomp Require Import ssreflect ssrbool eqtype seq.

# Computation of a Sequence's Supremum

This module provides a simple function supremum for the computation of a maximal element of a sequence, according to any given relation R. If the relation R is reflexive, total, and transitive, the result of supremum is indeed the supremum of the set of items in the sequence.
Section SelectSupremum.
Consider any type of elements with decidable equality...
Context {T : eqType}.
...and any given relation R.
Variable R : rel T.
We first define a help function choose_superior that, given an element x and maybe a second element y, picks x if R x y holds, and y otherwise.
Definition choose_superior (x : T) (maybe_y : option T) : option T :=
match maybe_y with
| Some y ⇒ if R x y then Some x else Some y
| None ⇒ Some x
end.
The supremum of a given sequence s can then be computed by simply folding s with choose_superior.
Definition supremum (s : seq T) : option T := foldr choose_superior None s.
Next, we establish that supremum satisfies its specification. To this end, we first establish a few simple helper lemmas.
We start with observing how supremum can be unrolled one step.
Lemma supremum_unfold :
∀ head tail,
supremum (head :: tail) = choose_superior head (supremum tail).
Next, we observe that supremum returns a result for any non-empty list.
Lemma supremum_exists : ∀ x s, x \in s → supremum s != None.
Conversely, if supremum finds nothing, then the list is empty.
Lemma supremum_none : ∀ s, supremum s = None → s = nil.
Next, we observe that the value found by supremum comes indeed from the list that it was given.
Lemma supremum_in :
∀ x s,
supremum s = Some x →
x \in s.
To prove that supremum indeed computes the given sequence's supremum, we need to make additional assumptions on R.
(1) R is reflexive.
Hypothesis H_R_reflexive : reflexive R.
(2) R is total.
Hypothesis H_R_total : total R.
(3) R is transitive.
Hypothesis H_R_transitive : transitive R.
Based on these assumptions, we show that the function supremum indeed computes an upper bound on all elements in the given sequence.
Lemma supremum_spec :
∀ x s,
supremum s = Some x →
∀ y,
y \in s → R x y.
End SelectSupremum.