Library prosa.util.supremum


(* ----------------------------------[ coqtop ]---------------------------------

Welcome to Coq 8.11.2 (June 2020)

----------------------------------------------------------------------------- *)


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 yif R x y then Some x else Some y
    | NoneSome 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).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 21)
  
  T : eqType
  R : rel T
  ============================
  forall (head : T) (tail : seq T),
  supremum (head :: tail) = choose_superior head (supremum tail)

----------------------------------------------------------------------------- *)


  Proof.
    movehead tail.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 23)
  
  T : eqType
  R : rel T
  head : T
  tail : seq T
  ============================
  supremum (head :: tail) = choose_superior head (supremum tail)

----------------------------------------------------------------------------- *)


    by rewrite [LHS]/supremum /foldr -/(foldr choose_superior None tail) -/(supremum tail).

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


  Qed.

Next, we observe that [supremum] returns a result for any non-empty list.
  Lemma supremum_exists: x s, x \in s supremum s != None.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 36)
  
  T : eqType
  R : rel T
  ============================
  forall (x : T) (s : seq_predType T), x \in s -> supremum s != None

----------------------------------------------------------------------------- *)


  Proof.
    movex s IN.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 39)
  
  T : eqType
  R : rel T
  x : T
  s : seq_predType T
  IN : x \in s
  ============================
  supremum s != None

----------------------------------------------------------------------------- *)


    elim: s IN; first by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 52)
  
  T : eqType
  R : rel T
  x : T
  ============================
  forall (a : T) (l : seq T),
  (x \in l -> supremum l != None) ->
  x \in a :: l -> supremum (a :: l) != None

----------------------------------------------------------------------------- *)


    movea l _ _.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 58)
  
  T : eqType
  R : rel T
  x, a : T
  l : seq T
  ============================
  supremum (a :: l) != None

----------------------------------------------------------------------------- *)


    rewrite supremum_unfold.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 62)
  
  T : eqType
  R : rel T
  x, a : T
  l : seq T
  ============================
  choose_superior a (supremum l) != None

----------------------------------------------------------------------------- *)


    destruct (supremum l); rewrite /choose_superior //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 72)
  
  T : eqType
  R : rel T
  x, a : T
  l : seq T
  s : T
  ============================
  (if R a s then Some a else Some s) != None

----------------------------------------------------------------------------- *)


    by destruct (R a s).

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


  Qed.

Conversely, if [supremum] finds nothing, then the list is empty.
  Lemma supremum_none: s, supremum s = None s = nil.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 44)
  
  T : eqType
  R : rel T
  ============================
  forall s : seq T, supremum s = None -> s = [::]

----------------------------------------------------------------------------- *)


  Proof.
    moves.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 45)
  
  T : eqType
  R : rel T
  s : seq T
  ============================
  supremum s = None -> s = [::]

----------------------------------------------------------------------------- *)


    elim: s; first by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 55)
  
  T : eqType
  R : rel T
  ============================
  forall (a : T) (l : seq T),
  (supremum l = None -> l = [::]) ->
  supremum (a :: l) = None -> a :: l = [::]

----------------------------------------------------------------------------- *)


    movea l IH.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 59)
  
  T : eqType
  R : rel T
  a : T
  l : seq T
  IH : supremum l = None -> l = [::]
  ============================
  supremum (a :: l) = None -> a :: l = [::]

----------------------------------------------------------------------------- *)


    rewrite supremum_unfold /choose_superior.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 64)
  
  T : eqType
  R : rel T
  a : T
  l : seq T
  IH : supremum l = None -> l = [::]
  ============================
  match supremum l with
  | Some y => if R a y then Some a else Some y
  | None => Some a
  end = None -> a :: l = [::]

----------------------------------------------------------------------------- *)


    by destruct (supremum l); try destruct (R a s).

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


  Qed.

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.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 55)
  
  T : eqType
  R : rel T
  ============================
  forall (x : T) (s : seq T), supremum s = Some x -> x \in s

----------------------------------------------------------------------------- *)


  Proof.
    movex.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 56)
  
  T : eqType
  R : rel T
  x : T
  ============================
  forall s : seq T, supremum s = Some x -> x \in s

----------------------------------------------------------------------------- *)


    elim ⇒ // a l IN_TAIL IN.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 125)
  
  T : eqType
  R : rel T
  x, a : T
  l : seq T
  IN_TAIL : supremum l = Some x -> x \in l
  IN : supremum (a :: l) = Some x
  ============================
  x \in a :: l

----------------------------------------------------------------------------- *)


    rewrite in_cons; apply /orP.

