Classical axiomatisation of reals

[Pierre-Marie Pédrot]

Dear coq users and developpers,

We're currently working on a class project based on Coq for our master's
first year at the ENS of Lyon. Our goals include extending stdlib with
lemmas which ought to be there, and commenting/cleaning stdlib in order
to conform to the naming convention.

Across our work on real analysis and properties of real numbers, we
realized (and proved) that Coq's classical axiomatization of reals
implied Markov's principle and countable principle of omniscience. After
some research, we found out that it had been already proved by Kaliszyk
and O'Connor, and that is was to be put in stdlib (although I did not
find it in the SVN yet).

So I came up with two questions :

- From a purely logical point of view, does classical axiomatization of
reals implies stronger than those two principles? (I guess not, as the
main classical facts comes from the decidability of equality on reals,
which is isomorphic to decidable equality on sequences nat -> bool).

- Is there any interest to create a "per se" library of real numbers
that would not use classical facts in their full power?

I mean, most of the classical theorems of real analysis rely only upon
countable principle of omniscience (as most of the properties are
defined in terms of sequences). We could that way prove those theorems
using only the very nature of classical reals, and nothing more.

One of the most salient examples would be Bolzano-Weierstrass theorem
which is, I think, provable using only properties entailed by the
classical axiomatisation.

That way, we would have a three-level distinction on real analysis theorem :

1. Purely constructive theorems (that don't use dedidable equality)
2. Partly classical theorems (that only use Markov or omniscience)
3. Fully classical theorems (that use excluded middle over uncoutable sets)

As we have got time to spare to demonstrate such theorems, do you Coq
users and developpers think that it could have any interest? Or could we
rewrite semi-classical theorems of stdlib using the aforementioned
principles?

Cordially,
Pierre-Marie Pédrot

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[hugo.herbelin]

Hi,

> Across our work on real analysis and properties of real numbers, we
> realized (and proved) that Coq's classical axiomatization of reals
> implied Markov's principle and countable principle of omniscience. After
> some research, we found out that it had been already proved by Kaliszyk
> and O'Connor, and that is was to be put in stdlib (although I did not
> find it in the SVN yet).

Notice that the proof that you found in Rlogic.v uses classical logic
(there is a call to the classical axiom not_all_ex_not of type
"~ forall n, P n -> exists n, ~ P n"). If your proof does not use
classical axiom, it is a stronger result.

One known result implied by the axiomatic of reals is the existence of
a decision function for any negative proposition (I mean here the
statement "forall A, {~A}+{~~A}"). This is proved using a
Diaconescu-style argument shown to me by Benjamin Werner (file
attached). I'm interested in your proof of the principle of
omniscience because we had some conjecture at some time that a
modification of the argument used for proving "forall A, {~A}+{~~A}"
could also prove omniscience (the idea, for P decidable, is to
consider the set made of 0 and of every 1/n such that P(n) is true;
this set is non empty and bound by 1; therefore it has a least upper
bound; if this lub is 0 then a proof of forall n, ~P(n) should be
derivable, otherwise, it should be provable that this upper bound is
1/n0 for some n0 and P(n0) is then provable).

Also, if you have a proof of omniscience derived only from the
axiomatic of R, then you will probably be able to simplify the current
axiomatization by deriving the Archimedian axiom. Indeed, from
{n | INR n > r}+ {forall n, INR n <= r} and the classical formulation
of Archimede ~(forall n, INR n <= r) (see Rlogic.v), it is reasonable
to think that you will be able to extract a function up : R -> Z that
will satisfy the axiom "archimed" of the Raxioms.v file.

> - Is there any interest to create a "per se" library of real numbers
> that would not use classical facts in their full power?

From the point of view of analysis I don't know. From the point of
view of provability strength, I find it interesting to know.

Best regards,

Hugo Herbelin

Require Import Raxioms.
Require Import RIneq.

Section EM_neg.

Variable A : Prop.

Let P (x : R) := x = 0%R \/ x = 1%R /\ A.

Theorem EM_neg : {~ ~ A} + {~ A}.
assert (Hnonempty : exists x : _, P x).
  exists 0%R; red in |- *; tauto.
assert (Hbound : bound P).
  exists 1%R. intros x [Hx_eq_0| (Hx_eq_1, _)].
SearchPattern (_ <= 1)%R.
  rewrite Hx_eq_0; left; apply Rlt_0_1.
  rewrite Hx_eq_1; right; reflexivity.
destruct (completeness P Hbound Hnonempty) as (y, (Hy_bound, Hy_lub)).
destruct (Rlt_le_dec y 1) as [Hy_lt_1| H_1_le_y].
(* y < 1 *)
right; intro Ha.

  assert (H_1_in_P : P 1).
    red in |- *; tauto.
  assert (H_1_inf_y : (1 <= y)%R).
    apply Hy_bound with (1 := H_1_in_P).
  apply Rlt_not_le with (1 := Hy_lt_1).
  apply H_1_inf_y.

