0
$\begingroup$

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
$\endgroup$
2
  • $\begingroup$ What is $a \# c$, and what library are you using? $\endgroup$
    – Couchy
    Aug 5 at 2:49
  • $\begingroup$ @Couchy a#c denote a rational number, whose numerator is a, and denominator is c. I use QArith library. $\endgroup$ Aug 6 at 1:50

1 Answer 1

1
$\begingroup$

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.
$\endgroup$
3
  • $\begingroup$ 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. $\endgroup$ Aug 4 at 1:15
  • 1
    $\begingroup$ 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). $\endgroup$ Aug 4 at 2:56
  • $\begingroup$ I understand it. Thank you $\endgroup$ Aug 4 at 2:58

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.