(* ----------------------------------[ coqtop ]---------------------------------

1 focused subgoal
(shelved: 1) (ID 155)
  
  T : eqType
  R : rel T
  x, a : T
  l : seq T
  IN_TAIL : supremum l = Some x -> x \in l
  IN : supremum (a :: l) = Some x
  ============================
  x == a \/ x \in l

----------------------------------------------------------------------------- *)


    move: IN; rewrite supremum_unfold.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 161)
  
  T : eqType
  R : rel T
  x, a : T
  l : seq T
  IN_TAIL : supremum l = Some x -> x \in l
  ============================
  choose_superior a (supremum l) = Some x -> x == a \/ x \in l

----------------------------------------------------------------------------- *)


    destruct (supremum l); rewrite /choose_superior.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 176)
  
  T : eqType
  R : rel T
  x, a : T
  l : seq T
  s : T
  IN_TAIL : Some s = Some x -> x \in l
  ============================
  (if R a s then Some a else Some s) = Some x -> x == a \/ x \in l

subgoal 2 (ID 177) is:
 Some a = Some x -> x == a \/ x \in l

----------------------------------------------------------------------------- *)


    {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 176)
  
  T : eqType
  R : rel T
  x, a : T
  l : seq T
  s : T
  IN_TAIL : Some s = Some x -> x \in l
  ============================
  (if R a s then Some a else Some s) = Some x -> x == a \/ x \in l

----------------------------------------------------------------------------- *)


elim: (R a s) ⇒ EQ.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 185)
  
  T : eqType
  R : rel T
  x, a : T
  l : seq T
  s : T
  IN_TAIL : Some s = Some x -> x \in l
  EQ : Some a = Some x
  ============================
  x == a \/ x \in l

subgoal 2 (ID 186) is:
 x == a \/ x \in l

----------------------------------------------------------------------------- *)


      - left; apply /eqP.

(* ----------------------------------[ coqtop ]---------------------------------

2 focused subgoals
(shelved: 1) (ID 216)
  
  T : eqType
  R : rel T
  x, a : T
  l : seq T
  s : T
  IN_TAIL : Some s = Some x -> x \in l
  EQ : Some a = Some x
  ============================
  x = a

subgoal 2 (ID 186) is:
 x == a \/ x \in l

----------------------------------------------------------------------------- *)


        by injection EQ.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 186)
  
  T : eqType
  R : rel T
  x, a : T
  l : seq T
  s : T
  IN_TAIL : Some s = Some x -> x \in l
  EQ : Some s = Some x
  ============================
  x == a \/ x \in l

----------------------------------------------------------------------------- *)


      - right; by apply IN_TAIL.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 177)

subgoal 1 (ID 177) is:
 Some a = Some x -> x == a \/ x \in l

----------------------------------------------------------------------------- *)


}

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 177)
  
  T : eqType
  R : rel T
  x, a : T
  l : seq T
  IN_TAIL : None = Some x -> x \in l
  ============================
  Some a = Some x -> x == a \/ x \in l

----------------------------------------------------------------------------- *)


    {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 177)
  
  T : eqType
  R : rel T
  x, a : T
  l : seq T
  IN_TAIL : None = Some x -> x \in l
  ============================
  Some a = Some x -> x == a \/ x \in l

----------------------------------------------------------------------------- *)


left.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 245)
  
  T : eqType
  R : rel T
  x, a : T
  l : seq T
  IN_TAIL : None = Some x -> x \in l
  IN : Some a = Some x
  ============================
  x == a

----------------------------------------------------------------------------- *)


apply /eqP.

(* ----------------------------------[ coqtop ]---------------------------------

1 focused subgoal
(shelved: 1) (ID 273)
  
  T : eqType
  R : rel T
  x, a : T
  l : seq T
  IN_TAIL : None = Some x -> x \in l
  IN : Some a = Some x
  ============================
  x = a

----------------------------------------------------------------------------- *)


      by injection IN.
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


}

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


  Qed.

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.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 71)
  
  T : eqType
  R : rel T
  H_R_reflexive : reflexive (T:=T) R
  H_R_total : total (T:=T) R
  H_R_transitive : transitive (T:=T) R
  ============================
  forall (x : T) (s : seq T),
  supremum s = Some x -> forall y : T, y \in s -> R x y

----------------------------------------------------------------------------- *)


  Proof.
    movex s SOME_x.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 74)
  
  T : eqType
  R : rel T
  H_R_reflexive : reflexive (T:=T) R
  H_R_total : total (T:=T) R
  H_R_transitive : transitive (T:=T) R
  x : T
  s : seq T
  SOME_x : supremum s = Some x
  ============================
  forall y : T, y \in s -> R x y