(* y >= 1 *)
left; intro Hna.
assert (~ (forall z : R, (0 < z)%R -> ~ P z)).
  intro H.
  assert (H_0_lub : is_upper_bound P 0).
    intros r Hr_in_P.
    destruct (Rlt_le_dec 0 r) as [H_0_lt_r| H_r_le_0].
      elim (H r H_0_lt_r Hr_in_P).
      assumption.
  assert (Hy_le_0 : (y <= 0)%R).
    apply Hy_lub; assumption.
  apply Rlt_irrefl with y.
  apply Rle_lt_trans with 0%R.
    exact Hy_le_0.
  apply Rlt_le_trans with 1%R.
  apply Rlt_0_1.
  exact H_1_le_y.
apply H; intros z Hz_lt_0 [Hz_eq_0| (Hz_eq_1, Ha)].
  (* z = 0, mais 0 < z *)
  rewrite Hz_eq_0 in Hz_lt_0.
  apply Rlt_irrefl with (1 := Hz_lt_0).
  (* z = 1 et A, mais ~A *)
  apply (Hna Ha).
Qed.

End EM_neg.

Print Assumptions EM_neg.

[Pierre-Marie Pédrot]

hugo.herbelin@... a écrit :
> Notice that the proof that you found in Rlogic.v uses classical logic
> (there is a call to the classical axiom not_all_ex_not of type
> "~ forall n, P n -> exists n, ~ P n"). If your proof does not use
> classical axiom, it is a stronger result.

I am unsure about the classical properties used; yet I don't think this
is the case, as long as the two extern lemmas thereafter are
intuitionnistic:

- Un_cv (fun n => (/ 2) ^ n) 0
- forall Un, Cauchy_crit Un -> {l : R| Un_cv Un l}

As far as I know, it is easy to show that (/ 2) ^ n converges to 0 using
constructive analysis, and Cauchy's criterion is the intuitionistic
definition of real number, so it should be constructivist.

Even more, we just need to prove that the binary notation of real
numbers converges, which seems quite natural.

I join the proof to the mail, if someone is interested to check.

The proof goes like the one of the article, using the dyadic rational
numbers to associate real numbers to sequences nat -> bool : we get that
way a function phi : (nat -> bool) -> R (more precisely into [0;1]).

We show then that : forall Un, (phi Un = 0) -> (forall n, Un n = false)
like in the article.

Then we use a stronger property : from the fact that (phi Un <> 0) we
extract a (N : nat) such that (phi Un > (/ 2) ^ N), and by construction
we get a property on a subset of nat bounded by N :

~ (forall n, n <= N -> (Un n = false))

because the weight of the remainder is less than (/ 2) ^ N.

That way we only get a finite subset of nat to explore, and we can
extract a witness of the existence of a n <= N such that Un n <> false.

