Library Coqtail.Reals.Logic.Rmarkov

Require Import Reals.
Require Import Fourier.

Open Scope R_scope.

Section Definitions.

Variable f : nat → bool.

Definition fp (b : bool) n :=
  if b then pow (/ 2) (S n)
  else 0.

Fixpoint Bn n :=
match n with
| O ⇒ 0
| S n ⇒ Bn n + fp (f n) n
end.

Lemma Rlt_0_inv_2 : 0 < / 2.
Proof.
assert (H : 1 < 2).
  pattern 1 at 1; rewrite <- (Rplus_0_r 1).
  apply Rplus_lt_compat_l; apply Rlt_0_1.
apply Rmult_lt_reg_l with (r := 2).
  eapply Rlt_trans; [apply Rlt_0_1|apply H].
  rewrite Rmult_0_r.
  replace (2 × / 2) with 1; [apply Rlt_0_1|].
  rewrite Rmult_comm; symmetry; apply Rinv_l.
  intros Hneg.
  apply (Rlt_asym 1 0).
    rewrite <- Hneg; apply H.
    apply Rlt_0_1.
Qed.

Lemma Rle_0_inv_2 : 0 ≤ / 2.
Proof.
left; apply Rlt_0_inv_2.
Qed.

Lemma Bn_pos : ∀ n, 0 ≤ Bn n.
Proof.
intros n; induction n; simpl.
apply Rle_refl.
unfold fp; destruct f.
  apply Rplus_le_le_0_compat.
    assumption.
    apply pow_le; apply Rle_0_inv_2.
    rewrite Rplus_0_r; assumption.
Qed.

Lemma Bn_growing : ∀ n, (Bn n) ≤ (Bn (S n)).
Proof.
intros n; induction n; simpl.
unfold fp; destruct f.
  apply Rplus_le_le_0_compat.
    apply Rle_refl.
    apply pow_le; apply Rle_0_inv_2.
    rewrite Rplus_0_l; apply Rle_refl.
unfold fp.
assert (H : 0 ≤ (/2) ^ (S (S n))).
  apply pow_le; apply Rle_0_inv_2.
do 2 destruct f; repeat rewrite Rplus_assoc.
  apply Rplus_le_compat_l.
  pattern ((/ 2) ^ S n) at 1.
  rewrite <- (Rplus_0_r ((/ 2) ^ S n)).
  apply Rplus_le_compat_l.
  apply pow_le; apply Rle_0_inv_2.
  apply Rplus_le_compat_l.
  rewrite Rplus_0_r; apply Rle_refl.
  apply Rplus_le_compat_l.
  rewrite Rplus_0_l; apply pow_le; apply Rle_0_inv_2.
  repeat rewrite Rplus_0_r; apply Rle_refl.
Qed.

Lemma Bn_growing_trans : ∀ n N, (Bn n) ≤ (Bn (N + n)).
Proof.
intros n N.
induction N.
  simpl; apply Rle_refl.
  replace (S N + n)%nat with (S (N + n))%nat by omega.
  eapply Rle_trans.
    apply IHN.
    apply Bn_growing.
Qed.

Lemma Bn_dist : ∀ n, (Bn (S n)) - Bn n ≤ (/ 2) ^ (S n).
Proof.
intros n; simpl Bn.
replace (Bn n + fp (f n) n - Bn n)
  with (fp (f n) n) by ring.
  unfold fp; destruct f; simpl.
  apply Rle_refl.
  rewrite <- (Rmult_0_r 0).
  apply Rmult_le_compat.
    apply Rle_refl.
    apply Rle_refl.
    apply Rle_0_inv_2.
    apply pow_le; apply Rle_0_inv_2.
Qed.

Lemma Bn_dist_trans : ∀ n N, Bn (N + n) - Bn n ≤ (/ 2) ^ n × (1 - (/ 2) ^ N).
Proof.
intros n N.
induction N.
  simpl.
  unfold Rminus; repeat rewrite Rplus_opp_r.
  rewrite Rmult_0_r.
  apply Rle_refl.
  simpl plus.
  replace (Bn (S (N + n)) - Bn n)
    with (Bn (S (N + n)) - Bn (N + n) + (Bn (N + n) - Bn n))
    by ring.
  eapply Rle_trans.
    apply Rplus_le_compat.
      apply Bn_dist.
      apply IHN.
  repeat rewrite <- tech_pow_Rmult.
  rewrite pow_add.
  right.
  apply Rminus_diag_uniq; ring_simplify.
  replace (2 × / 2) with 1; [ring|].
  symmetry; rewrite Rmult_comm; apply Rinv_l.
  intros Hneg.
  apply (Rlt_asym 1 0).
    rewrite <- Hneg; pattern 1 at 1; rewrite <- (Rplus_0_r 1).
    apply Rplus_lt_compat_l; apply Rlt_0_1.
    apply Rlt_0_1.
Qed.

