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
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.
The supremum of a given sequence [s] can then be computed by simply
folding [s] with [choose_superior].
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.
move⇒ head 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.
∀ 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.
move⇒ head 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.
move⇒ x 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
----------------------------------------------------------------------------- *)
move⇒ a 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 36)
T : eqType
R : rel T
============================
forall (x : T) (s : seq_predType T), x \in s -> supremum s != None
----------------------------------------------------------------------------- *)
Proof.
move⇒ x 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
----------------------------------------------------------------------------- *)
move⇒ a 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.
move⇒ s.
(* ----------------------------------[ 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 = [::]
----------------------------------------------------------------------------- *)
move ⇒ a 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 44)
T : eqType
R : rel T
============================
forall s : seq T, supremum s = None -> s = [::]
----------------------------------------------------------------------------- *)
Proof.
move⇒ s.
(* ----------------------------------[ 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 = [::]
----------------------------------------------------------------------------- *)
move ⇒ a 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.
move⇒ x.
(* ----------------------------------[ 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.
∀ 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.
move⇒ x.
(* ----------------------------------[ 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.
(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.
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.
move⇒ x 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
----------------------------------------------------------------------------- *)
move⇒ s1 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_superior ⇒ SOME_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_s1b ⇒ SOME_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_z ⇒ EQ; 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_z ⇒ EQ; subst.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End SelectSupremum.
∀ 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.
move⇒ x 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
----------------------------------------------------------------------------- *)
move⇒ s1 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_superior ⇒ SOME_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_s1b ⇒ SOME_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_z ⇒ EQ; 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_z ⇒ EQ; subst.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End SelectSupremum.