I don't know if this helps, and even if this doesn't use somewhere a
classical principle (although I don't think so).

Pierre-Marie Pédrot

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 Bn_pos : forall 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; fourier.
    fourier.
Qed.

Lemma Bn_growing : forall n, (Bn n) <= (Bn (S n)).
Proof.
intros n; induction n; simpl.
unfold fp; destruct f.
  apply Rplus_le_le_0_compat.
    fourier.
    apply pow_le; fourier.
    fourier.
unfold fp.
assert (H : 0 <= (/2) ^ (S (S n))).
  apply pow_le; fourier.
do 2 destruct f; fourier.
Qed.

Lemma Bn_dist : forall n, R_dist (Bn n) (Bn (S n)) <= (/ 2) ^ (S n).
Proof.
intros n; simpl Bn.
unfold R_dist.
replace (Bn n - (Bn n + fp (f n) n))
  with (- fp (f n) n) by field.
rewrite Rabs_Ropp.
assert (Hp : 0 <= (/ 2) ^ (S n)).
  apply pow_le; fourier.
assert (Hq : 0 <= (/ 2) ^ n).
  apply pow_le; fourier.
unfold fp; destruct f; rewrite Rabs_right; simpl; fourier.
Qed.

Lemma Bn_dist_trans : forall n N, R_dist (Bn n) (Bn (N + n)) <= (/ 2) ^ n * (1 - (/ 2) ^ N).
Proof.
intros n N.
induction N.
  simpl.
  unfold Rminus; rewrite Rplus_opp_r.
  rewrite Rmult_0_r.
  rewrite R_dist_eq.
  apply Rle_refl.
  simpl plus.
  unfold R_dist.
  replace (Bn n - Bn (S (N + n)))
    with (Bn n - Bn (N + n) + (Bn (N + n) - Bn (S (N + n))))
    by field.
  eapply Rle_trans; [apply Rabs_triang|].
  eapply Rle_trans.
    apply Rplus_le_compat.
      apply IHN.
      apply Bn_dist.
  repeat rewrite <- tech_pow_Rmult.
  rewrite pow_add.
  right; field.
Qed.

Lemma Bn_maj : forall n, Bn n <= 1.
Proof.
intros n.
pattern (Bn n) at 1.
rewrite <- Rabs_right; [|apply Rle_ge; apply Bn_pos].
replace (Bn n) with (Bn n - 0) by field.
replace 0 with (Bn 0) by reflexivity.
replace n with (n + 0)%nat by ring.
rewrite Rabs_minus_sym.
eapply Rle_trans.
  apply Bn_dist_trans.
  simpl; rewrite <- Rmult_1_r.
  apply Rmult_le_compat_l; [fourier|].
  rewrite <- Rminus_0_r.
  apply Rplus_le_compat_l.
  apply Ropp_le_contravar.
  apply pow_le; fourier.
Qed.

Lemma Bn_cauchy : Cauchy_crit Bn.
Proof.
intros eps Heps.
assert (H : forall n, (/ 2) ^ n <= 1).
  intros n; induction n; simpl; fourier.
destruct (pow_lt_1_zero (/2)) with (eps / 2) as [N HN].
  rewrite Rabs_right; [fourier|fourier].
  fourier.
exists N; intros n m Hn Hm.
eapply Rle_lt_trans.
  apply R_dist_tri with (z := Bn N).
replace eps with (eps / 2 + eps / 2) by field.
replace n with ((n - N) + N)%nat by omega.
replace m with ((m - N) + N)%nat by omega.
apply Rplus_lt_compat; [rewrite R_dist_sym|].
  eapply Rle_lt_trans.
    apply Bn_dist_trans.
  eapply Rle_lt_trans; [|apply (HN N); constructor].
  rewrite Rabs_right; [|apply Rle_ge; apply pow_le; fourier].
  rewrite <- Rmult_1_r.
  apply Rmult_le_compat_l.
    apply pow_le; fourier.
    rewrite <- Rminus_0_r.
    apply Rplus_le_compat_l.
    apply Ropp_le_contravar.
    apply pow_le; fourier.
  eapply Rle_lt_trans.
    apply Bn_dist_trans.
  eapply Rle_lt_trans; [|apply (HN N); constructor].
  rewrite Rabs_right; [|apply Rle_ge; apply pow_le; fourier].
  rewrite <- Rmult_1_r.
  apply Rmult_le_compat_l.
    apply pow_le; fourier.
    rewrite <- Rminus_0_r.
    apply Rplus_le_compat_l.
    apply Ropp_le_contravar.
    apply pow_le; fourier.
Qed.

Lemma Bn_cv : { l | Un_cv Bn l }.
Proof.
apply R_complete.
apply Bn_cauchy.
Qed.

Definition l := proj1_sig Bn_cv.
Definition Hlim := proj2_sig Bn_cv.

Lemma Rabs_le_maj : forall 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 l_maj : forall n, Bn n <= l.
Proof.
intros n.
apply le_epsilon; intros eps Heps.
destruct (Hlim eps) as [N HN]; [assumption|].
destruct (le_gt_dec N n) as [Hd|Hd].
  apply Rabs_le_maj.
  left; apply HN; assumption.
  assert (H : (exists p, N = p + n)%nat).
    exists (N - n)%nat; omega.
  destruct H as [p Hp].
  eapply Rle_trans with (Bn N).
    rewrite Hp; clear Hp.
    induction p.
      simpl; apply Rle_refl.
      simpl plus.
      eapply Rle_trans with (Bn (p + n)).
        assumption.
        apply Bn_growing.
    apply Rabs_le_maj.
    left; apply HN; constructor.
Qed.

Lemma Bn_l_dist : forall n, R_dist (Bn n) l <= (/2) ^ n.
Proof.
intros n.
apply le_epsilon; intros eps Heps.
destruct (Hlim eps) as [N HN]; [assumption|].
eapply Rle_trans.
  apply R_dist_tri with (z := Bn (Max.max n N)).
  apply Rplus_le_compat.
  destruct (le_ge_dec n N) as [He|He].
    rewrite Max.max_r; [|assumption].
    replace N with ((N - n) + n)%nat by omega.
    eapply Rle_trans.
      apply Bn_dist_trans.
      rewrite <- Rmult_1_r.
      apply Rmult_le_compat_l; [apply pow_le; fourier|].
      rewrite <- Rminus_0_r.
      apply Rplus_le_compat_l.
      apply Ropp_le_contravar.
      apply pow_le; fourier.
    rewrite Max.max_l; [|assumption].
    rewrite R_dist_eq; apply pow_le; fourier.
  left; apply HN; apply Max.le_max_r.
Qed.

Lemma l_partial : forall N, (forall n, (n <= N)%nat -> f n = false) -> l <= (/2) ^ N.
Proof.
intros N HN.
assert (forall 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.
      field.
assert (Hd : Bn N = 0); [apply H; constructor|].
eapply Rle_trans.
  apply RRle_abs.
  replace l with (l - Bn N) by (rewrite Hd; field).
  rewrite Rabs_minus_sym.
  apply Bn_l_dist.
Qed.

Section l_is_zero.

Hypothesis Hl : l = 0.

Lemma l_R0 : forall n, f n = false.
Proof.
assert (H : forall 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; fourier.
    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 : (/ 2) ^ S (S n) <> 0).
      apply pow_nonzero; apply Rgt_not_eq; fourier.
    contradiction.
    reflexivity.
Qed.

End l_is_zero.

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 : exists N, ~(forall n, (n <= N)%nat -> f n = false).
Proof.
assert (Hlt : l > 0); [apply Hl_lt_0|].
assert (HN : exists N, forall n, (n >= N)%nat -> (/ 2) ^ n < l).
  destruct (pow_lt_1_zero (/2)) with l as [N HN].
  rewrite Rabs_right; fourier.
  fourier.
  exists 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].
exists 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 : exists n, f n <> false.
Proof.
destruct l_not_R0_partial as [N HN].
induction N.
  exists 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].
    exists (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 : forall n, {P n} + {~ P n}.

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

Lemma Heq1 : forall 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 : forall 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 : ~ (forall n, P n) -> exists 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.
exists N; apply Heq1; assumption.
Qed.

Theorem R_sequence_dec : {forall n, P n} + {~ forall n, P n}.
Proof.
destruct (total_order_T (l f) 0) as [[Hlt|Heq]|Hgt].
  apply Rlt_not_eq in Hlt; right.
  destruct (l_not_R0 f) as [N HN]; [assumption|].
    intros Hneg; apply HN.
    destruct (Heq1 N); [assumption|apply Hneg].
  left; intros n.
  destruct (P_dec n) as [Hd|Hd]; [assumption|].
  apply l_R0 with (n := n) in Heq.
  apply Heq2 in Heq.
  contradiction.
  apply Rgt_not_eq in Hgt; right.
  destruct (l_not_R0 f) as [N HN]; [assumption|].
    intros Hneg; apply HN.
    destruct (Heq1 N); [assumption|apply Hneg].
Qed.

End Markov.

[roconnor]

On Sun, 1 Nov 2009, Pierre-Marie Pédrot wrote:

> I am unsure about the classical properties used; yet I don't think this
> is the case, as long as the two extern lemmas thereafter are
> intuitionnistic:

Running the two commands

Print Assumptions R_sequence_dec.

and

Print Assumptions forall_dec.

show that they depend on identical axioms.  In particular they both use:
Classical_Prop.classic : forall P : Prop, P \/ ~ P

> - forall Un, Cauchy_crit Un -> {l : R| Un_cv Un l}

This appears to be the first place the classic axiom is introduced.
Bn_cv uses R_complete, and R_complete depends on classic (possibly
indirectly).  I haven't looked at the proof of R_complete, so I don't know
if the axiom can be removed.

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''

[Pierre-Marie Pédrot]

roconnor@... a écrit :
> This appears to be the first place the classic axiom is introduced.
> Bn_cv uses R_complete, and R_complete depends on classic (possibly
> indirectly).  I haven't looked at the proof of R_complete, so I don't
> know if the axiom can be removed.

I have rewritten the proof of the convergence of Bn, and it does not use
the classical axiom anymore. This was the only part where excluded
middle was used, according to the Print Assumptions command.

Quite strangely, I believe that the proof of Markov's principle could
get rid of the axiom of trichotomy, because I only use it in the
definition of Rabs, and the proof only works on nonnegative numbers.

I have the feeling that the classical axiomatization of Coq minus the
axiom of trichotomy substly implies something like :

forall r : R, r <> 0 -> r # 0

which is equivalent to, up to a good isomophism,

forall P : nat -> bool, ~ (forall n, P n = false) -> exists n, ~ (P n =
false)

that is to say, the principle of Markov.

What do you think about that ?

Cordially,
Pierre-Marie Pédrot

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 Bn_pos : forall 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; fourier.
    fourier.
Qed.

Lemma Bn_growing : forall n, (Bn n) <= (Bn (S n)).
Proof.
intros n; induction n; simpl.
unfold fp; destruct f.
  apply Rplus_le_le_0_compat.
    fourier.
    apply pow_le; fourier.
    fourier.
unfold fp.
assert (H : 0 <= (/2) ^ (S (S n))).
  apply pow_le; fourier.
do 2 destruct f; fourier.
Qed.

Lemma Bn_growing_trans : forall 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 : forall n, R_dist (Bn n) (Bn (S n)) <= (/ 2) ^ (S n).
Proof.
intros n; simpl Bn.
unfold R_dist.
replace (Bn n - (Bn n + fp (f n) n))
  with (- fp (f n) n) by field.
rewrite Rabs_Ropp.
assert (Hp : 0 <= (/ 2) ^ (S n)).
  apply pow_le; fourier.
assert (Hq : 0 <= (/ 2) ^ n).
  apply pow_le; fourier.
unfold fp; destruct f; rewrite Rabs_right; simpl; fourier.
Qed.

Lemma Bn_dist_trans : forall n N, R_dist (Bn n) (Bn (N + n)) <= (/ 2) ^ n * (1 - (/ 2) ^ N).
Proof.
intros n N.
induction N.
  simpl.
  unfold Rminus; rewrite Rplus_opp_r.
  rewrite Rmult_0_r.
  rewrite R_dist_eq.
  apply Rle_refl.
  simpl plus.
  unfold R_dist.
  replace (Bn n - Bn (S (N + n)))
    with (Bn n - Bn (N + n) + (Bn (N + n) - Bn (S (N + n))))
    by field.
  eapply Rle_trans; [apply Rabs_triang|].
  eapply Rle_trans.
    apply Rplus_le_compat.
      apply IHN.
      apply Bn_dist.
  repeat rewrite <- tech_pow_Rmult.
  rewrite pow_add.
  right; field.
Qed.

Lemma Bn_maj : forall n, Bn n <= 1.
Proof.
intros n.
pattern (Bn n) at 1.
rewrite <- Rabs_right; [|apply Rle_ge; apply Bn_pos].
replace (Bn n) with (Bn n - 0) by field.
replace 0 with (Bn 0) by reflexivity.
replace n with (n + 0)%nat by ring.
rewrite Rabs_minus_sym.
eapply Rle_trans.
  apply Bn_dist_trans.
  simpl; rewrite <- Rmult_1_r.
  apply Rmult_le_compat_l; [fourier|].
  rewrite <- Rminus_0_r.
  apply Rplus_le_compat_l.
  apply Ropp_le_contravar.
  apply pow_le; fourier.
Qed.

Lemma Bn_cauchy : Cauchy_crit Bn.
Proof.
intros eps Heps.
assert (H : forall n, (/ 2) ^ n <= 1).
  intros n; induction n; simpl; fourier.
destruct (pow_lt_1_zero (/2)) with (eps / 2) as [N HN].
  rewrite Rabs_right; [fourier|fourier].
  fourier.
exists N; intros n m Hn Hm.
eapply Rle_lt_trans.
  apply R_dist_tri with (z := Bn N).
replace eps with (eps / 2 + eps / 2) by field.
replace n with ((n - N) + N)%nat by omega.
replace m with ((m - N) + N)%nat by omega.
apply Rplus_lt_compat; [rewrite R_dist_sym|].
  eapply Rle_lt_trans.
    apply Bn_dist_trans.
  eapply Rle_lt_trans; [|apply (HN N); constructor].
  rewrite Rabs_right; [|apply Rle_ge; apply pow_le; fourier].
  rewrite <- Rmult_1_r.
  apply Rmult_le_compat_l.
    apply pow_le; fourier.
    rewrite <- Rminus_0_r.
    apply Rplus_le_compat_l.
    apply Ropp_le_contravar.
    apply pow_le; fourier.
  eapply Rle_lt_trans.
    apply Bn_dist_trans.
  eapply Rle_lt_trans; [|apply (HN N); constructor].
  rewrite Rabs_right; [|apply Rle_ge; apply pow_le; fourier].
  rewrite <- Rmult_1_r.
  apply Rmult_le_compat_l.
    apply pow_le; fourier.
    rewrite <- Rminus_0_r.
    apply Rplus_le_compat_l.
    apply Ropp_le_contravar.
    apply pow_le; fourier.
Qed.

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

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

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

Lemma l_maj : forall n, Bn n <= l.
Proof.
intros n.
destruct Hlub as [Hb _].
apply Hb.
exists n; reflexivity.
Qed.

Lemma l_lub : forall M, (forall 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 Hlim : Un_cv Bn l.
Proof.
intros eps Heps.
destruct (pow_lt_1_zero (/ 2)) with eps as [N HN].
  rewrite Rabs_right; fourier.
  assumption.
exists N; intros n Hn.
unfold R_dist.
eapply Rle_lt_trans; [|apply HN; constructor].
pattern Rabs at 1.
rewrite Rabs_right; [|apply Rle_ge; apply pow_le; fourier].
rewrite Rabs_left1; [|apply Rle_minus; apply l_maj].
unfold Rminus; rewrite Ropp_plus_distr; rewrite Ropp_involutive.
rewrite <- Rplus_0_l.
replace 0 with (- Bn n + Bn n) by field.
rewrite Rplus_assoc.
apply Rplus_le_compat_l.
assert (H : Bn N + (/ 2) ^ N <= Bn n + (/ 2) ^ N).
  apply Rplus_le_compat_r.
  replace n with ((n - N) + N)%nat by omega.
  apply Bn_growing_trans.
eapply Rle_trans; [|eexact H].
clear Hn H Heps HN eps n.
apply l_lub; intros n.
destruct (le_ge_dec n N) as [Hd|Hd].
  pattern (Bn n); rewrite <- Rplus_0_r.
  apply Rplus_le_compat.
    replace N with ((N - n) + n)%nat by omega.
    apply Bn_growing_trans.
    apply pow_le; fourier.
  replace (Bn n) with (Bn N + (Bn n - Bn N)) by field.
  apply Rplus_le_compat_l.
  replace n with ((n - N) + N)%nat by omega.
  pattern (Bn (n - N + N) - Bn N).
  rewrite <- Rabs_right.
  eapply Rle_trans.
    rewrite Rabs_minus_sym.
    apply Bn_dist_trans.
    rewrite <- Rmult_1_r.
    apply Rmult_le_compat_l.
      apply pow_le; fourier.
      rewrite <- Rminus_0_r.
      apply Rplus_le_compat_l.
      apply Ropp_le_contravar.
      apply pow_le; fourier.
  apply Rge_minus; apply Rle_ge.
  apply Bn_growing_trans.
Qed.

Lemma Rabs_le_maj : forall 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 : forall n, R_dist (Bn n) l <= (/2) ^ n.
Proof.
intros n.
apply le_epsilon; intros eps Heps.
destruct (Hlim eps) as [N HN]; [assumption|].
eapply Rle_trans.
  apply R_dist_tri with (z := Bn (Max.max n N)).
  apply Rplus_le_compat.
  destruct (le_ge_dec n N) as [He|He].
    rewrite Max.max_r; [|assumption].
    replace N with ((N - n) + n)%nat by omega.
    eapply Rle_trans.
      apply Bn_dist_trans.
      rewrite <- Rmult_1_r.
      apply Rmult_le_compat_l; [apply pow_le; fourier|].
      rewrite <- Rminus_0_r.
      apply Rplus_le_compat_l.
      apply Ropp_le_contravar.
      apply pow_le; fourier.
    rewrite Max.max_l; [|assumption].
    rewrite R_dist_eq; apply pow_le; fourier.
  left; apply HN; apply Max.le_max_r.
Qed.

Lemma l_partial : forall N, (forall n, (n <= N)%nat -> f n = false) -> l <= (/2) ^ N.
Proof.
intros N HN.
assert (forall 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.
      field.
assert (Hd : Bn N = 0); [apply H; constructor|].
eapply Rle_trans.
  apply RRle_abs.
  replace l with (l - Bn N) by (rewrite Hd; field).
  rewrite Rabs_minus_sym.
  apply Bn_l_dist.
Qed.

Section l_is_zero.

Hypothesis Hl : l = 0.

Lemma l_R0 : forall n, f n = false.
Proof.
assert (H : forall 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; fourier.
    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 : (/ 2) ^ S (S n) <> 0).
      apply pow_nonzero; apply Rgt_not_eq; fourier.
    contradiction.
    reflexivity.
Qed.

End l_is_zero.

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 : exists N, ~(forall n, (n <= N)%nat -> f n = false).
Proof.
assert (Hlt : l > 0); [apply Hl_lt_0|].
assert (HN : exists N, forall n, (n >= N)%nat -> (/ 2) ^ n < l).
  destruct (pow_lt_1_zero (/2)) with l as [N HN].
  rewrite Rabs_right; fourier.
  fourier.
  exists 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].
exists 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 : exists n, f n <> false.
Proof.
destruct l_not_R0_partial as [N HN].
induction N.
  exists 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].
    exists (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 : forall n, {P n} + {~ P n}.

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

Lemma Heq1 : forall 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 : forall 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 : ~ (forall n, P n) -> exists 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.
exists N; apply Heq1; assumption.
Qed.

Theorem R_sequence_dec : {forall n, P n} + {~ forall n, P n}.
Proof.
destruct (total_order_T (l f) 0) as [[Hlt|Heq]|Hgt].
  apply Rlt_not_eq in Hlt; right.
  destruct (l_not_R0 f) as [N HN]; [assumption|].
    intros Hneg; apply HN.
    destruct (Heq1 N); [assumption|apply Hneg].
  left; intros n.
  destruct (P_dec n) as [Hd|Hd]; [assumption|].
  apply l_R0 with (n := n) in Heq.
  apply Heq2 in Heq.
  contradiction.
  apply Rgt_not_eq in Hgt; right.
  destruct (l_not_R0 f) as [N HN]; [assumption|].
    intros Hneg; apply HN.
    destruct (Heq1 N); [assumption|apply Hneg].
Qed.

End Markov.

[Bas Spitters-3]

A version of Markov's principle is provable in Coq.

I seem to recall that it was in cocorico, but I cannot find it currently.
You can find a discussion on Russell's blog:
http://r6research.livejournal.com/

Bas

2009/11/1 Pierre-Marie Pédrot <pierremarie.pedrot@...>

I have the feeling that the classical axiomatization of Coq minus the
axiom of trichotomy substly implies something like :

forall r : R, r <> 0 -> r # 0

which is equivalent to, up to a good isomophism,

forall P : nat -> bool, ~ (forall n, P n = false) -> exists n, ~ (P n =
false)

that is to say, the principle of Markov.

What do you think about that ?

Cordially,
Pierre-Marie Pédrot

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 Bn_pos : forall 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; fourier.
   fourier.
Qed.

Lemma Bn_growing : forall n, (Bn n) <= (Bn (S n)).
Proof.
intros n; induction n; simpl.
unfold fp; destruct f.
 apply Rplus_le_le_0_compat.
   fourier.
   apply pow_le; fourier.
   fourier.
unfold fp.
assert (H : 0 <= (/2) ^ (S (S n))).
 apply pow_le; fourier.
do 2 destruct f; fourier.
Qed.

Lemma Bn_growing_trans : forall 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 : forall n, R_dist (Bn n) (Bn (S n)) <= (/ 2) ^ (S n).
Proof.
intros n; simpl Bn.
unfold R_dist.
replace (Bn n - (Bn n + fp (f n) n))
 with (- fp (f n) n) by field.
rewrite Rabs_Ropp.
assert (Hp : 0 <= (/ 2) ^ (S n)).
 apply pow_le; fourier.
assert (Hq : 0 <= (/ 2) ^ n).
 apply pow_le; fourier.
unfold fp; destruct f; rewrite Rabs_right; simpl; fourier.
Qed.

Lemma Bn_dist_trans : forall n N, R_dist (Bn n) (Bn (N + n)) <= (/ 2) ^ n * (1 - (/ 2) ^ N).
Proof.
intros n N.
induction N.
 simpl.
 unfold Rminus; rewrite Rplus_opp_r.
 rewrite Rmult_0_r.
 rewrite R_dist_eq.
 apply Rle_refl.
 simpl plus.
 unfold R_dist.
 replace (Bn n - Bn (S (N + n)))
   with (Bn n - Bn (N + n) + (Bn (N + n) - Bn (S (N + n))))
   by field.
 eapply Rle_trans; [apply Rabs_triang|].
 eapply Rle_trans.
   apply Rplus_le_compat.
     apply IHN.
     apply Bn_dist.
 repeat rewrite <- tech_pow_Rmult.
 rewrite pow_add.
 right; field.
Qed.

Lemma Bn_maj : forall n, Bn n <= 1.
Proof.
intros n.
pattern (Bn n) at 1.
rewrite <- Rabs_right; [|apply Rle_ge; apply Bn_pos].
replace (Bn n) with (Bn n - 0) by field.
replace 0 with (Bn 0) by reflexivity.
replace n with (n + 0)%nat by ring.
rewrite Rabs_minus_sym.
eapply Rle_trans.
 apply Bn_dist_trans.
 simpl; rewrite <- Rmult_1_r.
 apply Rmult_le_compat_l; [fourier|].
 rewrite <- Rminus_0_r.
 apply Rplus_le_compat_l.
 apply Ropp_le_contravar.
 apply pow_le; fourier.
Qed.

Lemma Bn_cauchy : Cauchy_crit Bn.
Proof.
intros eps Heps.
assert (H : forall n, (/ 2) ^ n <= 1).
 intros n; induction n; simpl; fourier.
destruct (pow_lt_1_zero (/2)) with (eps / 2) as [N HN].
 rewrite Rabs_right; [fourier|fourier].
 fourier.
exists N; intros n m Hn Hm.
eapply Rle_lt_trans.
 apply R_dist_tri with (z := Bn N).
replace eps with (eps / 2 + eps / 2) by field.
replace n with ((n - N) + N)%nat by omega.
replace m with ((m - N) + N)%nat by omega.
apply Rplus_lt_compat; [rewrite R_dist_sym|].
 eapply Rle_lt_trans.
   apply Bn_dist_trans.
 eapply Rle_lt_trans; [|apply (HN N); constructor].
 rewrite Rabs_right; [|apply Rle_ge; apply pow_le; fourier].
 rewrite <- Rmult_1_r.
 apply Rmult_le_compat_l.
   apply pow_le; fourier.
   rewrite <- Rminus_0_r.
   apply Rplus_le_compat_l.
   apply Ropp_le_contravar.
   apply pow_le; fourier.
 eapply Rle_lt_trans.
   apply Bn_dist_trans.
 eapply Rle_lt_trans; [|apply (HN N); constructor].
 rewrite Rabs_right; [|apply Rle_ge; apply pow_le; fourier].
 rewrite <- Rmult_1_r.
 apply Rmult_le_compat_l.
   apply pow_le; fourier.
   rewrite <- Rminus_0_r.
   apply Rplus_le_compat_l.
   apply Ropp_le_contravar.
   apply pow_le; fourier.
Qed.

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

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

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

Lemma l_maj : forall n, Bn n <= l.
Proof.
intros n.
destruct Hlub as [Hb _].
apply Hb.
exists n; reflexivity.
Qed.

Lemma l_lub : forall M, (forall 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 Hlim : Un_cv Bn l.
Proof.
intros eps Heps.
destruct (pow_lt_1_zero (/ 2)) with eps as [N HN].
 rewrite Rabs_right; fourier.
 assumption.
exists N; intros n Hn.
unfold R_dist.
eapply Rle_lt_trans; [|apply HN; constructor].
pattern Rabs at 1.
rewrite Rabs_right; [|apply Rle_ge; apply pow_le; fourier].
rewrite Rabs_left1; [|apply Rle_minus; apply l_maj].
unfold Rminus; rewrite Ropp_plus_distr; rewrite Ropp_involutive.
rewrite <- Rplus_0_l.
replace 0 with (- Bn n + Bn n) by field.
rewrite Rplus_assoc.
apply Rplus_le_compat_l.
assert (H : Bn N + (/ 2) ^ N <= Bn n + (/ 2) ^ N).
 apply Rplus_le_compat_r.
 replace n with ((n - N) + N)%nat by omega.
 apply Bn_growing_trans.
eapply Rle_trans; [|eexact H].
clear Hn H Heps HN eps n.
apply l_lub; intros n.
destruct (le_ge_dec n N) as [Hd|Hd].
 pattern (Bn n); rewrite <- Rplus_0_r.
 apply Rplus_le_compat.
   replace N with ((N - n) + n)%nat by omega.
   apply Bn_growing_trans.
   apply pow_le; fourier.
 replace (Bn n) with (Bn N + (Bn n - Bn N)) by field.
 apply Rplus_le_compat_l.
 replace n with ((n - N) + N)%nat by omega.
 pattern (Bn (n - N + N) - Bn N).
 rewrite <- Rabs_right.
 eapply Rle_trans.
   rewrite Rabs_minus_sym.
   apply Bn_dist_trans.
   rewrite <- Rmult_1_r.
   apply Rmult_le_compat_l.
     apply pow_le; fourier.
     rewrite <- Rminus_0_r.
     apply Rplus_le_compat_l.
     apply Ropp_le_contravar.
     apply pow_le; fourier.
 apply Rge_minus; apply Rle_ge.
 apply Bn_growing_trans.
Qed.

Lemma Rabs_le_maj : forall 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 : forall n, R_dist (Bn n) l <= (/2) ^ n.
Proof.
intros n.
apply le_epsilon; intros eps Heps.
destruct (Hlim eps) as [N HN]; [assumption|].
eapply Rle_trans.
 apply R_dist_tri with (z := Bn (Max.max n N)).
 apply Rplus_le_compat.
 destruct (le_ge_dec n N) as [He|He].
   rewrite Max.max_r; [|assumption].
   replace N with ((N - n) + n)%nat by omega.
   eapply Rle_trans.
     apply Bn_dist_trans.
     rewrite <- Rmult_1_r.
     apply Rmult_le_compat_l; [apply pow_le; fourier|].
     rewrite <- Rminus_0_r.
     apply Rplus_le_compat_l.
     apply Ropp_le_contravar.
     apply pow_le; fourier.
   rewrite Max.max_l; [|assumption].
   rewrite R_dist_eq; apply pow_le; fourier.
 left; apply HN; apply Max.le_max_r.
Qed.

Lemma l_partial : forall N, (forall n, (n <= N)%nat -> f n = false) -> l <= (/2) ^ N.
Proof.
intros N HN.
assert (forall 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.
     field.
assert (Hd : Bn N = 0); [apply H; constructor|].
eapply Rle_trans.
 apply RRle_abs.
 replace l with (l - Bn N) by (rewrite Hd; field).
 rewrite Rabs_minus_sym.
 apply Bn_l_dist.
Qed.

Section l_is_zero.

Hypothesis Hl : l = 0.

Lemma l_R0 : forall n, f n = false.
Proof.
assert (H : forall 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; fourier.
   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 : (/ 2) ^ S (S n) <> 0).
     apply pow_nonzero; apply Rgt_not_eq; fourier.
   contradiction.
   reflexivity.
Qed.

End l_is_zero.

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 : exists N, ~(forall n, (n <= N)%nat -> f n = false).
Proof.
assert (Hlt : l > 0); [apply Hl_lt_0|].
assert (HN : exists N, forall n, (n >= N)%nat -> (/ 2) ^ n < l).
 destruct (pow_lt_1_zero (/2)) with l as [N HN].
 rewrite Rabs_right; fourier.
 fourier.
 exists 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].
exists 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 : exists n, f n <> false.
Proof.
destruct l_not_R0_partial as [N HN].
induction N.
 exists 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].
   exists (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 : forall n, {P n} + {~ P n}.

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

Lemma Heq1 : forall 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 : forall 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 : ~ (forall n, P n) -> exists 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.
exists N; apply Heq1; assumption.
Qed.

Theorem R_sequence_dec : {forall n, P n} + {~ forall n, P n}.
Proof.
destruct (total_order_T (l f) 0) as [[Hlt|Heq]|Hgt].
 apply Rlt_not_eq in Hlt; right.
 destruct (l_not_R0 f) as [N HN]; [assumption|].
   intros Hneg; apply HN.
   destruct (Heq1 N); [assumption|apply Hneg].
 left; intros n.
 destruct (P_dec n) as [Hd|Hd]; [assumption|].
 apply l_R0 with (n := n) in Heq.
 apply Heq2 in Heq.
 contradiction.
 apply Rgt_not_eq in Hgt; right.
 destruct (l_not_R0 f) as [N HN]; [assumption|].
   intros Hneg; apply HN.
   destruct (Heq1 N); [assumption|apply Hneg].
Qed.

End Markov.