# Library prosa.util.supremum

# Computation of a Sequence's Supremum

Consider any type of elements with decidable equality...

...and any given relation R.

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.

match maybe_y with

| Some y ⇒ if R x y then Some x else Some y

| None ⇒ Some x

end.

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.

Next, we observe that supremum returns a result for any non-empty
list.

Conversely, if supremum finds nothing, then the list is empty.

Next, we observe that the value found by supremum comes indeed from the
list that it was given.

To prove that supremum indeed computes the given sequence's supremum,
we need to make additional assumptions on R.
(1) R is reflexive.

(2) R is total.

(3) R is transitive.

Based on these assumptions, we show that the function supremum indeed
computes an upper bound on all elements in the given sequence.