Library prosa.util.step_function
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.13.0 (January 2021)
----------------------------------------------------------------------------- *)
Require Import prosa.util.tactics prosa.util.notation.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat.
Section StepFunction.
Section Defs.
(* We say that a function f... *)
Variable f: nat → nat.
(* ...is a step function iff the following holds. *)
Definition is_step_function :=
∀ t, f (t + 1) ≤ f t + 1.
End Defs.
Section Lemmas.
(* Let f be any step function over natural numbers. *)
Variable f: nat → nat.
Hypothesis H_step_function: is_step_function f.
(* In this section, we prove a result similar to the intermediate
value theorem for continuous functions. *)
Section ExistsIntermediateValue.
(* Consider any interval [x1, x2]. *)
Variable x1 x2: nat.
Hypothesis H_is_interval: x1 ≤ x2.
(* Let t be any value such that f x1 < y < f x2. *)
Variable y: nat.
Hypothesis H_between: f x1 ≤ y < f x2.
(* Then, we prove that there exists an intermediate point x_mid such that
f x_mid = y. *)
Lemma exists_intermediate_point:
∃ x_mid, x1 ≤ x_mid < x2 ∧ f x_mid = y.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 9)
f : nat -> nat
H_step_function : is_step_function f
x1, x2 : nat
H_is_interval : x1 <= x2
y : nat
H_between : f x1 <= y < f x2
============================
exists x_mid : nat, x1 <= x_mid < x2 /\ f x_mid = y
----------------------------------------------------------------------------- *)
Proof.
rename H_is_interval into INT, H_step_function into STEP, H_between into BETWEEN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 10)
f : nat -> nat
STEP : is_step_function f
x1, x2 : nat
INT : x1 <= x2
y : nat
BETWEEN : f x1 <= y < f x2
============================
exists x_mid : nat, x1 <= x_mid < x2 /\ f x_mid = y
----------------------------------------------------------------------------- *)
move: x2 INT BETWEEN; clear x2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 16)
f : nat -> nat
STEP : is_step_function f
x1, y : nat
============================
forall x2 : nat,
x1 <= x2 ->
f x1 <= y < f x2 -> exists x_mid : nat, x1 <= x_mid < x2 /\ f x_mid = y
----------------------------------------------------------------------------- *)
suff DELTA:
∀ delta,
f x1 ≤ y < f (x1 + delta) →
∃ x_mid, x1 ≤ x_mid < x1 + delta ∧ f x_mid = y.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 23)
f : nat -> nat
STEP : is_step_function f
x1, y : nat
DELTA : forall delta : nat,
f x1 <= y < f (x1 + delta) ->
exists x_mid : nat, x1 <= x_mid < x1 + delta /\ f x_mid = y
============================
forall x2 : nat,
x1 <= x2 ->
f x1 <= y < f x2 -> exists x_mid : nat, x1 <= x_mid < x2 /\ f x_mid = y
subgoal 2 (ID 22) is:
forall delta : nat,
f x1 <= y < f (x1 + delta) ->
exists x_mid : nat, x1 <= x_mid < x1 + delta /\ f x_mid = y
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 23)
f : nat -> nat
STEP : is_step_function f
x1, y : nat
DELTA : forall delta : nat,
f x1 <= y < f (x1 + delta) ->
exists x_mid : nat, x1 <= x_mid < x1 + delta /\ f x_mid = y
============================
forall x2 : nat,
x1 <= x2 ->
f x1 <= y < f x2 -> exists x_mid : nat, x1 <= x_mid < x2 /\ f x_mid = y
----------------------------------------------------------------------------- *)
move ⇒ x2 LE /andP [GEy LTy].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 64)
f : nat -> nat
STEP : is_step_function f
x1, y : nat
DELTA : forall delta : nat,
f x1 <= y < f (x1 + delta) ->
exists x_mid : nat, x1 <= x_mid < x1 + delta /\ f x_mid = y
x2 : nat
LE : x1 <= x2
GEy : f x1 <= y
LTy : y < f x2
============================
exists x_mid : nat, x1 <= x_mid < x2 /\ f x_mid = y
----------------------------------------------------------------------------- *)
exploit (DELTA (x2 - x1));
first by apply/andP; split; last by rewrite addnBA // addKn.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 338)
f : nat -> nat
STEP : is_step_function f
x1, y : nat
DELTA : forall delta : nat,
f x1 <= y < f (x1 + delta) ->
exists x_mid : nat, x1 <= x_mid < x1 + delta /\ f x_mid = y
x2 : nat
LE : x1 <= x2
GEy : f x1 <= y
LTy : y < f x2
============================
(exists x_mid : nat, x1 <= x_mid < x1 + (x2 - x1) /\ f x_mid = y) ->
exists x_mid : nat, x1 <= x_mid < x2 /\ f x_mid = y
----------------------------------------------------------------------------- *)
by rewrite addnBA // addKn.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal
subgoal 1 (ID 22) is:
forall delta : nat,
f x1 <= y < f (x1 + delta) ->
exists x_mid : nat, x1 <= x_mid < x1 + delta /\ f x_mid = y
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 22)
f : nat -> nat
STEP : is_step_function f
x1, y : nat
============================
forall delta : nat,
f x1 <= y < f (x1 + delta) ->
exists x_mid : nat, x1 <= x_mid < x1 + delta /\ f x_mid = y
----------------------------------------------------------------------------- *)
induction delta.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 448)
f : nat -> nat
STEP : is_step_function f
x1, y : nat
============================
f x1 <= y < f (x1 + 0) ->
exists x_mid : nat, x1 <= x_mid < x1 + 0 /\ f x_mid = y
subgoal 2 (ID 451) is:
f x1 <= y < f (x1 + delta.+1) ->
exists x_mid : nat, x1 <= x_mid < x1 + delta.+1 /\ f x_mid = y
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 448)
f : nat -> nat
STEP : is_step_function f
x1, y : nat
============================
f x1 <= y < f (x1 + 0) ->
exists x_mid : nat, x1 <= x_mid < x1 + 0 /\ f x_mid = y
----------------------------------------------------------------------------- *)
rewrite addn0; move ⇒ /andP [GE0 LT0].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 495)
f : nat -> nat
STEP : is_step_function f
x1, y : nat
GE0 : f x1 <= y
LT0 : y < f x1
============================
exists x_mid : nat, x1 <= x_mid < x1 /\ f x_mid = y
----------------------------------------------------------------------------- *)
by apply (leq_ltn_trans GE0) in LT0; rewrite ltnn in LT0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal
subgoal 1 (ID 451) is:
f x1 <= y < f (x1 + delta.+1) ->
exists x_mid : nat, x1 <= x_mid < x1 + delta.+1 /\ f x_mid = y
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 451)
f : nat -> nat
STEP : is_step_function f
x1, y, delta : nat
IHdelta : f x1 <= y < f (x1 + delta) ->
exists x_mid : nat, x1 <= x_mid < x1 + delta /\ f x_mid = y
============================
f x1 <= y < f (x1 + delta.+1) ->
exists x_mid : nat, x1 <= x_mid < x1 + delta.+1 /\ f x_mid = y
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 451)
f : nat -> nat
STEP : is_step_function f
x1, y, delta : nat
IHdelta : f x1 <= y < f (x1 + delta) ->
exists x_mid : nat, x1 <= x_mid < x1 + delta /\ f x_mid = y
============================
f x1 <= y < f (x1 + delta.+1) ->
exists x_mid : nat, x1 <= x_mid < x1 + delta.+1 /\ f x_mid = y
----------------------------------------------------------------------------- *)
move ⇒ /andP [GT LT].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 581)
f : nat -> nat
STEP : is_step_function f
x1, y, delta : nat
IHdelta : f x1 <= y < f (x1 + delta) ->
exists x_mid : nat, x1 <= x_mid < x1 + delta /\ f x_mid = y
GT : f x1 <= y
LT : y < f (x1 + delta.+1)
============================
exists x_mid : nat, x1 <= x_mid < x1 + delta.+1 /\ f x_mid = y
----------------------------------------------------------------------------- *)
specialize (STEP (x1 + delta)); rewrite leq_eqVlt in STEP.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 602)
f : nat -> nat
x1, delta, y : nat
IHdelta : f x1 <= y < f (x1 + delta) ->
exists x_mid : nat, x1 <= x_mid < x1 + delta /\ f x_mid = y
GT : f x1 <= y
LT : y < f (x1 + delta.+1)
STEP : (f (x1 + delta + 1) == f (x1 + delta) + 1)
|| (f (x1 + delta + 1) < f (x1 + delta) + 1)
============================
exists x_mid : nat, x1 <= x_mid < x1 + delta.+1 /\ f x_mid = y
----------------------------------------------------------------------------- *)
have LE: y ≤ f (x1 + delta).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 603)
f : nat -> nat
x1, delta, y : nat
IHdelta : f x1 <= y < f (x1 + delta) ->
exists x_mid : nat, x1 <= x_mid < x1 + delta /\ f x_mid = y
GT : f x1 <= y
LT : y < f (x1 + delta.+1)
STEP : (f (x1 + delta + 1) == f (x1 + delta) + 1)
|| (f (x1 + delta + 1) < f (x1 + delta) + 1)
============================
y <= f (x1 + delta)
subgoal 2 (ID 605) is:
exists x_mid : nat, x1 <= x_mid < x1 + delta.+1 /\ f x_mid = y
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 603)
f : nat -> nat
x1, delta, y : nat
IHdelta : f x1 <= y < f (x1 + delta) ->
exists x_mid : nat, x1 <= x_mid < x1 + delta /\ f x_mid = y
GT : f x1 <= y
LT : y < f (x1 + delta.+1)
STEP : (f (x1 + delta + 1) == f (x1 + delta) + 1)
|| (f (x1 + delta + 1) < f (x1 + delta) + 1)
============================
y <= f (x1 + delta)
----------------------------------------------------------------------------- *)
move: STEP ⇒ /orP [/eqP EQ | STEP];
first by rewrite !addn1 in EQ; rewrite addnS EQ ltnS in LT.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 681)
f : nat -> nat
x1, delta, y : nat
IHdelta : f x1 <= y < f (x1 + delta) ->
exists x_mid : nat, x1 <= x_mid < x1 + delta /\ f x_mid = y
GT : f x1 <= y
LT : y < f (x1 + delta.+1)
STEP : f (x1 + delta + 1) < f (x1 + delta) + 1
============================
y <= f (x1 + delta)
----------------------------------------------------------------------------- *)
rewrite [X in _ < X]addn1 ltnS in STEP.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 754)
f : nat -> nat
x1, delta, y : nat
IHdelta : f x1 <= y < f (x1 + delta) ->
exists x_mid : nat, x1 <= x_mid < x1 + delta /\ f x_mid = y
GT : f x1 <= y
LT : y < f (x1 + delta.+1)
STEP : f (x1 + delta + 1) <= f (x1 + delta)
============================
y <= f (x1 + delta)
----------------------------------------------------------------------------- *)
apply: (leq_trans _ STEP).
(* ----------------------------------[ coqtop ]---------------------------------
1 focused subgoal
(shelved: 1) (ID 765)
f : nat -> nat
x1, delta, y : nat
IHdelta : f x1 <= y < f (x1 + delta) ->
exists x_mid : nat, x1 <= x_mid < x1 + delta /\ f x_mid = y
GT : f x1 <= y
LT : y < f (x1 + delta.+1)
STEP : f (x1 + delta + 1) <= f (x1 + delta)
============================
y <= f (x1 + delta + 1)
----------------------------------------------------------------------------- *)
by rewrite addn1 -addnS ltnW.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal
subgoal 1 (ID 605) is:
exists x_mid : nat, x1 <= x_mid < x1 + delta.+1 /\ f x_mid = y
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 605)
f : nat -> nat
x1, delta, y : nat
IHdelta : f x1 <= y < f (x1 + delta) ->
exists x_mid : nat, x1 <= x_mid < x1 + delta /\ f x_mid = y
GT : f x1 <= y
LT : y < f (x1 + delta.+1)
STEP : (f (x1 + delta + 1) == f (x1 + delta) + 1)
|| (f (x1 + delta + 1) < f (x1 + delta) + 1)
LE : y <= f (x1 + delta)
============================
exists x_mid : nat, x1 <= x_mid < x1 + delta.+1 /\ f x_mid = y
----------------------------------------------------------------------------- *)
clear STEP LT.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 779)
f : nat -> nat
x1, delta, y : nat
IHdelta : f x1 <= y < f (x1 + delta) ->
exists x_mid : nat, x1 <= x_mid < x1 + delta /\ f x_mid = y
GT : f x1 <= y
LE : y <= f (x1 + delta)
============================
exists x_mid : nat, x1 <= x_mid < x1 + delta.+1 /\ f x_mid = y
----------------------------------------------------------------------------- *)
rewrite leq_eqVlt in LE.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 797)
f : nat -> nat
x1, delta, y : nat
IHdelta : f x1 <= y < f (x1 + delta) ->
exists x_mid : nat, x1 <= x_mid < x1 + delta /\ f x_mid = y
GT : f x1 <= y
LE : (y == f (x1 + delta)) || (y < f (x1 + delta))
============================
exists x_mid : nat, x1 <= x_mid < x1 + delta.+1 /\ f x_mid = y
----------------------------------------------------------------------------- *)
move: LE ⇒ /orP [/eqP EQy | LT].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 872)
f : nat -> nat
x1, delta, y : nat
IHdelta : f x1 <= y < f (x1 + delta) ->
exists x_mid : nat, x1 <= x_mid < x1 + delta /\ f x_mid = y
GT : f x1 <= y
EQy : y = f (x1 + delta)
============================
exists x_mid : nat, x1 <= x_mid < x1 + delta.+1 /\ f x_mid = y
subgoal 2 (ID 873) is:
exists x_mid : nat, x1 <= x_mid < x1 + delta.+1 /\ f x_mid = y
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 872)
f : nat -> nat
x1, delta, y : nat
IHdelta : f x1 <= y < f (x1 + delta) ->
exists x_mid : nat, x1 <= x_mid < x1 + delta /\ f x_mid = y
GT : f x1 <= y
EQy : y = f (x1 + delta)
============================
exists x_mid : nat, x1 <= x_mid < x1 + delta.+1 /\ f x_mid = y
----------------------------------------------------------------------------- *)
∃ (x1 + delta); split; last by rewrite EQy.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 877)
f : nat -> nat
x1, delta, y : nat
IHdelta : f x1 <= y < f (x1 + delta) ->
exists x_mid : nat, x1 <= x_mid < x1 + delta /\ f x_mid = y
GT : f x1 <= y
EQy : y = f (x1 + delta)
============================
x1 <= x1 + delta < x1 + delta.+1
----------------------------------------------------------------------------- *)
by apply/andP; split; [by apply leq_addr | by rewrite addnS].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal
subgoal 1 (ID 873) is:
exists x_mid : nat, x1 <= x_mid < x1 + delta.+1 /\ f x_mid = y
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 873)
f : nat -> nat
x1, delta, y : nat
IHdelta : f x1 <= y < f (x1 + delta) ->
exists x_mid : nat, x1 <= x_mid < x1 + delta /\ f x_mid = y
GT : f x1 <= y
LT : y < f (x1 + delta)
============================
exists x_mid : nat, x1 <= x_mid < x1 + delta.+1 /\ f x_mid = y
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 873)
f : nat -> nat
x1, delta, y : nat
IHdelta : f x1 <= y < f (x1 + delta) ->
exists x_mid : nat, x1 <= x_mid < x1 + delta /\ f x_mid = y
GT : f x1 <= y
LT : y < f (x1 + delta)
============================
exists x_mid : nat, x1 <= x_mid < x1 + delta.+1 /\ f x_mid = y
----------------------------------------------------------------------------- *)
feed (IHdelta); first by apply/andP; split.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 917)
f : nat -> nat
x1, delta, y : nat
IHdelta : exists x_mid : nat, x1 <= x_mid < x1 + delta /\ f x_mid = y
GT : f x1 <= y
LT : y < f (x1 + delta)
============================
exists x_mid : nat, x1 <= x_mid < x1 + delta.+1 /\ f x_mid = y
----------------------------------------------------------------------------- *)
move: IHdelta ⇒ [x_mid [/andP [GE0 LT0] EQ0]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1005)
f : nat -> nat
x1, delta, y : nat
GT : f x1 <= y
LT : y < f (x1 + delta)
x_mid : nat
GE0 : x1 <= x_mid
LT0 : x_mid < x1 + delta
EQ0 : f x_mid = y
============================
exists x_mid0 : nat, x1 <= x_mid0 < x1 + delta.+1 /\ f x_mid0 = y
----------------------------------------------------------------------------- *)
∃ x_mid; split; last by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1009)
f : nat -> nat
x1, delta, y : nat
GT : f x1 <= y
LT : y < f (x1 + delta)
x_mid : nat
GE0 : x1 <= x_mid
LT0 : x_mid < x1 + delta
EQ0 : f x_mid = y
============================
x1 <= x_mid < x1 + delta.+1
----------------------------------------------------------------------------- *)
apply/andP; split; first by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1037)
f : nat -> nat
x1, delta, y : nat
GT : f x1 <= y
LT : y < f (x1 + delta)
x_mid : nat
GE0 : x1 <= x_mid
LT0 : x_mid < x1 + delta
EQ0 : f x_mid = y
============================
x_mid < x1 + delta.+1
----------------------------------------------------------------------------- *)
by apply: (leq_trans LT0); rewrite addnS.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End ExistsIntermediateValue.
End Lemmas.
(* In this section, we prove an analogue of the intermediate
value theorem, but for predicates of natural numbers. *)
Section ExistsIntermediateValuePredicates.
(* Let P be any predicate on natural numbers. *)
Variable P : nat → bool.
(* Consider a time interval [t1,t2] such that ... *)
Variables t1 t2 : nat.
Hypothesis H_t1_le_t2 : t1 ≤ t2.
(* ... P doesn't hold for t1 ... *)
Hypothesis H_not_P_at_t1 : ~~ P t1.
(* ... but holds for t2. *)
Hypothesis H_P_at_t2 : P t2.
(* Then we prove that within time interval [t1,t2] there exists time
instant t such that t is the first time instant when P holds. *)
Lemma exists_first_intermediate_point:
∃ t, (t1 < t ≤ t2) ∧ (∀ x, t1 ≤ x < t → ~~ P x) ∧ P t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 9)
P : nat -> bool
t1, t2 : nat
H_t1_le_t2 : t1 <= t2
H_not_P_at_t1 : ~~ P t1
H_P_at_t2 : P t2
============================
exists t : nat,
t1 < t <= t2 /\ (forall x : nat, t1 <= x < t -> ~~ P x) /\ P t
----------------------------------------------------------------------------- *)
Proof.
have EX: ∃ x, P x && (t1 < x ≤ t2).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 12)
P : nat -> bool
t1, t2 : nat
H_t1_le_t2 : t1 <= t2
H_not_P_at_t1 : ~~ P t1
H_P_at_t2 : P t2
============================
exists x : nat, [&& P x, t1 < x & x <= t2]
subgoal 2 (ID 14) is:
exists t : nat,
t1 < t <= t2 /\ (forall x : nat, t1 <= x < t -> ~~ P x) /\ P t
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 12)
P : nat -> bool
t1, t2 : nat
H_t1_le_t2 : t1 <= t2
H_not_P_at_t1 : ~~ P t1
H_P_at_t2 : P t2
============================
exists x : nat, [&& P x, t1 < x & x <= t2]
----------------------------------------------------------------------------- *)
∃ t2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 16)
P : nat -> bool
t1, t2 : nat
H_t1_le_t2 : t1 <= t2
H_not_P_at_t1 : ~~ P t1
H_P_at_t2 : P t2
============================
[&& P t2, t1 < t2 & t2 <= t2]
----------------------------------------------------------------------------- *)
apply/andP; split; first by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 43)
P : nat -> bool
t1, t2 : nat
H_t1_le_t2 : t1 <= t2
H_not_P_at_t1 : ~~ P t1
H_P_at_t2 : P t2
============================
t1 < t2 <= t2
----------------------------------------------------------------------------- *)
apply/andP; split; last by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 69)
P : nat -> bool
t1, t2 : nat
H_t1_le_t2 : t1 <= t2
H_not_P_at_t1 : ~~ P t1
H_P_at_t2 : P t2
============================
t1 < t2
----------------------------------------------------------------------------- *)
move: H_t1_le_t2; rewrite leq_eqVlt; move ⇒ /orP [/eqP EQ | NEQ1]; last by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 148)
P : nat -> bool
t1, t2 : nat
H_t1_le_t2 : t1 <= t2
H_not_P_at_t1 : ~~ P t1
H_P_at_t2 : P t2
EQ : t1 = t2
============================
t1 < t2
----------------------------------------------------------------------------- *)
by exfalso; subst t2; move: H_not_P_at_t1 ⇒ /negP NPt1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal
subgoal 1 (ID 14) is:
exists t : nat,
t1 < t <= t2 /\ (forall x : nat, t1 <= x < t -> ~~ P x) /\ P t
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 14)
P : nat -> bool
t1, t2 : nat
H_t1_le_t2 : t1 <= t2
H_not_P_at_t1 : ~~ P t1
H_P_at_t2 : P t2
EX : exists x : nat, [&& P x, t1 < x & x <= t2]
============================
exists t : nat,
t1 < t <= t2 /\ (forall x : nat, t1 <= x < t -> ~~ P x) /\ P t
----------------------------------------------------------------------------- *)
have MIN := ex_minnP EX.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 214)
P : nat -> bool
t1, t2 : nat
H_t1_le_t2 : t1 <= t2
H_not_P_at_t1 : ~~ P t1
H_P_at_t2 : P t2
EX : exists x : nat, [&& P x, t1 < x & x <= t2]
MIN : ex_minn_spec (fun x : nat => [&& P x, t1 < x & x <= t2])
(ex_minn (P:=fun x : nat => [&& P x, t1 < x & x <= t2]) EX)
============================
exists t : nat,
t1 < t <= t2 /\ (forall x : nat, t1 <= x < t -> ~~ P x) /\ P t
----------------------------------------------------------------------------- *)
move: MIN ⇒ [x /andP [Px /andP [LT1 LT2]] MIN]; clear EX.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 304)
P : nat -> bool
t1, t2 : nat
H_t1_le_t2 : t1 <= t2
H_not_P_at_t1 : ~~ P t1
H_P_at_t2 : P t2
x : nat
Px : P x
LT1 : t1 < x
LT2 : x <= t2
MIN : forall n : nat, [&& P n, t1 < n & n <= t2] -> x <= n
============================
exists t : nat,
t1 < t <= t2 /\ (forall x0 : nat, t1 <= x0 < t -> ~~ P x0) /\ P t
----------------------------------------------------------------------------- *)
∃ x; repeat split; [ apply/andP; split | | ]; try done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 312)
P : nat -> bool
t1, t2 : nat
H_t1_le_t2 : t1 <= t2
H_not_P_at_t1 : ~~ P t1
H_P_at_t2 : P t2
x : nat
Px : P x
LT1 : t1 < x
LT2 : x <= t2
MIN : forall n : nat, [&& P n, t1 < n & n <= t2] -> x <= n
============================
forall x0 : nat, t1 <= x0 < x -> ~~ P x0
----------------------------------------------------------------------------- *)
move ⇒ y /andP [NEQ1 NEQ2]; apply/negPn; intros Py.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 447)
P : nat -> bool
t1, t2 : nat
H_t1_le_t2 : t1 <= t2
H_not_P_at_t1 : ~~ P t1
H_P_at_t2 : P t2
x : nat
Px : P x
LT1 : t1 < x
LT2 : x <= t2
MIN : forall n : nat, [&& P n, t1 < n & n <= t2] -> x <= n
y : nat
NEQ1 : t1 <= y
NEQ2 : y < x
Py : P y
============================
False
----------------------------------------------------------------------------- *)
feed (MIN y).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 448)
P : nat -> bool
t1, t2 : nat
H_t1_le_t2 : t1 <= t2
H_not_P_at_t1 : ~~ P t1
H_P_at_t2 : P t2
x : nat
Px : P x
LT1 : t1 < x
LT2 : x <= t2
MIN : forall n : nat, [&& P n, t1 < n & n <= t2] -> x <= n
y : nat
NEQ1 : t1 <= y
NEQ2 : y < x
Py : P y
============================
[&& P y, t1 < y & y <= t2]
subgoal 2 (ID 453) is:
False
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 448)
P : nat -> bool
t1, t2 : nat
H_t1_le_t2 : t1 <= t2
H_not_P_at_t1 : ~~ P t1
H_P_at_t2 : P t2
x : nat
Px : P x
LT1 : t1 < x
LT2 : x <= t2
MIN : forall n : nat, [&& P n, t1 < n & n <= t2] -> x <= n
y : nat
NEQ1 : t1 <= y
NEQ2 : y < x
Py : P y
============================
[&& P y, t1 < y & y <= t2]
----------------------------------------------------------------------------- *)
apply/andP; split; first by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 480)
P : nat -> bool
t1, t2 : nat
H_t1_le_t2 : t1 <= t2
H_not_P_at_t1 : ~~ P t1
H_P_at_t2 : P t2
x : nat
Px : P x
LT1 : t1 < x
LT2 : x <= t2
MIN : forall n : nat, [&& P n, t1 < n & n <= t2] -> x <= n
y : nat
NEQ1 : t1 <= y
NEQ2 : y < x
Py : P y
============================
t1 < y <= t2
----------------------------------------------------------------------------- *)
apply/andP; split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 506)
P : nat -> bool
t1, t2 : nat
H_t1_le_t2 : t1 <= t2
H_not_P_at_t1 : ~~ P t1
H_P_at_t2 : P t2
x : nat
Px : P x
LT1 : t1 < x
LT2 : x <= t2
MIN : forall n : nat, [&& P n, t1 < n & n <= t2] -> x <= n
y : nat
NEQ1 : t1 <= y
NEQ2 : y < x
Py : P y
============================
t1 < y
subgoal 2 (ID 507) is:
y <= t2
----------------------------------------------------------------------------- *)
- move: NEQ1.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 509)
P : nat -> bool
t1, t2 : nat
H_t1_le_t2 : t1 <= t2
H_not_P_at_t1 : ~~ P t1
H_P_at_t2 : P t2
x : nat
Px : P x
LT1 : t1 < x
LT2 : x <= t2
MIN : forall n : nat, [&& P n, t1 < n & n <= t2] -> x <= n
y : nat
NEQ2 : y < x
Py : P y
============================
t1 <= y -> t1 < y
subgoal 2 (ID 507) is:
y <= t2
----------------------------------------------------------------------------- *)
rewrite leq_eqVlt; move ⇒ /orP [/eqP EQ | NEQ1]; last by done.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 586)
P : nat -> bool
t1, t2 : nat
H_t1_le_t2 : t1 <= t2
H_not_P_at_t1 : ~~ P t1
H_P_at_t2 : P t2
x : nat
Px : P x
LT1 : t1 < x
LT2 : x <= t2
MIN : forall n : nat, [&& P n, t1 < n & n <= t2] -> x <= n
y : nat
NEQ2 : y < x
Py : P y
EQ : t1 = y
============================
t1 < y
subgoal 2 (ID 507) is:
y <= t2
----------------------------------------------------------------------------- *)
by exfalso; subst y; move: H_not_P_at_t1 ⇒ /negP NPt1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 507)
P : nat -> bool
t1, t2 : nat
H_t1_le_t2 : t1 <= t2
H_not_P_at_t1 : ~~ P t1
H_P_at_t2 : P t2
x : nat
Px : P x
LT1 : t1 < x
LT2 : x <= t2
MIN : forall n : nat, [&& P n, t1 < n & n <= t2] -> x <= n
y : nat
NEQ1 : t1 <= y
NEQ2 : y < x
Py : P y
============================
y <= t2
----------------------------------------------------------------------------- *)
- by apply ltnW, leq_trans with x.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal
subgoal 1 (ID 453) is:
False
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 453)
P : nat -> bool
t1, t2 : nat
H_t1_le_t2 : t1 <= t2
H_not_P_at_t1 : ~~ P t1
H_P_at_t2 : P t2
x : nat
Px : P x
LT1 : t1 < x
LT2 : x <= t2
y : nat
MIN : x <= y
NEQ1 : t1 <= y
NEQ2 : y < x
Py : P y
============================
False
----------------------------------------------------------------------------- *)
by move: NEQ2; rewrite ltnNge; move ⇒ /negP NEQ2.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End ExistsIntermediateValuePredicates.
End StepFunction.