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]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
(** Additional lemmas about [BigMax]. *)SectionExtraLemmas.(** Given a function [F], a predicate [P], and a sequence [xs], we show that [F x <= max { F i | ∀ i ∈ xs, P i}] for any [x] in [xs]. *)
forall (X : eqType) (F : X -> nat) (P : pred X)
(xs : seq X) (x : X),
x \in xs -> P x -> F x <= \max_(i <- xs | P i) F i
forall (X : eqType) (F : X -> nat) (P : pred X)
(xs : seq X) (x : X),
x \in xs -> P x -> F x <= \max_(i <- xs | P i) F i
bymove=> X F P xs x IN Px; rewrite (big_rem x) //= Px leq_maxl.Qed.(** Similarly, we show that for a constant [n] to be bounded by [max { F i | ∀ i ∈ xs, P i}], it is sufficient to find an element [x ∈ xs] such that [P x] and [n <= F x]. *)
forall (X : eqType) (P : pred X) (F : X -> nat)
(xs : seq X) (n : nat),
(existsx : X, x \in xs /\ P x /\ n <= F x) ->
n <= \max_(x <- xs | P x) F x
forall (X : eqType) (P : pred X) (F : X -> nat)
(xs : seq X) (n : nat),
(existsx : X, x \in xs /\ P x /\ n <= F x) ->
n <= \max_(x <- xs | P x) F x
X: eqType P: pred X F: X -> nat xs: seq X n: nat x: X IN: x \in xs Px: P x LE: n <= F x
n <= \max_(x <- xs | P x) F x
X: eqType P: pred X F: X -> nat xs: seq X n: nat x: X IN: x \in xs Px: P x LE: n <= F x
F x <= \max_(x <- xs | P x) F x
byapply leq_bigmax_cond_seq.Qed.(** Next, we show that the fact [max { F i | ∀ i ∈ xs, P i} <= m] for some [m] is equivalent to the fact that [∀ x ∈ xs, P x -> F x <= m]. *)
forall (X : eqType) (F : X -> nat) (P : pred X)
(xs : seq X) (m : nat),
reflect (forallx : X, x \in xs -> P x -> F x <= m)
(\max_(x <- xs | P x) F x <= m)
forall (X : eqType) (F : X -> nat) (P : pred X)
(xs : seq X) (m : nat),
reflect (forallx : X, x \in xs -> P x -> F x <= m)
(\max_(x <- xs | P x) F x <= m)
X: eqType F: X -> nat P: pred X xs: seq X m: nat
reflect (forallx : X, x \in xs -> P x -> F x <= m)
(\max_(x <- xs | P x) F x <= m)
X: eqType F: X -> nat P: pred X xs: seq X m: nat leFm: \max_(x <- xs | P x) F x <= m i: X IINR: i \in xs Pi: P i
F i <= m
X: eqType F: X -> nat P: pred X xs: seq X m: nat leFm: forallx : X, x \in xs -> P x -> F x <= m
\max_(x <- xs | P x) F x <= m
X: eqType F: X -> nat P: pred X xs: seq X m: nat leFm: \max_(x <- xs | P x) F x <= m i: X IINR: i \in xs Pi: P i
X: eqType F: X -> nat P: pred X xs: seq X m: nat leFm: forallx : X, x \in xs -> P x -> F x <= m
\max_(x <- xs | P x) F x <= m
X: eqType F: X -> nat P: pred X xs: seq X m: nat leFm: forallx : X, x \in xs -> P x -> F x <= m m1, m2: nat
m1 <= m -> m2 <= m -> maxn m1 m2 <= m
X: eqType F: X -> nat P: pred X xs: seq X m: nat leFm: forallx : X, x \in xs -> P x -> F x <= m m1: X m2: (m1 \in xs) && P m1
F m1 <= m
X: eqType F: X -> nat P: pred X xs: seq X m: nat leFm: forallx : X, x \in xs -> P x -> F x <= m m1, m2: nat
m1 <= m -> m2 <= m -> maxn m1 m2 <= m
byintros; rewrite geq_max; apply/andP; split.
X: eqType F: X -> nat P: pred X xs: seq X m: nat leFm: forallx : X, x \in xs -> P x -> F x <= m m1: X m2: (m1 \in xs) && P m1
F m1 <= m
bymove: m2 => /andP [M1IN Pm1]; apply: leFm.Qed.(** Given two functions [F1] and [F2], a predicate [P], and sequence [xs], we show that if [F1 x <= F2 x] for any [x \in xs] such that [P x], then [max] of [{F1 x | ∀ x ∈ xs, P x}] is bounded by the [max] of [{F2 x | ∀ x ∈ xs, P x}]. *)
forall (X : eqType) (F1F2 : X -> nat) (P : pred X)
(xs : seq X),
(forallx : X, x \in xs -> P x -> F1 x <= F2 x) ->
\max_(x <- xs | P x) F1 x <= \max_(x <- xs | P x) F2 x
forall (X : eqType) (F1F2 : X -> nat) (P : pred X)
(xs : seq X),
(forallx : X, x \in xs -> P x -> F1 x <= F2 x) ->
\max_(x <- xs | P x) F1 x <= \max_(x <- xs | P x) F2 x
X: eqType F1, F2: X -> nat P: pred X xs: seq X ALL: forallx : X, x \in xs -> P x -> F1 x <= F2 x x: X IN: x \in xs Px: P x
F1 x <= \max_(x <- xs | P x) F2 x
X: eqType F1, F2: X -> nat P: pred X xs: seq X x: X ALL: F1 x <= F2 x IN: x \in xs Px: P x
F1 x <= \max_(x <- xs | P x) F2 x
X: eqType F1, F2: X -> nat P: pred X xs: seq X x: X ALL: F1 x <= F2 x IN: x \in xs Px: P x
F1 x <=
maxn (F2 x) (\max_(y <- rem (T:=X) x xs | P y) F2 y)
byapply leq_trans with (F2 x); [ | rewrite leq_maxl].Qed.(** We show that for a positive [n], [max] of [{0, …, n-1}] is smaller than [n]. *)
foralln : nat, 0 < n -> \max_(i < n) i < n
foralln : nat, 0 < n -> \max_(i < n) i < n
n: nat POS: 0 < n.+1
\max_(i < n.+1) i < n.+1
n: nat
\max_(i < n.+1) i < n.+1
n: nat IHn: \max_(i < n.+1) i < n.+1
\max_(i < n.+2) i < n.+2
byrewrite big_ord_recr /= /maxn IHn.Qed.(** We state the next lemma in terms of _ordinals_. Given a natural number [n], a predicate [P], and an ordinal [i0 ∈ {0, …, n-1}] satisfying [P], we show that [max {i | P i} < n]. Note that the element satisfying [P] is needed to prove that [{i | P i}] is not empty. *)
forall (n : nat) (P : pred nat) (i0 : 'I_n),
P i0 -> \max_(i < n | P i) i < n
forall (n : nat) (P : pred nat) (i0 : 'I_n),
P i0 -> \max_(i < n | P i) i < n
n: nat P: pred nat i0: 'I_n Pi: P i0
\max_(i < n | P i) i < n
n: nat P: pred nat i0: 'I_n.+1 Pi: P i0
\max_(i < n.+1 | P i) i < n.+1
n: nat P: pred nat i0: 'I_n.+1 Pi: P i0
\big[ssrnat_maxn__canonical__Monoid_Law/0]_i
(if P i then i else0) < n.+1
n: nat P: pred nat i0: 'I_n.+1 Pi: P i0
\big[ssrnat_maxn__canonical__Monoid_Law/0]_i
(if P i then i else0) <= \max_(i < n.+1) i
n: nat P: pred nat i0: 'I_n.+1 Pi: P i0
\max_(i < n.+1) i < n.+1
n: nat P: pred nat i0: 'I_n.+1 Pi: P i0
\big[ssrnat_maxn__canonical__Monoid_Law/0]_i
(if P i then i else0) <= \max_(i < n.+1) i
n: nat P: pred nat i0: 'I_n.+1 Pi: P i0 i: fintype_ordinal__canonical__fintype_Finite n.+1
(if P i then i else0) <= \max_(i < n.+1) i
n: nat P: pred nat i0: 'I_n.+1 Pi: P i0 i: fintype_ordinal__canonical__fintype_Finite n.+1
i <= \max_(i < n.+1) i
byapply leq_bigmax_cond.
n: nat P: pred nat i0: 'I_n.+1 Pi: P i0
\max_(i < n.+1) i < n.+1
byapply bigmax_ord_ltn_identity.Qed.(** Next, we show that, given a natural number [n], a predicate [P], and an ordinal [i0 ∈ {0, …, n-1}] satisfying [P], [max {i | P i} < n] also satisfies [P]. *)
forall (n : nat) (P : pred nat) (i0 : 'I_n),
P i0 -> P (\max_(i < n | P i) i)
forall (n : nat) (P : pred nat) (i0 : 'I_n),
P i0 -> P (\max_(i < n | P i) i)
n: nat P: pred nat i0: 'I_n Pi0: P i0
P (\max_(i < n | P i) i)
P: pred nat i0: 'I_0 Pi0: P i0
P (\max_(i < 0 | P i) i)
P: pred nat n: nat IHn: foralli0 : 'I_n, P i0 -> P (\max_(i < n | P i) i) i0: 'I_n.+1 Pi0: P i0
P (\max_(i < n.+1 | P i) i)
P: pred nat i0: 'I_0 Pi0: P i0
P (\max_(i < 0 | P i) i)
bydestruct i0 as [i0 P0]; move: (P0) => P1; rewrite ltn0 in P1.
P: pred nat n: nat IHn: foralli0 : 'I_n, P i0 -> P (\max_(i < n | P i) i) i0: 'I_n.+1 Pi0: P i0
P (\max_(i < n.+1 | P i) i)
P: pred nat n: nat IHn: foralli0 : 'I_n, P i0 -> P (\max_(i < n | P i) i) i0: 'I_n.+1 Pi0: P i0
P (\max_(i < n.+1 | P i) i)
P: pred nat n: nat IHn: foralli0 : 'I_n, P i0 -> P (\max_(i < n | P i) i) i0: 'I_n.+1 Pi0: P i0
P
(maxn (\max_(i < n) (if P i then i else0))
(if P n then n else0))
P: pred nat n: nat IHn: foralli0 : 'I_n, P i0 -> P (\max_(i < n | P i) i) i0: 'I_n.+1 Pi0: P i0 Pn: P n = true
P (maxn (\max_(i < n) (if P i then i else0)) n)
P: pred nat n: nat IHn: foralli0 : 'I_n, P i0 -> P (\max_(i < n | P i) i) i0: 'I_n.+1 Pi0: P i0 Pn: P n = false
P (maxn (\max_(i < n) (if P i then i else0)) 0)
P: pred nat n: nat IHn: foralli0 : 'I_n, P i0 -> P (\max_(i < n | P i) i) i0: 'I_n.+1 Pi0: P i0 Pn: P n = true
P (maxn (\max_(i < n) (if P i then i else0)) n)
P: pred nat n: nat IHn: foralli0 : 'I_n.+1, P i0 -> P (\max_(i < n.+1 | P i) i) i0: 'I_n.+2 Pi0: P i0 Pn: P n.+1 = true
P (maxn (\max_(i < n.+1) (if P i then i else0)) n.+1)
P: pred nat n: nat IHn: foralli0 : 'I_n.+1, P i0 -> P (\max_(i < n.+1 | P i) i) i0: 'I_n.+2 Pi0: P i0 Pn: P n.+1 = true
P
(if \max_(i < n.+1) (if P i then i else0) < n.+1then n.+1else \max_(i < n.+1) (if P i then i else0))
P: pred nat n: nat IHn: foralli0 : 'I_n.+1, P i0 -> P (\max_(i < n.+1 | P i) i) i0: 'I_n.+2 Pi0: P i0 Pn: P n.+1 = true Pi: (\max_(i < n.+1) (if P i then i else0) < n.+1) =
false
P
(if \max_(i < n.+1) (if P i then i else0) < n.+1then n.+1else \max_(i < n.+1) (if P i then i else0))
P: pred nat n: nat IHn: foralli0 : 'I_n.+1, P i0 -> P (\max_(i < n.+1 | P i) i) i0: 'I_n.+2 Pi0: P i0 Pn: P n.+1 = true Pi: (\max_(i < n.+1) (if P i then i else0) < n.+1) =
false
False
P: pred nat n: nat IHn: foralli0 : 'I_n.+1, P i0 -> P (\max_(i < n.+1 | P i) i) i0: 'I_n.+2 Pi0: P i0 Pn: P n.+1 = true
\max_(i < n.+1) (if P i then i else0) < n.+1
P: pred nat n: nat IHn: foralli0 : 'I_n.+1, P i0 -> P (\max_(i < n.+1 | P i) i) i0: 'I_n.+2 Pi0: P i0 Pn: P n.+1 = true
\max_(i < n.+1) (if P i then i else0) <=
\max_(i < n.+1) i
P: pred nat n: nat IHn: foralli0 : 'I_n.+1, P i0 -> P (\max_(i < n.+1 | P i) i) i0: 'I_n.+2 Pi0: P i0 Pn: P n.+1 = true
\max_(i < n.+1) i < n.+1
P: pred nat n: nat IHn: foralli0 : 'I_n.+1, P i0 -> P (\max_(i < n.+1 | P i) i) i0: 'I_n.+2 Pi0: P i0 Pn: P n.+1 = true
\max_(i < n.+1) (if P i then i else0) <=
\max_(i < n.+1) i
P: pred nat n: nat IHn: foralli0 : 'I_n.+1, P i0 -> P (\max_(i < n.+1 | P i) i) i0: 'I_n.+2 Pi0: P i0 Pn: P n.+1 = true i: 'I_n.+1
(if P i then i else0) <= \max_(i < n.+1) i
bydestruct (P i); firstapply leq_bigmax_cond.
P: pred nat n: nat IHn: foralli0 : 'I_n.+1, P i0 -> P (\max_(i < n.+1 | P i) i) i0: 'I_n.+2 Pi0: P i0 Pn: P n.+1 = true
\max_(i < n.+1) i < n.+1
P: pred nat n: nat IHn: foralli0 : 'I_n.+1, P i0 -> P (\max_(i < n.+1 | P i) i) i0: 'I_n.+2 Pi0: P i0 Pn: P n.+1 = true
\max_(i < n.+1) i < n.+1
byapply bigmax_ord_ltn_identity.}
P: pred nat n: nat IHn: foralli0 : 'I_n, P i0 -> P (\max_(i < n | P i) i) i0: 'I_n.+1 Pi0: P i0 Pn: P n = false
P (maxn (\max_(i < n) (if P i then i else0)) 0)
P: pred nat n: nat IHn: foralli0 : 'I_n, P i0 -> P (\max_(i < n | P i) i) i0: 'I_n.+1 Pi0: P i0 Pn: P n = false
P (maxn (\max_(i < n) (if P i then i else0)) 0)
P: pred nat n: nat IHn: foralli0 : 'I_n, P i0 -> P (\max_(i < n | P i) i) i0: 'I_n.+1 Pi0: P i0 Pn: P n = false
P (\max_(i < n | P i) i)
P: pred nat n: nat IHn: foralli0 : 'I_n, P i0 -> P (\max_(i < n | P i) i) i0: 'I_n.+1 Pi0: P i0 Pn: P n = false
i0 < n
P: pred nat n: nat IHn: foralli0 : 'I_n, P i0 -> P (\max_(i < n | P i) i) i0: 'I_n.+1 Pi0: P i0 Pn: P n = false
i0 != n
P: pred nat n: nat IHn: foralli0 : 'I_n, P i0 -> P (\max_(i < n | P i) i) i0: 'I_n.+1 Pi0: P i0 Pn: P n = false BUG: i0 = n
False
byrewrite -BUG Pi0 in Pn.}}Qed.(** Furthermore, we observe that, if there is any element that satisfies the predicate, then there exists a witness for the computed maximum. *)
T: eqType
forall (xs : seq T) (P : pred T) (F : T -> nat),
has P xs ->
existsx : T,
x \in xs /\ P x /\ F x = \max_(x0 <- xs | P x0) F x0
T: eqType
forall (xs : seq T) (P : pred T) (F : T -> nat),
has P xs ->
existsx : T,
x \in xs /\ P x /\ F x = \max_(x0 <- xs | P x0) F x0
T: eqType xs: seq T P: pred T F: T -> nat
has P xs ->
existsx : T,
x \in xs /\ P x /\ F x = \max_(x0 <- xs | P x0) F x0
T: eqType P: pred T F: T -> nat a: T xs: seq T IH: has P xs ->
existsx : T,
x \in xs /\
P x /\ F x = \max_(x0 <- xs | P x0) F x0 HAS: has P (a :: xs)
existsx : T,
x \in a :: xs /\
P x /\ F x = \max_(x0 <- (a :: xs) | P x0) F x0
T: eqType P: pred T F: T -> nat a: T xs: seq T IH: has P xs ->
existsx : T,
x \in xs /\
P x /\ F x = \max_(x0 <- xs | P x0) F x0 HAS: has P (a :: xs)
~~ P a ->
existsx : T,
x \in a :: xs /\
P x /\ F x = \max_(x0 <- (a :: xs) | P x0) F x0
T: eqType P: pred T F: T -> nat a: T xs: seq T IH: has P xs ->
existsx : T,
x \in xs /\
P x /\ F x = \max_(x0 <- xs | P x0) F x0 HAS: has P (a :: xs)
P a ->
existsx : T,
x \in a :: xs /\
P x /\ F x = \max_(x0 <- (a :: xs) | P x0) F x0
T: eqType P: pred T F: T -> nat a: T xs: seq T IH: has P xs ->
existsx : T,
x \in xs /\
P x /\ F x = \max_(x0 <- xs | P x0) F x0 HAS: has P (a :: xs)
~~ P a ->
existsx : T,
x \in a :: xs /\
P x /\ F x = \max_(x0 <- (a :: xs) | P x0) F x0
T: eqType P: pred T F: T -> nat a: T xs: seq T IH: has P xs ->
existsx : T,
x \in xs /\
P x /\ F x = \max_(x0 <- xs | P x0) F x0 HAS: has P (a :: xs) NOT: P a = false
existsx : T,
x \in a :: xs /\
P x /\ F x = \max_(x0 <- (a :: xs) | P x0) F x0
T: eqType P: pred T F: T -> nat a: T xs: seq T IH: has P xs ->
existsx : T,
x \in xs /\
P x /\ F x = \max_(x0 <- xs | P x0) F x0 NOT: P a = false HAS: has P xs
existsx : T,
x \in a :: xs /\
P x /\ F x = \max_(x0 <- (a :: xs) | P x0) F x0
T: eqType P: pred T F: T -> nat a: T xs: seq T IH: has P xs ->
existsx : T,
x \in xs /\
P x /\ F x = \max_(x0 <- xs | P x0) F x0 NOT: P a = false HAS: has P xs x: T IN: x \in xs Px: P x Fx: F x = \max_(x <- xs | P x) F x
existsx : T,
x \in a :: xs /\
P x /\ F x = \max_(x0 <- (a :: xs) | P x0) F x0
T: eqType P: pred T F: T -> nat a: T xs: seq T IH: has P xs ->
existsx : T,
x \in xs /\
P x /\ F x = \max_(x0 <- xs | P x0) F x0 NOT: P a = false HAS: has P xs x: T IN: x \in xs Px: P x Fx: F x = \max_(x <- xs | P x) F x
F x = \max_(x <- (a :: xs) | P x) F x
byrewrite big_cons ifF.
T: eqType P: pred T F: T -> nat a: T xs: seq T IH: has P xs ->
existsx : T,
x \in xs /\
P x /\ F x = \max_(x0 <- xs | P x0) F x0 HAS: has P (a :: xs)
P a ->
existsx : T,
x \in a :: xs /\
P x /\ F x = \max_(x0 <- (a :: xs) | P x0) F x0
T: eqType P: pred T F: T -> nat a: T xs: seq T IH: has P xs ->
existsx : T,
x \in xs /\
P x /\ F x = \max_(x0 <- xs | P x0) F x0 HAS: has P (a :: xs)
P a ->
existsx : T,
x \in a :: xs /\
P x /\ F x = \max_(x0 <- (a :: xs) | P x0) F x0
T: eqType P: pred T F: T -> nat a: T xs: seq T IH: has P xs ->
existsx : T,
x \in xs /\
P x /\ F x = \max_(x0 <- xs | P x0) F x0 HAS: has P (a :: xs) Pa: P a
existsx : T,
x \in a :: xs /\
P x /\ F x = \max_(x0 <- (a :: xs) | P x0) F x0
T: eqType P: pred T F: T -> nat a: T xs: seq T IH: has P xs ->
existsx : T,
x \in xs /\
P x /\ F x = \max_(x0 <- xs | P x0) F x0 HAS: has P (a :: xs) Pa: P a HAS': ~~ has P xs
existsx : T,
x \in a :: xs /\
P x /\ F x = \max_(x0 <- (a :: xs) | P x0) F x0
T: eqType P: pred T F: T -> nat a: T xs: seq T IH: has P xs ->
existsx : T,
x \in xs /\
P x /\ F x = \max_(x0 <- xs | P x0) F x0 HAS: has P (a :: xs) Pa: P a HAS': has P xs
existsx : T,
x \in a :: xs /\
P x /\ F x = \max_(x0 <- (a :: xs) | P x0) F x0
T: eqType P: pred T F: T -> nat a: T xs: seq T IH: has P xs ->
existsx : T,
x \in xs /\
P x /\ F x = \max_(x0 <- xs | P x0) F x0 HAS: has P (a :: xs) Pa: P a HAS': ~~ has P xs
existsx : T,
x \in a :: xs /\
P x /\ F x = \max_(x0 <- (a :: xs) | P x0) F x0
T: eqType P: pred T F: T -> nat a: T xs: seq T IH: has P xs ->
existsx : T,
x \in xs /\
P x /\ F x = \max_(x0 <- xs | P x0) F x0 HAS: has P (a :: xs) Pa: P a HAS': ~~ has P xs
F a = \max_(x <- (a :: xs) | P x) F x
byrewrite big_cons ifT // big_hasC.
T: eqType P: pred T F: T -> nat a: T xs: seq T IH: has P xs ->
existsx : T,
x \in xs /\
P x /\ F x = \max_(x0 <- xs | P x0) F x0 HAS: has P (a :: xs) Pa: P a HAS': has P xs
existsx : T,
x \in a :: xs /\
P x /\ F x = \max_(x0 <- (a :: xs) | P x0) F x0
T: eqType P: pred T F: T -> nat a: T xs: seq T IH: has P xs ->
existsx : T,
x \in xs /\
P x /\ F x = \max_(x0 <- xs | P x0) F x0 HAS: has P (a :: xs) Pa: P a HAS': has P xs
existsx : T,
x \in a :: xs /\
P x /\ F x = \max_(x0 <- (a :: xs) | P x0) F x0
T: eqType P: pred T F: T -> nat a: T xs: seq T IH: has P xs ->
existsx : T,
x \in xs /\
P x /\ F x = \max_(x0 <- xs | P x0) F x0 HAS: has P (a :: xs) Pa: P a HAS': has P xs x: T IN: x \in xs Px: P x MAX: F x = \max_(x <- xs | P x) F x
existsx : T,
x \in a :: xs /\
P x /\ F x = \max_(x0 <- (a :: xs) | P x0) F x0
T: eqType P: pred T F: T -> nat a: T xs: seq T IH: has P xs ->
existsx : T,
x \in xs /\
P x /\ F x = \max_(x0 <- xs | P x0) F x0 HAS: has P (a :: xs) Pa: P a HAS': has P xs x: T IN: x \in xs Px: P x MAX: F x = \max_(x <- xs | P x) F x
\max_(x <- xs | P x) F x <= F a ->
existsx : T,
x \in a :: xs /\
P x /\ F x = \max_(x0 <- (a :: xs) | P x0) F x0
T: eqType P: pred T F: T -> nat a: T xs: seq T IH: has P xs ->
existsx : T,
x \in xs /\
P x /\ F x = \max_(x0 <- xs | P x0) F x0 HAS: has P (a :: xs) Pa: P a HAS': has P xs x: T IN: x \in xs Px: P x MAX: F x = \max_(x <- xs | P x) F x
F a < \max_(x <- xs | P x) F x ->
existsx : T,
x \in a :: xs /\
P x /\ F x = \max_(x0 <- (a :: xs) | P x0) F x0
T: eqType P: pred T F: T -> nat a: T xs: seq T IH: has P xs ->
existsx : T,
x \in xs /\
P x /\ F x = \max_(x0 <- xs | P x0) F x0 HAS: has P (a :: xs) Pa: P a HAS': has P xs x: T IN: x \in xs Px: P x MAX: F x = \max_(x <- xs | P x) F x
\max_(x <- xs | P x) F x <= F a ->
existsx : T,
x \in a :: xs /\
P x /\ F x = \max_(x0 <- (a :: xs) | P x0) F x0
T: eqType P: pred T F: T -> nat a: T xs: seq T IH: has P xs ->
existsx : T,
x \in xs /\
P x /\ F x = \max_(x0 <- xs | P x0) F x0 HAS: has P (a :: xs) Pa: P a HAS': has P xs x: T IN: x \in xs Px: P x MAX: F x = \max_(x <- xs | P x) F x LEQ: \max_(x <- xs | P x) F x <= F a
existsx : T,
x \in a :: xs /\
P x /\ F x = \max_(x0 <- (a :: xs) | P x0) F x0
T: eqType P: pred T F: T -> nat a: T xs: seq T IH: has P xs ->
existsx : T,
x \in xs /\
P x /\ F x = \max_(x0 <- xs | P x0) F x0 HAS: has P (a :: xs) Pa: P a HAS': has P xs x: T IN: x \in xs Px: P x MAX: F x = \max_(x <- xs | P x) F x LEQ: \max_(x <- xs | P x) F x <= F a
a \in a :: xs /\
P a /\ F a = \max_(x <- (a :: xs) | P x) F x
T: eqType P: pred T F: T -> nat a: T xs: seq T IH: has P xs ->
existsx : T,
x \in xs /\
P x /\ F x = \max_(x0 <- xs | P x0) F x0 HAS: has P (a :: xs) Pa: P a HAS': has P xs x: T IN: x \in xs Px: P x MAX: F x = \max_(x <- xs | P x) F x LEQ: \max_(x <- xs | P x) F x <= F a
F a = \max_(x <- (a :: xs) | P x) F x
T: eqType P: pred T F: T -> nat a: T xs: seq T IH: has P xs ->
existsx : T,
x \in xs /\
P x /\ F x = \max_(x0 <- xs | P x0) F x0 HAS: has P (a :: xs) Pa: P a HAS': has P xs x: T IN: x \in xs Px: P x MAX: F x = \max_(x <- xs | P x) F x LEQ: \max_(x <- xs | P x) F x <= F a
(F a < \max_(j <- xs | P j) F j) = false
bylia.
T: eqType P: pred T F: T -> nat a: T xs: seq T IH: has P xs ->
existsx : T,
x \in xs /\
P x /\ F x = \max_(x0 <- xs | P x0) F x0 HAS: has P (a :: xs) Pa: P a HAS': has P xs x: T IN: x \in xs Px: P x MAX: F x = \max_(x <- xs | P x) F x
F a < \max_(x <- xs | P x) F x ->
existsx : T,
x \in a :: xs /\
P x /\ F x = \max_(x0 <- (a :: xs) | P x0) F x0
T: eqType P: pred T F: T -> nat a: T xs: seq T IH: has P xs ->
existsx : T,
x \in xs /\
P x /\ F x = \max_(x0 <- xs | P x0) F x0 HAS: has P (a :: xs) Pa: P a HAS': has P xs x: T IN: x \in xs Px: P x MAX: F x = \max_(x <- xs | P x) F x
F a < \max_(x <- xs | P x) F x ->
existsx : T,
x \in a :: xs /\
P x /\ F x = \max_(x0 <- (a :: xs) | P x0) F x0
T: eqType P: pred T F: T -> nat a: T xs: seq T IH: has P xs ->
existsx : T,
x \in xs /\
P x /\ F x = \max_(x0 <- xs | P x0) F x0 HAS: has P (a :: xs) Pa: P a HAS': has P xs x: T IN: x \in xs Px: P x MAX: F x = \max_(x <- xs | P x) F x LT: F a < \max_(x <- xs | P x) F x
existsx : T,
x \in a :: xs /\
P x /\ F x = \max_(x0 <- (a :: xs) | P x0) F x0
T: eqType P: pred T F: T -> nat a: T xs: seq T IH: has P xs ->
existsx : T,
x \in xs /\
P x /\ F x = \max_(x0 <- xs | P x0) F x0 HAS: has P (a :: xs) Pa: P a HAS': has P xs x: T IN: x \in xs Px: P x MAX: F x = \max_(x <- xs | P x) F x LT: F a < \max_(x <- xs | P x) F x
x \in a :: xs /\
P x /\ F x = \max_(x <- (a :: xs) | P x) F x
T: eqType P: pred T F: T -> nat a: T xs: seq T IH: has P xs ->
existsx : T,
x \in xs /\
P x /\ F x = \max_(x0 <- xs | P x0) F x0 HAS: has P (a :: xs) Pa: P a HAS': has P xs x: T IN: x \in xs Px: P x MAX: F x = \max_(x <- xs | P x) F x LT: F a < \max_(x <- xs | P x) F x
F x = \max_(x <- (a :: xs) | P x) F x
byrewrite big_cons ifT //= [maxn (_) (_)]/maxn ifT.}}}Qed.(** Additionally, we observe that, if two predicates yield different maxima, then there must exist a witness that satisfies only one of the predicates. *)
T: eqType
forall (xs : seq T) (P1P2 : T -> bool) (F : T -> nat),
\max_(x <- xs | P1 x) F x < \max_(x <- xs | P2 x) F x ->
existsx : T, x \in xs /\ ~~ P1 x /\ P2 x
T: eqType
forall (xs : seq T) (P1P2 : T -> bool) (F : T -> nat),
\max_(x <- xs | P1 x) F x < \max_(x <- xs | P2 x) F x ->
existsx : T, x \in xs /\ ~~ P1 x /\ P2 x
T: eqType xs: seq T P1, P2: T -> bool F: T -> nat LT: \max_(x <- xs | P1 x) F x <
\max_(x <- xs | P2 x) F x
existsx : T, x \in xs /\ ~~ P1 x /\ P2 x
T: eqType xs: seq T P1, P2: T -> bool F: T -> nat LT: \max_(x <- xs | P1 x) F x <
\max_(x <- xs | P2 x) F x HP1: has P1 xs HP2: has P2 xs
existsx : T, x \in xs /\ ~~ P1 x /\ P2 x
T: eqType xs: seq T P1, P2: T -> bool F: T -> nat LT: \max_(x <- xs | P1 x) F x <
\max_(x <- xs | P2 x) F x HP1: has P1 xs HP2: ~~ has P2 xs
existsx : T, x \in xs /\ ~~ P1 x /\ P2 x
T: eqType xs: seq T P1, P2: T -> bool F: T -> nat LT: \max_(x <- xs | P1 x) F x <
\max_(x <- xs | P2 x) F x HP1: ~~ has P1 xs HP2: has P2 xs
existsx : T, x \in xs /\ ~~ P1 x /\ P2 x
T: eqType xs: seq T P1, P2: T -> bool F: T -> nat LT: \max_(x <- xs | P1 x) F x <
\max_(x <- xs | P2 x) F x HP1: ~~ has P1 xs HP2: ~~ has P2 xs
existsx : T, x \in xs /\ ~~ P1 x /\ P2 x
T: eqType xs: seq T P1, P2: T -> bool F: T -> nat LT: \max_(x <- xs | P1 x) F x <
\max_(x <- xs | P2 x) F x HP1: has P1 xs HP2: has P2 xs
existsx : T, x \in xs /\ ~~ P1 x /\ P2 x
T: eqType xs: seq T P1, P2: T -> bool F: T -> nat LT: \max_(x <- xs | P1 x) F x <
\max_(x <- xs | P2 x) F x HP1: has P1 xs HP2: has P2 xs x2: T IN2: x2 \in xs Px2: P2 x2 MAX2: F x2 = \max_(x <- xs | P2 x) F x
existsx : T, x \in xs /\ ~~ P1 x /\ P2 x
T: eqType xs: seq T P1, P2: T -> bool F: T -> nat LT: \max_(x <- xs | P1 x) F x <
\max_(x <- xs | P2 x) F x HP1: has P1 xs HP2: has P2 xs x2: T IN2: x2 \in xs Px2: P2 x2 MAX2: F x2 = \max_(x <- xs | P2 x) F x
~~ P1 x2
T: eqType xs: seq T P1, P2: T -> bool F: T -> nat LT: \max_(x <- xs | P1 x) F x <
\max_(x <- xs | P2 x) F x HP1: has P1 xs HP2: has P2 xs x2: T IN2: x2 \in xs Px2: P2 x2 MAX2: F x2 = \max_(x <- xs | P2 x) F x Px1: P1 x2
False
T: eqType xs: seq T P1, P2: T -> bool F: T -> nat LT: \max_(x <- xs | P1 x) F x <
\max_(x <- xs | P2 x) F x HP1: has P1 xs HP2: has P2 xs x2: T IN2: x2 \in xs Px2: P2 x2 MAX2: F x2 = \max_(x <- xs | P2 x) F x Px1: P1 x2 BOUNDED: F x2 <= \max_(x <- xs | P1 x) F x
False
bylia.
T: eqType xs: seq T P1, P2: T -> bool F: T -> nat LT: \max_(x <- xs | P1 x) F x <
\max_(x <- xs | P2 x) F x HP1: has P1 xs HP2: ~~ has P2 xs
existsx : T, x \in xs /\ ~~ P1 x /\ P2 x
T: eqType xs: seq T P1, P2: T -> bool F: T -> nat LT: \max_(x <- xs | P1 x) F x <
\max_(x <- xs | P2 x) F x HP1: ~~ has P1 xs HP2: has P2 xs
existsx : T, x \in xs /\ ~~ P1 x /\ P2 x
T: eqType xs: seq T P1, P2: T -> bool F: T -> nat LT: \max_(x <- xs | P1 x) F x <
\max_(x <- xs | P2 x) F x HP1: ~~ has P1 xs HP2: ~~ has P2 xs
existsx : T, x \in xs /\ ~~ P1 x /\ P2 x
T: eqType xs: seq T P1, P2: T -> bool F: T -> nat LT: \max_(x <- xs | P1 x) F x <
\max_(x <- xs | P2 x) F x HP1: has P1 xs HP2: ~~ has P2 xs
T: eqType xs: seq T P1, P2: T -> bool F: T -> nat LT: \max_(x <- xs | P1 x) F x <
\max_(x <- xs | P2 x) F x HP1: ~~ has P1 xs HP2: has P2 xs
existsx : T, x \in xs /\ ~~ P1 x /\ P2 x
T: eqType xs: seq T P1, P2: T -> bool F: T -> nat LT: \max_(x <- xs | P1 x) F x <
\max_(x <- xs | P2 x) F x HP1: ~~ has P1 xs HP2: ~~ has P2 xs
existsx : T, x \in xs /\ ~~ P1 x /\ P2 x
T: eqType xs: seq T P1, P2: T -> bool F: T -> nat LT: \max_(x <- xs | P1 x) F x <
\max_(x <- xs | P2 x) F x HP1: ~~ has P1 xs HP2: has P2 xs
existsx : T, x \in xs /\ ~~ P1 x /\ P2 x
T: eqType xs: seq T P1, P2: T -> bool F: T -> nat LT: \max_(x <- xs | P1 x) F x <
\max_(x <- xs | P2 x) F x HP1: ~~ has P1 xs HP2: has P2 xs x2: T IN2: x2 \in xs Px2: P2 x2 MAX2: F x2 = \max_(x <- xs | P2 x) F x
existsx : T, x \in xs /\ ~~ P1 x /\ P2 x
T: eqType xs: seq T P1, P2: T -> bool F: T -> nat LT: \max_(x <- xs | P1 x) F x <
\max_(x <- xs | P2 x) F x HP1: ~~ has P1 xs HP2: has P2 xs x2: T IN2: x2 \in xs Px2: P2 x2 MAX2: F x2 = \max_(x <- xs | P2 x) F x
~~ P1 x2
T: eqType xs: seq T P1, P2: T -> bool F: T -> nat LT: \max_(x <- xs | P1 x) F x <
\max_(x <- xs | P2 x) F x HP2: has P2 xs x2: T IN2: x2 \in xs Px2: P2 x2 MAX2: F x2 = \max_(x <- xs | P2 x) F x HP1: {in xs, forallx : T, ~~ P1 x}
~~ P1 x2
bymove: (HP1 x2 IN2).
T: eqType xs: seq T P1, P2: T -> bool F: T -> nat LT: \max_(x <- xs | P1 x) F x <
\max_(x <- xs | P2 x) F x HP1: ~~ has P1 xs HP2: ~~ has P2 xs
existsx : T, x \in xs /\ ~~ P1 x /\ P2 x
T: eqType xs: seq T P1, P2: T -> bool F: T -> nat LT: \max_(x <- xs | P1 x) F x <
\max_(x <- xs | P2 x) F x HP1: ~~ has P1 xs HP2: ~~ has P2 xs
existsx : T, x \in xs /\ ~~ P1 x /\ P2 x
byexfalso; move: LT; rewrite !big_hasC.}Qed.(** Conversely, we observe that if one predicates implies another, then the corresponding maxima are related. *)
T: eqType
forall (xs : seq T) (P1P2 : pred T) (F : T -> nat),
(forallx : T, x \in xs -> P1 x -> P2 x) ->
\max_(x <- xs | P1 x) F x <= \max_(x <- xs | P2 x) F x
T: eqType
forall (xs : seq T) (P1P2 : pred T) (F : T -> nat),
(forallx : T, x \in xs -> P1 x -> P2 x) ->
\max_(x <- xs | P1 x) F x <= \max_(x <- xs | P2 x) F x
T: eqType xs: seq T P1, P2: pred T F: T -> nat IMPL: forallx : T, x \in xs -> P1 x -> P2 x
\max_(x <- xs | P1 x) F x <= \max_(x <- xs | P2 x) F x
T: eqType xs: seq T P1, P2: pred T F: T -> nat IMPL: forallx : T, x \in xs -> P1 x -> P2 x LT: \max_(x <- xs | P2 x) F x <
\max_(x <- xs | P1 x) F x
false
T: eqType xs: seq T P1, P2: pred T F: T -> nat IMPL: forallx : T, x \in xs -> P1 x -> P2 x LT: \max_(x <- xs | P2 x) F x <
\max_(x <- xs | P1 x) F x
False
T: eqType xs: seq T P1, P2: pred T F: T -> nat IMPL: forallx : T, x \in xs -> P1 x -> P2 x LT: \max_(x <- xs | P2 x) F x <
\max_(x <- xs | P1 x) F x x: T IN: x \in xs Px2: ~ P2 x Px1: P1 x