Solution to the problem "Infinite valleys and the limited principle of omniscience"

P2_omniscience.v

(* https://coq-math-problems.github.io/Problem2/ *)

Require Import Coq.Arith.Arith.
Require Import Coq.Classes.Morphisms.

Definition LPO := forall f : nat -> bool, (exists x, f x = true) \/ (forall x, f x = false).

Definition decr (f : nat -> nat) := forall n, f (S n) <= f n.

Definition infvalley (f : nat -> nat) (x : nat) := forall y, x <= y -> f y = f x.

Definition bool_to_nat (b : bool) := if b then 1 else 0.

Fixpoint all_up_to_n_false (f : nat -> bool) (n : nat) : bool :=
  match n with
  | O => negb (f n)
  | S n' => negb (f n) && all_up_to_n_false f n'
  end.

Definition mk_decr (f : nat -> bool) (n : nat) : nat := bool_to_nat (all_up_to_n_false f n).

Ltac simpl_mk_decr_everywhere := unfold mk_decr in *; simpl in *.

Lemma mk_decr_is_decr fb : decr (mk_decr fb).
Proof.
  intros n; induction n; simpl_mk_decr_everywhere.
  - destruct (fb 0), (fb 1); auto with arith.
  - destruct (fb (S n)), (fb (S (S n))); auto with arith.
Qed.

Lemma mk_decr_is_one {fb} n : mk_decr fb n = 1 -> forall m, m <= n -> fb m = false.
Proof.
  induction n; intros Hmk m Hle.
  - apply Nat.le_0_r in Hle; subst.
    now simpl_mk_decr_everywhere; destruct (fb 0).
  - simpl_mk_decr_everywhere.
    destruct (fb (S n)) eqn:Eq; [easy | inversion Hle; auto].
Qed.

Lemma mk_decr_is_zero {fb} n : mk_decr fb n = 0 -> exists m, fb m = true.
Proof.
  induction n; intros Hmk; simpl_mk_decr_everywhere.
  - exists 0. now destruct (fb 0).
  - destruct (fb (S n)) eqn:Eq; eauto.
Qed.

Lemma mk_decr_values f n : mk_decr f n = 0 \/ mk_decr f n = 1.
Proof.
  induction n; simpl_mk_decr_everywhere;
    [destruct (f 0) |  destruct (f (S n))]; auto.
Qed.

Theorem infvalley_LPO : (forall f, decr f -> exists x, infvalley f x) -> LPO.
Proof.
  intros Hv fb.
  specialize (Hv (mk_decr fb) (mk_decr_is_decr fb)) as [i Hv].
  destruct (mk_decr_values fb i) as [Heq | Heq].
  - apply mk_decr_is_zero in Heq; auto.
  - right; intros x.
    destruct (Nat.le_gt_cases x i).
    + apply (mk_decr_is_one _ Heq x H).
    + apply (mk_decr_is_one x); auto.
      rewrite Hv; auto with arith.
Qed.

Lemma decr_global {f} : decr f -> forall m n, m <= n -> f n <= f m.
Proof.
  intros Hd m n; induction 1 as [| m' Hle IHle]; [trivial |].
  exact (Nat.le_trans _ _ _ (Hd _) IHle).
Qed.

Lemma decr_min {f} y : decr f -> decr (fun n => min (f n) y).
Proof. intros H n. apply Nat.min_le_compat_r, H. Qed.

Lemma min_equal {f} z :
  decr f ->
  forall x, z <= x -> f x = Nat.min (f x) (f z).
Proof with (auto with arith).
  intros Hd x Hzn.
  destruct (Nat.min_dec (f x) (f z)) as [E | E]...
  rewrite E; apply Nat.min_r_iff in E.
  apply (decr_global Hd) in Hzn...
Qed.

Lemma min_max_antimono_decr {f} (Hd : decr f) x y :
  Nat.min (f x) (f y) = f (Nat.max x y).
Proof.
  apply Nat.min_max_antimono; intros x1 x2; [auto | apply (decr_global Hd)].
Qed.

Theorem LPO_infvalley : LPO -> forall f, decr f -> exists x, infvalley f x.
Proof with (eauto with arith).
  enough (LPO -> forall y f, f 0 = y -> decr f -> (exists x, infvalley f x))...
  intros L; induction y as [y IH] using lt_wf_ind; intros f <- Hd.
  specialize (L (fun n => f (S n) <? f n)); destruct L as [[i H]|H].
  - rewrite Nat.ltb_lt in H.
    pose proof (Nat.lt_le_trans _ _ _ H (decr_global Hd 0 i (Peano.le_0_n _))) as Hlt0.
    specialize (IH (f (S i))
                   Hlt0
                   (fun n => min (f n) (f (S i)))
                   (Nat.min_r _ _ (Nat.lt_le_incl _ _ Hlt0))
                   (decr_min (f (S i)) Hd)) as [x Hinf]; clear H Hlt0.
    exists (Nat.max x (S i)); intros y Hxy.
    apply Nat.max_lub_iff in Hxy as [Hxy HSiy].
    pose proof (min_equal (S i) Hd y HSiy) as Hy.
    specialize (Hinf y Hxy); simpl in Hinf; rewrite <-Hy in Hinf; clear Hy.
    rewrite Hinf.
    now apply min_max_antimono_decr.
  - exists 0; intros x _; induction x; [trivial|].
    specialize (H x); rewrite Nat.ltb_ge in H.
    rewrite <-IHx...
Qed.