----------------------------------------------------------------------------- *)


    move: x SOME_x (supremum_in _ _ SOME_x).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 83)
  
  T : eqType
  R : rel T
  H_R_reflexive : reflexive (T:=T) R
  H_R_total : total (T:=T) R
  H_R_transitive : transitive (T:=T) R
  s : seq T
  ============================
  forall x : T,
  supremum s = Some x -> x \in s -> forall y : T, y \in s -> R x y

----------------------------------------------------------------------------- *)


    elim: s; first by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 93)
  
  T : eqType
  R : rel T
  H_R_reflexive : reflexive (T:=T) R
  H_R_total : total (T:=T) R
  H_R_transitive : transitive (T:=T) R
  ============================
  forall (a : T) (l : seq T),
  (forall x : T,
   supremum l = Some x -> x \in l -> forall y : T, y \in l -> R x y) ->
  forall x : T,
  supremum (a :: l) = Some x ->
  x \in a :: l -> forall y : T, y \in a :: l -> R x y

----------------------------------------------------------------------------- *)


    moves1 sn IH z SOME_z IN_z_s y.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 132)
  
  T : eqType
  R : rel T
  H_R_reflexive : reflexive (T:=T) R
  H_R_total : total (T:=T) R
  H_R_transitive : transitive (T:=T) R
  s1 : T
  sn : seq T
  IH : forall x : T,
       supremum sn = Some x -> x \in sn -> forall y : T, y \in sn -> R x y
  z : T
  SOME_z : supremum (s1 :: sn) = Some z
  IN_z_s : z \in s1 :: sn
  y : T
  ============================
  y \in s1 :: sn -> R z y

----------------------------------------------------------------------------- *)


    move: SOME_z.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 134)
  
  T : eqType
  R : rel T
  H_R_reflexive : reflexive (T:=T) R
  H_R_total : total (T:=T) R
  H_R_transitive : transitive (T:=T) R
  s1 : T
  sn : seq T
  IH : forall x : T,
       supremum sn = Some x -> x \in sn -> forall y : T, y \in sn -> R x y
  z : T
  IN_z_s : z \in s1 :: sn
  y : T
  ============================
  supremum (s1 :: sn) = Some z -> y \in s1 :: sn -> R z y

----------------------------------------------------------------------------- *)


rewrite supremum_unfold /choose_superiorSOME_z.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 140)
  
  T : eqType
  R : rel T
  H_R_reflexive : reflexive (T:=T) R
  H_R_total : total (T:=T) R
  H_R_transitive : transitive (T:=T) R
  s1 : T
  sn : seq T
  IH : forall x : T,
       supremum sn = Some x -> x \in sn -> forall y : T, y \in sn -> R x y
  z : T
  IN_z_s : z \in s1 :: sn
  y : T
  SOME_z : match supremum sn with
           | Some y => if R s1 y then Some s1 else Some y
           | None => Some s1
           end = Some z
  ============================
  y \in s1 :: sn -> R z y

----------------------------------------------------------------------------- *)


    destruct (supremum sn) as [b|] eqn:SUPR; last first.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 173)
  
  T : eqType
  R : rel T
  H_R_reflexive : reflexive (T:=T) R
  H_R_total : total (T:=T) R
  H_R_transitive : transitive (T:=T) R
  s1 : T
  sn : seq T
  SUPR : supremum sn = None
  IH : forall x : T,
       None = Some x -> x \in sn -> forall y : T, y \in sn -> R x y
  z : T
  IN_z_s : z \in s1 :: sn
  y : T
  SOME_z : Some s1 = Some z
  ============================
  y \in s1 :: sn -> R z y

subgoal 2 (ID 168) is:
 y \in s1 :: sn -> R z y

----------------------------------------------------------------------------- *)


    {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 173)
  
  T : eqType
  R : rel T
  H_R_reflexive : reflexive (T:=T) R
  H_R_total : total (T:=T) R
  H_R_transitive : transitive (T:=T) R
  s1 : T
  sn : seq T
  SUPR : supremum sn = None
  IH : forall x : T,
       None = Some x -> x \in sn -> forall y : T, y \in sn -> R x y
  z : T
  IN_z_s : z \in s1 :: sn
  y : T
  SOME_z : Some s1 = Some z
  ============================
  y \in s1 :: sn -> R z y

----------------------------------------------------------------------------- *)


