# A problem similar to intermediate value problem

My assumption is as follows :

f : Q -> Q
H1 : forall p q : Q, p == q -> f p == f q
H2 : forall q : Q, f q == 0 \/ f q == 1
H3 : forall p q : Q, p < q -> f p <= f q
a : Z
b : Z
c : positive
H4 : f(a # c) == 0
H5 : f(b # c) == 1
H6 : (a < b)%Z


In this assumption, I want to prove the following statement.

exists d : Z, (a <= d)%Z /\ (d < b)%Z /\ f(d # c) == 0 /\ f((d+1) # c) == 1


Informally, a function $$f$$ is a monotocially increasing function from $$\mathbb{Q}$$ to $$\{0, 1\}$$.

I think I need to do some inductive process.

However, I don't know how to initiate it.

Edit : The below is integers' version.

f : Z -> Z
H1 : forall n m : Z, n = m -> f n = f m
H2 : forall n : Z, f n = 0 \/ f n = 1
H3 : forall n m : Z, n < m -> f n <= f m
x y : Z
H4 : f(x) = 0
H5 : f(y) = 1
H6 : x < y


I want to prove that

exists w : Z, (x <= w) /\ (w < y) /\ f(w) = 0 /\ f(w+1) = 1

• What is $a \# c$, and what library are you using?
– Couchy
Aug 5 at 2:49
• @Couchy a#c denote a rational number, whose numerator is a, and denominator is c. I use QArith library. Aug 6 at 1:50

This is a proof of integer's version. To carry out induction, we can restate the theorem and leverage the induction principle of nat. I believe that there are easier ways to do this, but the following proof is the most straightforward one I can come up with.

Require Import ZArith.
Open Scope Z_scope.

Definition dichotomy (f : Z -> Z) := forall n : Z, f n = 0 \/ f n = 1.

Definition monotone (f : Z -> Z) := forall x y : Z, x < y -> f x <= f y.

Lemma intermediate' : forall (f : Z -> Z), dichotomy f -> monotone f ->
forall (m : Z) (n : nat), f m = 0 -> f (m + Z.of_nat n) = 1 ->
exists w : Z, 0 <= w /\ w < Z.of_nat n /\ f (m + w) = 0 /\ f (m + w + 1) = 1.
Proof.
intros f dich mono.
intros m n. induction n; intros Hfm Hfm'.
- destruct (Z.eq_dec (f (m + Z.of_nat n)) 1) as [E|E].
+ destruct (IHn Hfm E) as [w [W1 [W2 [W3 W4]]]].
exists w. intuition.
+ destruct (dich (m + Z.of_nat n)) as [E'|E'].
{ exists (Z.of_nat n).
split. apply Nat2Z.is_nonneg.
split. apply inj_lt. constructor.
split. exact E'.
rewrite->Nat2Z.inj_succ in Hfm'. rewrite<-Z.add_1_r in Hfm'.
rewrite->Zplus_assoc_reverse. exact Hfm'. }
{ congruence. }
Qed.

Lemma intermediate : forall (f : Z -> Z), dichotomy f -> monotone f ->
forall (m : Z) (n : Z), f m = 0 -> f n = 1 -> m < n ->
exists w : Z, m <= w /\ w < n /\ f w = 0 /\ f (w + 1) = 1.
Proof.
intros f dich mono. intros m n Hfm Hfm' ltmn.
replace n with (m + Z.of_nat (Z.to_nat (n - m))) in *.
- destruct (intermediate' _ dich mono m _ Hfm Hfm') as [w Hw]. exists (m + w).
split. { rewrite<-Z.add_0_r at 1. apply Zplus_le_compat_l. apply Hw. }
split. { apply Zplus_lt_compat_l. apply Hw. }
intuition.
- rewrite->ZifyInst.of_nat_to_nat_eq. rewrite->Z.max_r.
ring. apply Zle_minus_le_0. apply Z.lt_le_incl. exact ltmn.
Qed.

• Thank you for your help. I have a question. From the first Lemma, you assume that ... forall (m : Z) (n : nat) f m = 0 -> f (m + Z.of nat n) = 1 ... If so, then f m = 0, f m = 1, f(m+1) = 1, f(m+2) = 1... right? I think it is weird. Aug 4 at 1:15
• No. I think you might have put the brackets in the wrong place. What I wrote is ... forall (m : Z) (n : nat), A -> B -> C, which stands for ... (forall (m : Z) (n : nat), (A -> (B -> C))), not ... ((forall (m : Z) (n : nat), (A -> B)) -> C). Aug 4 at 2:56
• I understand it. Thank you Aug 4 at 2:58