Library prosa.util.minmax
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.11.2 (June 2020)
----------------------------------------------------------------------------- *)
Require Export prosa.util.notation prosa.util.nat prosa.util.list.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
(* Additional lemmas about max. *)
Section ExtraLemmas.
Lemma leq_bigmax_cond_seq (T : eqType) (P : pred T) (r : seq T) F i0 :
i0 \in r → P i0 → F i0 ≤ \max_(i <- r | P i) F i.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 37)
T : eqType
P : pred T
r : seq T
F : T -> nat
i0 : T
============================
i0 \in r -> P i0 -> F i0 <= \max_(i <- r | P i) F i
----------------------------------------------------------------------------- *)
Proof.
intros IN0 Pi0; by rewrite (big_rem i0) //= Pi0 leq_maxl.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Lemma bigmax_sup_seq:
∀ (T: eqType) (i: T) r (P: pred T) m F,
i \in r → P i → m ≤ F i → m ≤ \max_(i <- r| P i) F i.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 54)
============================
forall (T : eqType) (i : T) (r : seq_predType T)
(P : pred T) (m : nat) (F : T -> nat),
i \in r -> P i -> m <= F i -> m <= \max_(i0 <- r | P i0) F i0
----------------------------------------------------------------------------- *)
Proof.
intros.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 63)
T : eqType
i : T
r : seq_predType T
P : pred T
m : nat
F : T -> nat
H : i \in r
H0 : P i
H1 : m <= F i
============================
m <= \max_(i0 <- r | P i0) F i0
----------------------------------------------------------------------------- *)
induction r.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 73)
T : eqType
i : T
P : pred T
m : nat
F : T -> nat
H : i \in [::]
H0 : P i
H1 : m <= F i
============================
m <= \max_(i0 <- [::] | P i0) F i0
subgoal 2 (ID 80) is:
m <= \max_(i0 <- (a :: r) | P i0) F i0
----------------------------------------------------------------------------- *)
- by rewrite in_nil in H.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 80)
T : eqType
i, a : T
r : seq T
P : pred T
m : nat
F : T -> nat
H : i \in a :: r
H0 : P i
H1 : m <= F i
IHr : i \in r -> m <= \max_(i <- r | P i) F i
============================
m <= \max_(i0 <- (a :: r) | P i0) F i0
----------------------------------------------------------------------------- *)
move: H; rewrite in_cons; move ⇒ /orP [/eqP EQA | IN].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 204)
T : eqType
i, a : T
r : seq T
P : pred T
m : nat
F : T -> nat
H0 : P i
H1 : m <= F i
IHr : i \in r -> m <= \max_(i <- r | P i) F i
EQA : i = a
============================
m <= \max_(i0 <- (a :: r) | P i0) F i0
subgoal 2 (ID 205) is:
m <= \max_(i0 <- (a :: r) | P i0) F i0
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 204)
T : eqType
i, a : T
r : seq T
P : pred T
m : nat
F : T -> nat
H0 : P i
H1 : m <= F i
IHr : i \in r -> m <= \max_(i <- r | P i) F i
EQA : i = a
============================
m <= \max_(i0 <- (a :: r) | P i0) F i0
----------------------------------------------------------------------------- *)
clear IHr; subst a.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 208)
T : eqType
i : T
r : seq T
P : pred T
m : nat
F : T -> nat
H0 : P i
H1 : m <= F i
============================
m <= \max_(i0 <- (i :: r) | P i0) F i0
----------------------------------------------------------------------------- *)
rewrite (big_rem i) //=; last by rewrite in_cons; apply/orP; left.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 226)
T : eqType
i : T
r : seq T
P : pred T
m : nat
F : T -> nat
H0 : P i
H1 : m <= F i
============================
m <=
maxn (if P i then F i else 0)
(\max_(y <- (if i == i then r else i :: rem (T:=T) i r) | P y) F y)
----------------------------------------------------------------------------- *)
apply leq_trans with (F i); first by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 305)
T : eqType
i : T
r : seq T
P : pred T
m : nat
F : T -> nat
H0 : P i
H1 : m <= F i
============================
F i <=
maxn (if P i then F i else 0)
(\max_(y <- (if i == i then r else i :: rem (T:=T) i r) | P y) F y)
----------------------------------------------------------------------------- *)
by rewrite H0 leq_maxl.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 205)
subgoal 1 (ID 205) is:
m <= \max_(i0 <- (a :: r) | P i0) F i0
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 205)
T : eqType
i, a : T
r : seq T
P : pred T
m : nat
F : T -> nat
H0 : P i
H1 : m <= F i
IHr : i \in r -> m <= \max_(i <- r | P i) F i
IN : i \in r
============================
m <= \max_(i0 <- (a :: r) | P i0) F i0
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 205)
T : eqType
i, a : T
r : seq T
P : pred T
m : nat
F : T -> nat
H0 : P i
H1 : m <= F i
IHr : i \in r -> m <= \max_(i <- r | P i) F i
IN : i \in r
============================
m <= \max_(i0 <- (a :: r) | P i0) F i0
----------------------------------------------------------------------------- *)
apply leq_trans with (\max_(i0 <- r | P i0) F i0); first by apply IHr.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 318)
T : eqType
i, a : T
r : seq T
P : pred T
m : nat
F : T -> nat
H0 : P i
H1 : m <= F i
IHr : i \in r -> m <= \max_(i <- r | P i) F i
IN : i \in r
============================
\max_(i0 <- r | P i0) F i0 <= \max_(i0 <- (a :: r) | P i0) F i0
----------------------------------------------------------------------------- *)
rewrite [in X in _ ≤ X](big_rem a) //=; last by rewrite in_cons; apply/orP; left.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 342)
T : eqType
i, a : T
r : seq T
P : pred T
m : nat
F : T -> nat
H0 : P i
H1 : m <= F i
IHr : i \in r -> m <= \max_(i <- r | P i) F i
IN : i \in r
============================
\max_(i0 <- r | P i0) F i0 <=
maxn (if P a then F a else 0)
(\max_(y <- (if a == a then r else a :: rem (T:=T) a r) | P y) F y)
----------------------------------------------------------------------------- *)
have Ob: a == a; first by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 423)
T : eqType
i, a : T
r : seq T
P : pred T
m : nat
F : T -> nat
H0 : P i
H1 : m <= F i
IHr : i \in r -> m <= \max_(i <- r | P i) F i
IN : i \in r
Ob : a == a
============================
\max_(i0 <- r | P i0) F i0 <=
maxn (if P a then F a else 0)
(\max_(y <- (if a == a then r else a :: rem (T:=T) a r) | P y) F y)
----------------------------------------------------------------------------- *)
by rewrite Ob leq_maxr.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Lemma bigmax_leq_seqP (T : eqType) (P : pred T) (r : seq T) F m :
reflect (∀ i, i \in r → P i → F i ≤ m)
(\max_(i <- r | P i) F i ≤ m).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 75)
T : eqType
P : pred T
r : seq T
F : T -> nat
m : nat
============================
reflect (forall i : T, i \in r -> P i -> F i <= m)
(\max_(i <- r | P i) F i <= m)
----------------------------------------------------------------------------- *)
Proof.
apply: (iffP idP) ⇒ leFm ⇒ [i IINR Pi|];
first by apply: leq_trans leFm; apply leq_bigmax_cond_seq.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 110)
T : eqType
P : pred T
r : seq T
F : T -> nat
m : nat
leFm : forall i : T, i \in r -> P i -> F i <= m
============================
\max_(i <- r | P i) F i <= m
----------------------------------------------------------------------------- *)
rewrite big_seq_cond; elim/big_ind: _ ⇒ // m1 m2.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 232)
T : eqType
P : pred T
r : seq T
F : T -> nat
m : nat
leFm : forall i : T, i \in r -> P i -> F i <= m
m1, m2 : nat
============================
m1 <= m -> m2 <= m -> maxn m1 m2 <= m
subgoal 2 (ID 233) is:
F m1 <= m
----------------------------------------------------------------------------- *)
by intros; rewrite geq_max; apply/andP; split.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 233)
T : eqType
P : pred T
r : seq T
F : T -> nat
m : nat
leFm : forall i : T, i \in r -> P i -> F i <= m
m1 : T
m2 : (m1 \in r) && P m1
============================
F m1 <= m
----------------------------------------------------------------------------- *)
by move: m2 ⇒ /andP [M1IN Pm1]; apply: leFm.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Lemma leq_big_max (T : eqType) (P : pred T) (r : seq T) F1 F2 :
(∀ i, i \in r → P i → F1 i ≤ F2 i) →
\max_(i <- r | P i) F1 i ≤ \max_(i <- r | P i) F2 i.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 103)
T : eqType
P : pred T
r : seq T
F1, F2 : T -> nat
============================
(forall i : T, i \in r -> P i -> F1 i <= F2 i) ->
\max_(i <- r | P i) F1 i <= \max_(i <- r | P i) F2 i
----------------------------------------------------------------------------- *)
Proof.
intros; apply /bigmax_leq_seqP; intros.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 138)
T : eqType
P : pred T
r : seq T
F1, F2 : T -> nat
H : forall i : T, i \in r -> P i -> F1 i <= F2 i
i : T
H0 : i \in r
H1 : P i
============================
F1 i <= \max_(i0 <- r | P i0) F2 i0
----------------------------------------------------------------------------- *)
specialize (H i); feed_n 2 H; try(done).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 152)
T : eqType
P : pred T
r : seq T
F1, F2 : T -> nat
i : T
H : F1 i <= F2 i
H0 : i \in r
H1 : P i
============================
F1 i <= \max_(i0 <- r | P i0) F2 i0
----------------------------------------------------------------------------- *)
rewrite (big_rem i) //=; rewrite H1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 216)
T : eqType
P : pred T
r : seq T
F1, F2 : T -> nat
i : T
H : F1 i <= F2 i
H0 : i \in r
H1 : P i
============================
F1 i <= maxn (F2 i) (\max_(y <- rem (T:=T) i r | P y) F2 y)
----------------------------------------------------------------------------- *)
by apply leq_trans with (F2 i); [ | rewrite leq_maxl].
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Lemma bigmax_ord_ltn_identity n :
n > 0 →
\max_(i < n) i < n.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 113)
n : nat
============================
0 < n -> \max_(i < n) i < n
----------------------------------------------------------------------------- *)
Proof.
intros LT.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 114)
n : nat
LT : 0 < n
============================
\max_(i < n) i < n
----------------------------------------------------------------------------- *)
destruct n; first by rewrite ltn0 in LT.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 125)
n : nat
LT : 0 < n.+1
============================
\max_(i < n.+1) i < n.+1
----------------------------------------------------------------------------- *)
clear LT.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 137)
n : nat
============================
\max_(i < n.+1) i < n.+1
----------------------------------------------------------------------------- *)
induction n; first by rewrite big_ord_recr /= big_ord0 maxn0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 144)
n : nat
IHn : \max_(i < n.+1) i < n.+1
============================
\max_(i < n.+2) i < n.+2
----------------------------------------------------------------------------- *)
rewrite big_ord_recr /=.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 172)
n : nat
IHn : \max_(i < n.+1) i < n.+1
============================
maxn (\max_(i < n.+1) i) n.+1 < n.+2
----------------------------------------------------------------------------- *)
by unfold maxn at 1; rewrite IHn.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Lemma bigmax_ltn_ord n (P : pred nat) (i0: 'I_n) :
P i0 →
\max_(i < n | P i) i < n.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 125)
n : nat
P : pred nat
i0 : 'I_n
============================
P i0 -> \max_(i < n | P i) i < n
----------------------------------------------------------------------------- *)
Proof.
intros LT.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 126)
n : nat
P : pred nat
i0 : 'I_n
LT : P i0
============================
\max_(i < n | P i) i < n
----------------------------------------------------------------------------- *)
destruct n; first by destruct i0 as [i0 P0]; move: (P0) ⇒ P0'; rewrite ltn0 in P0'.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 142)
n : nat
P : pred nat
i0 : 'I_n.+1
LT : P i0
============================
\max_(i < n.+1 | P i) i < n.+1
----------------------------------------------------------------------------- *)
rewrite big_mkcond.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 176)
n : nat
P : pred nat
i0 : 'I_n.+1
LT : P i0
============================
\big[maxn_monoid/0]_i (if P i then i else 0) < n.+1
----------------------------------------------------------------------------- *)
apply leq_ltn_trans with (n := \max_(i < n.+1) i).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 184)
n : nat
P : pred nat
i0 : 'I_n.+1
LT : P i0
============================
\big[maxn_monoid/0]_i (if P i then i else 0) <= \max_(i < n.+1) i
subgoal 2 (ID 185) is:
\max_(i < n.+1) i < n.+1
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 184)
n : nat
P : pred nat
i0 : 'I_n.+1
LT : P i0
============================
\big[maxn_monoid/0]_i (if P i then i else 0) <= \max_(i < n.+1) i
----------------------------------------------------------------------------- *)
apply/bigmax_leqP; ins.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 243)
n : nat
P : pred nat
i0 : 'I_n.+1
LT : P i0
i : 'I_n.+1
H : true
============================
(if P i then i else 0) <= \max_(i1 < n.+1) i1
----------------------------------------------------------------------------- *)
destruct (P i); last by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 250)
n : nat
P : pred nat
i0 : 'I_n.+1
LT : P i0
i : 'I_n.+1
H : true
============================
i <= \max_(i1 < n.+1) i1
----------------------------------------------------------------------------- *)
by apply leq_bigmax_cond.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 185)
subgoal 1 (ID 185) is:
\max_(i < n.+1) i < n.+1
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 185)
n : nat
P : pred nat
i0 : 'I_n.+1
LT : P i0
============================
\max_(i < n.+1) i < n.+1
----------------------------------------------------------------------------- *)
by apply bigmax_ord_ltn_identity.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Lemma bigmax_pred n (P : pred nat) (i0: 'I_n) :
P (i0) →
P (\max_(i < n | P i) i).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 137)
n : nat
P : pred nat
i0 : 'I_n
============================
P i0 -> P (\max_(i < n | P i) i)
----------------------------------------------------------------------------- *)
Proof.
intros PRED.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 138)
n : nat
P : pred nat
i0 : 'I_n
PRED : P i0
============================
P (\max_(i < n | P i) i)
----------------------------------------------------------------------------- *)
induction n.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 150)
P : pred nat
i0 : 'I_0
PRED : P i0
============================
P (\max_(i < 0 | P i) i)
subgoal 2 (ID 157) is:
P (\max_(i < n.+1 | P i) i)
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 150)
P : pred nat
i0 : 'I_0
PRED : P i0
============================
P (\max_(i < 0 | P i) i)
----------------------------------------------------------------------------- *)
destruct i0 as [i0 P0].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 165)
P : pred nat
i0 : nat
P0 : i0 < 0
PRED : P (Ordinal (n:=0) (m:=i0) P0)
============================
P (\max_(i < 0 | P i) i)
----------------------------------------------------------------------------- *)
by move: (P0) ⇒ P1; rewrite ltn0 in P1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 157)
subgoal 1 (ID 157) is:
P (\max_(i < n.+1 | P i) i)
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 157)
n : nat
P : pred nat
i0 : 'I_n.+1
PRED : P i0
IHn : forall i0 : 'I_n, P i0 -> P (\max_(i < n | P i) i)
============================
P (\max_(i < n.+1 | P i) i)
----------------------------------------------------------------------------- *)
rewrite big_mkcond big_ord_recr /=.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 221)
n : nat
P : pred nat
i0 : 'I_n.+1
PRED : P i0
IHn : forall i0 : 'I_n, P i0 -> P (\max_(i < n | P i) i)
============================
P (maxn (\max_(i < n) (if P i then i else 0)) (if P n then n else 0))
----------------------------------------------------------------------------- *)
destruct (P n) eqn:Pn.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 233)
n : nat
P : pred nat
i0 : 'I_n.+1
PRED : P i0
IHn : forall i0 : 'I_n, P i0 -> P (\max_(i < n | P i) i)
Pn : P n = true
============================
P (maxn (\max_(i < n) (if P i then i else 0)) n)
subgoal 2 (ID 234) is:
P (maxn (\max_(i < n) (if P i then i else 0)) 0)
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 233)
n : nat
P : pred nat
i0 : 'I_n.+1
PRED : P i0
IHn : forall i0 : 'I_n, P i0 -> P (\max_(i < n | P i) i)
Pn : P n = true
============================
P (maxn (\max_(i < n) (if P i then i else 0)) n)
----------------------------------------------------------------------------- *)
destruct n; first by rewrite big_ord0 maxn0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 258)
n : nat
P : pred nat
i0 : 'I_n.+2
PRED : P i0
IHn : forall i0 : 'I_n.+1, P i0 -> P (\max_(i < n.+1 | P i) i)
Pn : P n.+1 = true
============================
P (maxn (\max_(i < n.+1) (if P i then i else 0)) n.+1)
----------------------------------------------------------------------------- *)
unfold maxn at 1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 272)
n : nat
P : pred nat
i0 : 'I_n.+2
PRED : P i0
IHn : forall i0 : 'I_n.+1, P i0 -> P (\max_(i < n.+1 | P i) i)
Pn : P n.+1 = true
============================
P
(if \max_(i < n.+1) (if P i then i else 0) < n.+1
then n.+1
else \max_(i < n.+1) (if P i then i else 0))
----------------------------------------------------------------------------- *)
destruct (\max_(i < n.+1) (match P (@nat_of_ord (S n) i) return nat with
| true ⇒ @nat_of_ord (S n) i
| false ⇒ O
end) < n.+1) eqn:Pi; first by rewrite Pi.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 290)
n : nat
P : pred nat
i0 : 'I_n.+2
PRED : P i0
IHn : forall i0 : 'I_n.+1, P i0 -> P (\max_(i < n.+1 | P i) i)
Pn : P n.+1 = true
Pi : (\max_(i < n.+1) (if P i then i else 0) < n.+1) = false
============================
P
(if \max_(i < n.+1) (if P i then i else 0) < n.+1
then n.+1
else \max_(i < n.+1) (if P i then i else 0))
----------------------------------------------------------------------------- *)
exfalso.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 293)
n : nat
P : pred nat
i0 : 'I_n.+2
PRED : P i0
IHn : forall i0 : 'I_n.+1, P i0 -> P (\max_(i < n.+1 | P i) i)
Pn : P n.+1 = true
Pi : (\max_(i < n.+1) (if P i then i else 0) < n.+1) = false
============================
False
----------------------------------------------------------------------------- *)
apply negbT in Pi; move: Pi ⇒ /negP BUG.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 323)
n : nat
P : pred nat
i0 : 'I_n.+2
PRED : P i0
IHn : forall i0 : 'I_n.+1, P i0 -> P (\max_(i < n.+1 | P i) i)
Pn : P n.+1 = true
BUG : ~ \max_(i < n.+1) (if P i then i else 0) < n.+1
============================
False
----------------------------------------------------------------------------- *)
apply BUG.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 324)
n : nat
P : pred nat
i0 : 'I_n.+2
PRED : P i0
IHn : forall i0 : 'I_n.+1, P i0 -> P (\max_(i < n.+1 | P i) i)
Pn : P n.+1 = true
BUG : ~ \max_(i < n.+1) (if P i then i else 0) < n.+1
============================
\max_(i < n.+1) (if P i then i else 0) < n.+1
----------------------------------------------------------------------------- *)
apply leq_ltn_trans with (n := \max_(i < n.+1) i).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 332)
n : nat
P : pred nat
i0 : 'I_n.+2
PRED : P i0
IHn : forall i0 : 'I_n.+1, P i0 -> P (\max_(i < n.+1 | P i) i)
Pn : P n.+1 = true
BUG : ~ \max_(i < n.+1) (if P i then i else 0) < n.+1
============================
\max_(i < n.+1) (if P i then i else 0) <= \max_(i < n.+1) i
subgoal 2 (ID 333) is:
\max_(i < n.+1) i < n.+1
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 332)
n : nat
P : pred nat
i0 : 'I_n.+2
PRED : P i0
IHn : forall i0 : 'I_n.+1, P i0 -> P (\max_(i < n.+1 | P i) i)
Pn : P n.+1 = true
BUG : ~ \max_(i < n.+1) (if P i then i else 0) < n.+1
============================
\max_(i < n.+1) (if P i then i else 0) <= \max_(i < n.+1) i
----------------------------------------------------------------------------- *)
apply/bigmax_leqP; ins.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 392)
n : nat
P : pred nat
i0 : 'I_n.+2
PRED : P i0
IHn : forall i0 : 'I_n.+1, P i0 -> P (\max_(i < n.+1 | P i) i)
Pn : P n.+1 = true
BUG : ~ \max_(i < n.+1) (if P i then i else 0) < n.+1
i : 'I_n.+1
H : true
============================
(if P i then i else 0) <= \max_(i1 < n.+1) i1
----------------------------------------------------------------------------- *)
destruct (P i); last by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 399)
n : nat
P : pred nat
i0 : 'I_n.+2
PRED : P i0
IHn : forall i0 : 'I_n.+1, P i0 -> P (\max_(i < n.+1 | P i) i)
Pn : P n.+1 = true
BUG : ~ \max_(i < n.+1) (if P i then i else 0) < n.+1
i : 'I_n.+1
H : true
============================
i <= \max_(i1 < n.+1) i1
----------------------------------------------------------------------------- *)
by apply leq_bigmax_cond.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 333)
subgoal 1 (ID 333) is:
\max_(i < n.+1) i < n.+1
subgoal 2 (ID 234) is:
P (maxn (\max_(i < n) (if P i then i else 0)) 0)
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 333)
n : nat
P : pred nat
i0 : 'I_n.+2
PRED : P i0
IHn : forall i0 : 'I_n.+1, P i0 -> P (\max_(i < n.+1 | P i) i)
Pn : P n.+1 = true
BUG : ~ \max_(i < n.+1) (if P i then i else 0) < n.+1
============================
\max_(i < n.+1) i < n.+1
----------------------------------------------------------------------------- *)
by apply bigmax_ord_ltn_identity.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 234)
subgoal 1 (ID 234) is:
P (maxn (\max_(i < n) (if P i then i else 0)) 0)
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 234)
n : nat
P : pred nat
i0 : 'I_n.+1
PRED : P i0
IHn : forall i0 : 'I_n, P i0 -> P (\max_(i < n | P i) i)
Pn : P n = false
============================
P (maxn (\max_(i < n) (if P i then i else 0)) 0)
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 234)
n : nat
P : pred nat
i0 : 'I_n.+1
PRED : P i0
IHn : forall i0 : 'I_n, P i0 -> P (\max_(i < n | P i) i)
Pn : P n = false
============================
P (maxn (\max_(i < n) (if P i then i else 0)) 0)
----------------------------------------------------------------------------- *)
rewrite maxn0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 407)
n : nat
P : pred nat
i0 : 'I_n.+1
PRED : P i0
IHn : forall i0 : 'I_n, P i0 -> P (\max_(i < n | P i) i)
Pn : P n = false
============================
P (\max_(i < n) (if P i then i else 0))
----------------------------------------------------------------------------- *)
rewrite -big_mkcond /=.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 417)
n : nat
P : pred nat
i0 : 'I_n.+1
PRED : P i0
IHn : forall i0 : 'I_n, P i0 -> P (\max_(i < n | P i) i)
Pn : P n = false
============================
P (\max_(i < n | P i) i)
----------------------------------------------------------------------------- *)
have LT: i0 < n.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 418)
n : nat
P : pred nat
i0 : 'I_n.+1
PRED : P i0
IHn : forall i0 : 'I_n, P i0 -> P (\max_(i < n | P i) i)
Pn : P n = false
============================
i0 < n
subgoal 2 (ID 420) is:
P (\max_(i < n | P i) i)
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 418)
n : nat
P : pred nat
i0 : 'I_n.+1
PRED : P i0
IHn : forall i0 : 'I_n, P i0 -> P (\max_(i < n | P i) i)
Pn : P n = false
============================
i0 < n
----------------------------------------------------------------------------- *)
rewrite ltn_neqAle; apply/andP; split;
last by rewrite -ltnS; apply ltn_ord.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 450)
n : nat
P : pred nat
i0 : 'I_n.+1
PRED : P i0
IHn : forall i0 : 'I_n, P i0 -> P (\max_(i < n | P i) i)
Pn : P n = false
============================
i0 != n
----------------------------------------------------------------------------- *)
apply/negP; move ⇒ /eqP BUG.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 510)
n : nat
P : pred nat
i0 : 'I_n.+1
PRED : P i0
IHn : forall i0 : 'I_n, P i0 -> P (\max_(i < n | P i) i)
Pn : P n = false
BUG : i0 = n
============================
False
----------------------------------------------------------------------------- *)
by rewrite -BUG PRED in Pn.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 420)
subgoal 1 (ID 420) is:
P (\max_(i < n | P i) i)
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 420)
n : nat
P : pred nat
i0 : 'I_n.+1
PRED : P i0
IHn : forall i0 : 'I_n, P i0 -> P (\max_(i < n | P i) i)
Pn : P n = false
LT : i0 < n
============================
P (\max_(i < n | P i) i)
----------------------------------------------------------------------------- *)
by rewrite (IHn (Ordinal LT)).
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End ExtraLemmas.