The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

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.