apply supremum_none in SUPR; subst.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 183)
  
  T : eqType
  R : rel T
  H_R_reflexive : reflexive (T:=T) R
  H_R_total : total (T:=T) R
  H_R_transitive : transitive (T:=T) R
  s1 : T
  IH : forall x : T,
       None = Some x -> x \in [::] -> forall y : T, y \in [::] -> R x y
  z : T
  IN_z_s : z \in [:: s1]
  y : T
  SOME_z : Some s1 = Some z
  ============================
  y \in [:: s1] -> R z y

----------------------------------------------------------------------------- *)


      rewrite mem_seq1 ⇒ /eqP →.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 226)
  
  T : eqType
  R : rel T
  H_R_reflexive : reflexive (T:=T) R
  H_R_total : total (T:=T) R
  H_R_transitive : transitive (T:=T) R
  s1 : T
  IH : forall x : T,
       None = Some x -> x \in [::] -> forall y : T, y \in [::] -> R x y
  z : T
  IN_z_s : z \in [:: s1]
  y : T
  SOME_z : Some s1 = Some z
  ============================
  R z s1

----------------------------------------------------------------------------- *)


      by injection SOME_z ⇒ →.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 168)

subgoal 1 (ID 168) is:
 y \in s1 :: sn -> R z y

----------------------------------------------------------------------------- *)


}

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 168)
  
  T : eqType
  R : rel T
  H_R_reflexive : reflexive (T:=T) R
  H_R_total : total (T:=T) R
  H_R_transitive : transitive (T:=T) R
  s1 : T
  sn : seq T
  b : T
  SUPR : supremum sn = Some b
  IH : forall x : T,
       Some b = Some x -> x \in sn -> forall y : T, y \in sn -> R x y
  z : T
  IN_z_s : z \in s1 :: sn
  y : T
  SOME_z : (if R s1 b then Some s1 else Some b) = Some z
  ============================
  y \in s1 :: sn -> R z y

----------------------------------------------------------------------------- *)


    {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 168)
  
  T : eqType
  R : rel T
  H_R_reflexive : reflexive (T:=T) R
  H_R_total : total (T:=T) R
  H_R_transitive : transitive (T:=T) R
  s1 : T
  sn : seq T
  b : T
  SUPR : supremum sn = Some b
  IH : forall x : T,
       Some b = Some x -> x \in sn -> forall y : T, y \in sn -> R x y
  z : T
  IN_z_s : z \in s1 :: sn
  y : T
  SOME_z : (if R s1 b then Some s1 else Some b) = Some z
  ============================
  y \in s1 :: sn -> R z y

----------------------------------------------------------------------------- *)


rewrite in_cons ⇒ /orP [/eqP EQy | INy]; last first.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 314)
  
  T : eqType
  R : rel T
  H_R_reflexive : reflexive (T:=T) R
  H_R_total : total (T:=T) R
  H_R_transitive : transitive (T:=T) R
  s1 : T
  sn : seq T
  b : T
  SUPR : supremum sn = Some b
  IH : forall x : T,
       Some b = Some x -> x \in sn -> forall y : T, y \in sn -> R x y
  z : T
  IN_z_s : z \in s1 :: sn
  y : T
  SOME_z : (if R s1 b then Some s1 else Some b) = Some z
  INy : y \in sn
  ============================
  R z y

subgoal 2 (ID 313) is:
 R z y

----------------------------------------------------------------------------- *)


      - have R_by: R b y
          by apply IH ⇒ //; apply supremum_in.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 343)
  
  T : eqType
  R : rel T
  H_R_reflexive : reflexive (T:=T) R
  H_R_total : total (T:=T) R
  H_R_transitive : transitive (T:=T) R
  s1 : T
  sn : seq T
  b : T
  SUPR : supremum sn = Some b
  IH : forall x : T,
       Some b = Some x -> x \in sn -> forall y : T, y \in sn -> R x y
  z : T
  IN_z_s : z \in s1 :: sn
  y : T
  SOME_z : (if R s1 b then Some s1 else Some b) = Some z
  INy : y \in sn
  R_by : R b y
  ============================
  R z y

subgoal 2 (ID 313) is:
 R z y

----------------------------------------------------------------------------- *)


        apply H_R_transitive with (y := b) ⇒ //.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 344)
  
  T : eqType
  R : rel T
  H_R_reflexive : reflexive (T:=T) R
  H_R_total : total (T:=T) R
  H_R_transitive : transitive (T:=T) R
  s1 : T
  sn : seq T
  b : T
  SUPR : supremum sn = Some b
  IH : forall x : T,
       Some b = Some x -> x \in sn -> forall y : T, y \in sn -> R x y
  z : T
  IN_z_s : z \in s1 :: sn
  y : T
  SOME_z : (if R s1 b then Some s1 else Some b) = Some z
  INy : y \in sn
  R_by : R b y
  ============================
  R z b