Lemma Bn_maj : ∀ n, Bn n ≤ 1.
Proof.
intros n.
pattern (Bn n) at 1.
replace (Bn n) with (Bn n - 0) by ring.
replace 0 with (Bn 0) by reflexivity.
replace n with (n + 0)%nat by ring.
eapply Rle_trans.
  apply Bn_dist_trans.
  simpl; rewrite <- Rmult_1_r.
  apply Rmult_le_compat_l; [apply Rle_0_1|].
  rewrite <- Rminus_0_r.
  apply Rplus_le_compat_l.
  apply Ropp_le_contravar.
  apply pow_le; apply Rle_0_inv_2.
Qed.

Let E r := ∃ n, Bn n = r.

Lemma Bn_lub : { l | is_lub E l }.
Proof.
destruct (completeness E) as [l Hl].
  ∃ 1.
  unfold is_upper_bound.
  intros r Hr.
  destruct Hr as [n Hn].
  rewrite <- Hn.
  apply Bn_maj.
  ∃ 0; ∃ 0%nat.
  reflexivity.
∃ l; assumption.
Qed.

Definition l := proj1_sig Bn_lub.
Definition Hlub := proj2_sig Bn_lub.

Lemma l_maj : ∀ n, Bn n ≤ l.
Proof.
intros n.
destruct Hlub as [Hb _].
apply Hb.
∃ n; reflexivity.
Qed.

Lemma l_lub : ∀ M, (∀ n, Bn n ≤ M) → l ≤ M.
Proof.
intros M HM.
destruct Hlub as [_ Hl].
apply Hl.
intros r Hr.
destruct Hr as [n Hn].
rewrite <- Hn.
apply HM.
Qed.

Lemma Rabs_le_maj : ∀ r1 r2 d, Rabs (r1 - r2) ≤ d → r1 ≤ r2 + d.
Proof.
intros r1 r2 d H.
unfold Rabs in H;
repeat destruct Rcase_abs in H; fourier.
Qed.

Lemma Bn_l_dist : ∀ n, l - Bn n ≤ (/2) ^ n.
Proof.
intros n.
apply (Rplus_le_reg_l (Bn n)); ring_simplify.
apply l_lub; intros m.
destruct (le_ge_dec m n) as [Hd|Hd].
  pattern (Bn m); rewrite <- Rplus_0_r.
  apply Rplus_le_compat.
    replace n with ((n - m) + m)%nat by omega.
    apply Bn_growing_trans.
    apply pow_le; apply Rle_0_inv_2.
  replace (Bn m) with (Bn n + (Bn m - Bn n)) by ring.
  apply Rplus_le_compat_l.
  replace m with ((m - n) + n)%nat by omega.
  eapply Rle_trans.
    apply Bn_dist_trans.
    rewrite <- Rmult_1_r.
    apply Rmult_le_compat_l.
      apply pow_le; apply Rle_0_inv_2.
      rewrite <- Rminus_0_r.
      apply Rplus_le_compat_l.
      apply Ropp_le_contravar.
      apply pow_le; apply Rle_0_inv_2.
Qed.

Lemma l_partial : ∀ N, (∀ n, (n ≤ N)%nat → f n = false) → l ≤ (/2) ^ N.
Proof.
intros N HN.
assert (∀ n, (n ≤ N)%nat → Bn n = 0).
  intros n H; induction n.
    reflexivity.
    replace (Bn (S n))
      with (Bn n + fp (f n) n) by reflexivity.
    rewrite IHn; [|omega].
    unfold fp.
    destruct (Bool.bool_dec (f n) true) as [Hd|Hd].
      destruct (Bool.eq_true_false_abs (f n)).
      assumption.
      apply HN; omega.
    destruct (f n) as [He|He].
      elim Hd; reflexivity.
      ring.
assert (Hd : Bn N = 0); [apply H; constructor|].
  replace l with (l - Bn N) by (rewrite Hd; ring).
  apply Bn_l_dist.
Qed.

Section l_is_zero.

Hypothesis Hl : l = 0.

Lemma l_R0 : ∀ n, f n = false.
Proof.
assert (H : ∀ n, Bn n = 0).
  intros n.
  apply Rle_antisym.
    rewrite <- Hl; apply l_maj.
    apply Bn_pos.
intros n; induction n.
  assert (H1 : Bn 1 = 0); [exact (H 1%nat)|].
  unfold Bn, fp in H1.
  destruct (f 0).
    simpl in H1; rewrite Rplus_0_l in H1.
    rewrite Rmult_1_r in H1; symmetry in H1.
    eelim Rlt_not_eq; [apply Rlt_0_inv_2|assumption].
    reflexivity.
  assert (Hn : Bn (S (S n)) = 0); [exact (H (S (S n)))|].
  replace (Bn (S (S n)))
    with (Bn (S n) + fp (f (S n)) (S n)) in Hn by reflexivity.
  unfold fp in Hn.
  destruct (f n).
    discriminate IHn.
    destruct (f (S n)).
    replace (Bn (S n)) with 0 in Hn by (symmetry; apply H).
    rewrite Rplus_0_l in Hn.
    assert (Hc : ∀ m, (/ 2) ^ m > 0).
      intros m; induction m; simpl.
        apply Rlt_0_1.
        apply Rmult_lt_0_compat.
        apply Rlt_0_inv_2.
        assumption.
    eelim Rgt_not_eq; [apply Hc|apply Hn].
    reflexivity.
