A problem similar to intermediate value problem

Question

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

Answer 1

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'.
  - rewrite->Z.add_0_r in Hfm'. congruence.
  - 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.