subgoal 2 (ID 313) is:
 R z y

----------------------------------------------------------------------------- *)


        destruct (R s1 b) eqn:R_s1b;
          by injection SOME_z ⇒ <-.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 313)
  
  T : eqType
  R : rel T
  H_R_reflexive : reflexive (T:=T) R
  H_R_total : total (T:=T) R
  H_R_transitive : transitive (T:=T) R
  s1 : T
  sn : seq T
  b : T
  SUPR : supremum sn = Some b
  IH : forall x : T,
       Some b = Some x -> x \in sn -> forall y : T, y \in sn -> R x y
  z : T
  IN_z_s : z \in s1 :: sn
  y : T
  SOME_z : (if R s1 b then Some s1 else Some b) = Some z
  EQy : y = s1
  ============================
  R z y

----------------------------------------------------------------------------- *)


      - move: IN_z_s; rewrite in_cons ⇒ /orP [/eqP EQz | INz];
          first by subst.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 488)
  
  T : eqType
  R : rel T
  H_R_reflexive : reflexive (T:=T) R
  H_R_total : total (T:=T) R
  H_R_transitive : transitive (T:=T) R
  s1 : T
  sn : seq T
  b : T
  SUPR : supremum sn = Some b
  IH : forall x : T,
       Some b = Some x -> x \in sn -> forall y : T, y \in sn -> R x y
  z, y : T
  SOME_z : (if R s1 b then Some s1 else Some b) = Some z
  EQy : y = s1
  INz : z \in sn
  ============================
  R z y

----------------------------------------------------------------------------- *)


        move: (H_R_total s1 b) ⇒ /orP [R_s1b|R_bs1].

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 540)
  
  T : eqType
  R : rel T
  H_R_reflexive : reflexive (T:=T) R
  H_R_total : total (T:=T) R
  H_R_transitive : transitive (T:=T) R
  s1 : T
  sn : seq T
  b : T
  SUPR : supremum sn = Some b
  IH : forall x : T,
       Some b = Some x -> x \in sn -> forall y : T, y \in sn -> R x y
  z, y : T
  SOME_z : (if R s1 b then Some s1 else Some b) = Some z
  EQy : y = s1
  INz : z \in sn
  R_s1b : R s1 b
  ============================
  R z y

subgoal 2 (ID 541) is:
 R z y

----------------------------------------------------------------------------- *)


        + move: SOME_z.
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 543)
  
  T : eqType
  R : rel T
  H_R_reflexive : reflexive (T:=T) R
  H_R_total : total (T:=T) R
  H_R_transitive : transitive (T:=T) R
  s1 : T
  sn : seq T
  b : T
  SUPR : supremum sn = Some b
  IH : forall x : T,
       Some b = Some x -> x \in sn -> forall y : T, y \in sn -> R x y
  z, y : T
  EQy : y = s1
  INz : z \in sn
  R_s1b : R s1 b
  ============================
  (if R s1 b then Some s1 else Some b) = Some z -> R z y

subgoal 2 (ID 541) is:
 R z y

----------------------------------------------------------------------------- *)


rewrite R_s1bSOME_z.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 546)
  
  T : eqType
  R : rel T
  H_R_reflexive : reflexive (T:=T) R
  H_R_total : total (T:=T) R
  H_R_transitive : transitive (T:=T) R
  s1 : T
  sn : seq T
  b : T
  SUPR : supremum sn = Some b
  IH : forall x : T,
       Some b = Some x -> x \in sn -> forall y : T, y \in sn -> R x y
  z, y : T
  EQy : y = s1
  INz : z \in sn
  R_s1b : R s1 b
  SOME_z : Some s1 = Some z
  ============================
  R z y

subgoal 2 (ID 541) is:
 R z y

----------------------------------------------------------------------------- *)


          by injection SOME_zEQ; subst.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 541)
  
  T : eqType
  R : rel T
  H_R_reflexive : reflexive (T:=T) R
  H_R_total : total (T:=T) R
  H_R_transitive : transitive (T:=T) R
  s1 : T
  sn : seq T
  b : T
  SUPR : supremum sn = Some b
  IH : forall x : T,
       Some b = Some x -> x \in sn -> forall y : T, y \in sn -> R x y
  z, y : T
  SOME_z : (if R s1 b then Some s1 else Some b) = Some z
  EQy : y = s1
  INz : z \in sn
  R_bs1 : R b s1
  ============================
  R z y

----------------------------------------------------------------------------- *)


        + by destruct (R s1 b); injection SOME_zEQ; subst.
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


}

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


  Qed.

End SelectSupremum.