Qed.

End l_is_zero.

Section f_is_false.

Hypothesis Hf : ∀ n, f n = false.

Lemma f_false : l = 0.
Proof.
apply Rle_antisym.
  apply l_lub.
  intros n.
  induction n; simpl.
    apply Rle_refl.
    assert (H : f n = false).
      apply Hf.
    unfold fp; destruct (f n).
      discriminate H.
    rewrite Rplus_0_r; assumption.
  apply Rle_trans with (Bn 0).
    apply Rle_refl.
    apply l_maj.
Qed.

End f_is_false.

Section l_not_zero.

Hypothesis Hl : l ≠ 0.

Lemma Hl_lt_0 : l > 0.
Proof.
assert (H : 0 ≤ l).
  eapply Rle_trans.
    apply (Bn_pos 0).
    apply l_maj.
destruct H.
  assumption.
  elim Hl; symmetry; assumption.
Qed.

Lemma l_not_R0_partial : ∃ N, ~(∀ n, (n ≤ N)%nat → f n = false).
Proof.
assert (Hlt : l > 0); [apply Hl_lt_0|].
assert (HN : ∃ N, ∀ n, (n ≥ N)%nat → (/ 2) ^ n < l).
  destruct (pow_lt_1_zero (/2)) with l as [N HN].
  rewrite Rabs_right; fourier.
  fourier.
  ∃ N; intros n Hn.
  pattern ((/ 2) ^ n); rewrite <- Rabs_right.
    apply HN; assumption.
    apply Rle_ge; apply pow_le; fourier.
destruct HN as [N HN].
∃ N; intros Hneg.
assert (Hc : l ≤ (/2) ^ N).
  apply l_partial; assumption.
assert (Hk : l > (/2) ^ N).
  apply HN; constructor.
fourier.
Qed.

Lemma l_not_R0 : ∃ n, f n ≠ false.
Proof.
destruct l_not_R0_partial as [N HN].
induction N.
  ∃ 0%nat; intro Hneg.
  destruct HN.
   intros n Hn; induction n.
     assumption.
     inversion Hn.
  destruct (Bool.bool_dec (f (S N)) true) as [H|H].
    ∃ (S N); intros Hneg.
      eapply Bool.eq_true_false_abs; eassumption.
    apply IHN; intros Hneg.
    apply Bool.not_true_is_false in H.
    apply HN; intros n Hn.
    destruct (eq_nat_dec n (S N)) as [Hd|Hd].
      rewrite Hd; assumption.
      apply Hneg; omega.
Qed.

End l_not_zero.

End Definitions.

Section Markov.

Variable P : nat → Prop.
Hypothesis P_dec : ∀ n, {P n} + {¬ P n}.

Let f n := if (P_dec n) then false else true.

Lemma Heq1 : ∀ n, f n ≠ false → ¬ P n.
Proof.
intros n; unfold f; intros H.
destruct (P_dec n) as [Hd|Hd].
  elim H; reflexivity.
  assumption.
Qed.

Lemma Heq2 : ∀ n, f n = false → P n.
Proof.
intros n; unfold f; intros H.
  destruct (P_dec n) as [Hd|Hd].
    assumption.
    discriminate H.
Qed.

Theorem R_markov : ¬ (∀ n, P n) → ∃ n, ¬ P n.
Proof.
intros Hneg.
destruct (l_not_R0 f) as [N HN].
  intros Hf.
  apply Hneg.
  intros n; apply l_R0 with (n := n) in Hf.
  apply Heq2; assumption.
∃ N; apply Heq1; assumption.
Qed.

Theorem R_sequence_dec : {∀ n, P n} + {¬ ∀ n, P n}.
Proof.
assert (H : {l f = 0} + {l f ≠ 0}).
  destruct (total_order_T (l f) 0) as [[Hlt|Heq]|Hgt].
  right; apply Rlt_not_eq; assumption.
  left; assumption.
  right; apply Rgt_not_eq; assumption.
destruct H as [H|H].
  left; intros n.
  destruct (P_dec n) as [Hd|Hd]; [assumption|].
  apply l_R0 with (n := n) in H.
  apply Heq2; assumption.
  right; intros Hneg; elim H.
  apply f_false; intros n.
  assert (Hd : {f n = false} + {f n ≠ false}).
    destruct (f n); [right|left].
      intros Hc; discriminate Hc.
      reflexivity.
  destruct Hd as [Hd|Hd]; [assumption|].
  apply Heq1 in Hd; elim Hd; apply Hneg.
Qed.

End Markov.