Timings for ConstructiveLUB.v
- /home/gitlab-runner/builds/v6HyzL39/0/coq/coq/_bench/opam.OLD/ocaml-OLD/.opam-switch/build/coq-stdlib.dev/_build/default/theories//./Reals/Abstract/ConstructiveLUB.timing
- /home/gitlab-runner/builds/v6HyzL39/0/coq/coq/_bench/opam.NEW/ocaml-NEW/.opam-switch/build/coq-stdlib.dev/_build/default/theories//./Reals/Abstract/ConstructiveLUB.timing
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(************************************************************************)
(** Proof that LPO and the excluded middle for negations imply
the existence of least upper bounds for all non-empty and bounded
subsets of the real numbers.
WARNING: this file is experimental and likely to change in future releases.
*)
Require Import QArith_base Qabs.
Require Import ConstructiveReals.
Require Import ConstructiveAbs.
Require Import ConstructiveLimits.
Require Import Logic.ConstructiveEpsilon.
Local Open Scope ConstructiveReals.
Definition sig_forall_dec_T : Type
:= forall (P : nat -> Prop), (forall n, {P n} + {~P n})
-> {n | ~P n} + {forall n, P n}.
Definition sig_not_dec_T : Type := forall P : Prop, { ~~P } + { ~P }.
Definition is_upper_bound {R : ConstructiveReals}
(E:CRcarrier R -> Prop) (m:CRcarrier R)
:= forall x:CRcarrier R, E x -> x <= m.
Definition is_lub {R : ConstructiveReals}
(E:CRcarrier R -> Prop) (m:CRcarrier R) :=
is_upper_bound E m /\ (forall b:CRcarrier R, is_upper_bound E b -> m <= b).
Lemma CRlt_lpo_dec : forall {R : ConstructiveReals} (x y : CRcarrier R),
(forall (P : nat -> Prop), (forall n, {P n} + {~P n})
-> {n | ~P n} + {forall n, P n})
-> sum (x < y) (y <= x).
assert (forall (z:CRcarrier R) (n : nat), z < z + CR_of_Q R (1 # Pos.of_nat (S n))).
apply (CRle_lt_trans _ (z+0)).
apply CRplus_lt_compat_l.
pose (fun n:nat => let (q,_) := CR_Q_dense
R x (x + CR_of_Q R (1 # Pos.of_nat (S n))) (H x n)
in q)
as xn.
pose (fun n:nat => let (q,_) := CR_Q_dense
R y (y + CR_of_Q R (1 # Pos.of_nat (S n))) (H y n)
in q)
as yn.
destruct (lpo (fun n => Qle (yn n) (xn n + (1 # Pos.of_nat (S n))))).
destruct (Q_dec (yn n) (xn n + (1 # Pos.of_nat (S n)))).
apply (Qlt_not_le _ _ q).
apply Qnot_le_lt in nmaj.
apply (CRlt_le_trans _ (CR_of_Q R (xn n))).
destruct (CR_Q_dense R x (x + CR_of_Q R (1 # Pos.of_nat (S n))) (H x n)).
apply (CRle_trans _ (CR_of_Q R (yn n - (1 # Pos.of_nat (S n))))).
rewrite <- (Qplus_le_l _ _ (1# Pos.of_nat (S n))).
destruct (CR_Q_dense R y (y + CR_of_Q R (1 # Pos.of_nat (S n))) (H y n)).
rewrite CR_of_Q_plus, CR_of_Q_opp.
apply (CRplus_le_reg_r (CR_of_Q R (1 # Pos.of_nat (S n)))).
rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r.
apply CRlt_asym, (snd p).
apply (CR_cv_le (fun n => CR_of_Q R (yn n))
(fun n => CR_of_Q R (xn n) + CR_of_Q R (1 # Pos.of_nat (S n)))).
destruct (CR_Q_dense R y (y + CR_of_Q R (1 # Pos.of_nat (S i))) (H y i)).
apply (CRplus_le_reg_r y).
rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r.
apply (CRle_trans _ (y + CR_of_Q R (1 # Pos.of_nat (S i)))).
apply CRlt_asym, (snd p0).
apply CRplus_le_compat_l.
rewrite Z.mul_1_l, Z.mul_1_l.
rewrite <- (CRplus_opp_r y).
apply CRplus_le_compat_r, CRlt_asym, p0.
apply (CR_cv_proper _ (x+0)).
2: rewrite CRplus_0_r; reflexivity.
destruct (CR_Q_dense R x (x + CR_of_Q R (1 # Pos.of_nat (S i))) (H x i)).
apply (CRplus_le_reg_r x).
rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r.
apply (CRle_trans _ (x + CR_of_Q R (1 # Pos.of_nat (S i)))).
apply CRlt_asym, (snd p0).
apply CRplus_le_compat_l.
rewrite Z.mul_1_l, Z.mul_1_l.
rewrite <- (CRplus_opp_r x).
apply CRplus_le_compat_r, CRlt_asym, p0.
rewrite CRopp_0, CRplus_0_r, CRabs_right.
rewrite Z.mul_1_l, Z.mul_1_l.
Lemma is_upper_bound_dec :
forall {R : ConstructiveReals} (E:CRcarrier R -> Prop) (x:CRcarrier R),
sig_forall_dec_T
-> sig_not_dec_T
-> { is_upper_bound E x } + { ~is_upper_bound E x }.
intros R E x lpo sig_not_dec.
destruct (sig_not_dec (~exists y:CRcarrier R, E y /\ CRltProp R x y)).
destruct (CRlt_lpo_dec x y lpo).
Lemma is_upper_bound_epsilon :
forall {R : ConstructiveReals} (E:CRcarrier R -> Prop),
sig_forall_dec_T
-> sig_not_dec_T
-> (exists x:CRcarrier R, is_upper_bound E x)
-> { n:nat | is_upper_bound E (CR_of_Q R (Z.of_nat n # 1)) }.
intros R E lpo sig_not_dec Ebound.
apply constructive_indefinite_ground_description_nat.
apply is_upper_bound_dec.
destruct Ebound as [x H].
destruct (CRup_nat x) as [n nmaj].
apply (CRle_trans _ x _ H).
Lemma is_upper_bound_not_epsilon :
forall {R : ConstructiveReals} (E:CRcarrier R -> Prop),
sig_forall_dec_T
-> sig_not_dec_T
-> (exists x : CRcarrier R, E x)
-> { m:nat | ~is_upper_bound E (-CR_of_Q R (Z.of_nat m # 1)) }.
intros R E lpo sig_not_dec H.
apply constructive_indefinite_ground_description_nat.
destruct (is_upper_bound_dec E (-CR_of_Q R (Z.of_nat n # 1)) lpo sig_not_dec).
destruct (CRup_nat (-x)) as [n H0].
rewrite <- (CRopp_involutive x).
apply CRopp_gt_lt_contravar.
(* Decidable Dedekind cuts are Cauchy reals. *)
Record DedekindDecCut : Type :=
{
DDupcut : Q -> Prop;
DDproper : forall q r : Q, (q == r -> DDupcut q -> DDupcut r)%Q;
DDlow : Q;
DDhigh : Q;
DDdec : forall q:Q, { DDupcut q } + { ~DDupcut q };
DDinterval : forall q r : Q, Qle q r -> DDupcut q -> DDupcut r;
DDhighProp : DDupcut DDhigh;
DDlowProp : ~DDupcut DDlow;
}.
Lemma DDlow_below_up : forall (upcut : DedekindDecCut) (a b : Q),
DDupcut upcut a -> ~DDupcut upcut b -> Qlt b a.
destruct (Qlt_le_dec b a).
apply (DDinterval upcut a).
Fixpoint DDcut_limit_fix (upcut : DedekindDecCut) (r : Q) (n : nat) :
Qlt 0 r
-> (DDupcut upcut (DDlow upcut + (Z.of_nat n#1) * r))
-> { q : Q | DDupcut upcut q /\ ~DDupcut upcut (q - r) }.
apply (DDproper upcut _ (DDlow upcut)) in H0.
exact (DDlowProp upcut H0).
destruct (DDdec upcut (DDlow upcut + (Z.of_nat n # 1) * r)).
exact (DDcut_limit_fix upcut r n H d).
exists (DDlow upcut + (Z.of_nat (S n) # 1) * r)%Q.
apply (DDproper upcut _ (DDlow upcut + (Z.of_nat n # 1) * r)) in abs.
rewrite <- Qinv_plus_distr.
Lemma DDcut_limit : forall (upcut : DedekindDecCut) (r : Q),
Qlt 0 r
-> { q : Q | DDupcut upcut q /\ ~DDupcut upcut (q - r) }.
destruct (Qarchimedean ((DDhigh upcut - DDlow upcut)/r)) as [n nmaj].
apply (DDcut_limit_fix upcut r (Pos.to_nat n) H).
apply (Qmult_lt_r _ _ r) in nmaj.
rewrite <- Qmult_assoc, (Qmult_comm (/r)), Qmult_inv_r, Qmult_1_r in nmaj.
apply (DDinterval upcut (DDhigh upcut)).
2: exact (DDhighProp upcut).
apply (Qplus_lt_r _ _ (-DDlow upcut)).
rewrite Qplus_assoc, <- (Qplus_comm (DDlow upcut)), Qplus_opp_r,
Qplus_0_l, Qplus_comm.
Lemma glb_dec_Q : forall {R : ConstructiveReals} (upcut : DedekindDecCut),
{ x : CRcarrier R
| forall r:Q, (x < CR_of_Q R r -> DDupcut upcut r)
/\ (CR_of_Q R r < x -> ~DDupcut upcut r) }.
assert (forall a b : Q, Qle a b -> Qle (-b) (-a)).
apply (Qplus_le_l _ _ (a+b)).
assert (CR_cauchy R (fun n:nat => CR_of_Q R (proj1_sig (DDcut_limit
upcut (1#Pos.of_nat n) (eq_refl _))))).
destruct (DDcut_limit upcut (1 # Pos.of_nat i) eq_refl),
(DDcut_limit upcut (1 # Pos.of_nat j) eq_refl); unfold proj1_sig.
rewrite <- CR_of_Q_opp, <- CR_of_Q_opp, <- CR_of_Q_plus.
apply (Qplus_le_l _ _ x0).
setoid_replace (-1 * (1 # p) + x0)%Q with (x0 - (1 # p))%Q.
apply (Qle_trans _ (x0- (1#Pos.of_nat j))).
pose proof (Pos2Nat.is_pos p).
apply Qlt_le_weak, (DDlow_below_up upcut).
rewrite <- CR_of_Q_opp, <- CR_of_Q_plus.
apply (Qplus_le_l _ _ (x0-(1#p))).
setoid_replace (x -1 * (1 # p))%Q with (x - (1 # p))%Q.
apply (Qle_trans _ (x- (1#Pos.of_nat i))).
pose proof (Pos2Nat.is_pos p).
apply Qlt_le_weak, (DDlow_below_up upcut).
(* find an upper point between the limit and r *)
destruct (CR_cv_open_above _ (CR_of_Q R r) l lcv H0) as [p pmaj].
specialize (pmaj p (Nat.le_refl p)).
unfold proj1_sig in pmaj.
destruct (DDcut_limit upcut (1 # Pos.of_nat p) eq_refl) as [q qmaj].
apply (DDinterval upcut q).
apply (CR_of_Q_lt R) in q0.
exact (CRlt_asym _ _ pmaj q0).
assert ((CR_of_Q R r+l) * CR_of_Q R (1#2) < l).
apply (CRmult_lt_reg_r (CR_of_Q R 2)).
rewrite CRmult_assoc, <- CR_of_Q_mult, (CR_of_Q_plus R 1 1).
setoid_replace ((1 # 2) * 2)%Q with 1%Q.
rewrite CRmult_plus_distr_l, CRmult_1_r, CRmult_1_r.
apply CRplus_lt_compat_r.
destruct (CR_cv_open_below _ _ l lcv H1) as [p pmaj].
assert (0 < (l-CR_of_Q R r) * CR_of_Q R (1#2)).
apply CRmult_lt_0_compat.
rewrite <- (CRplus_opp_r (CR_of_Q R r)).
apply CRplus_lt_compat_r.
destruct (CRup_nat (CRinv R _ (inr H2))) as [i imaj].
exact (CRlt_asym _ _ imaj (CRinv_0_lt_compat R _ (inr H2) H2)).
specialize (pmaj (max (S i) (S p)) (Nat.le_trans p (S p) _ (le_S p p (Nat.le_refl p)) (Nat.le_max_r (S i) (S p)))).
unfold proj1_sig in pmaj.
destruct (DDcut_limit upcut (1 # Pos.of_nat (max (S i) (S p))) eq_refl)
as [q qmaj].
apply (DDinterval upcut r).
apply (Qplus_le_l _ _ (1 # Pos.of_nat (Init.Nat.max (S i) (S p)))).
apply (Qle_trans _ (r + (1 # Pos.of_nat (S i)))).
rewrite Z.mul_1_l, Z.mul_1_l.
rewrite Nat2Pos.id, Nat2Pos.id.
apply (CRmult_lt_compat_l ((l - CR_of_Q R r) * CR_of_Q R (1 # 2))) in imaj.
destruct (Q_dec (r+(1#Pos.of_nat (S i))) q);[|rewrite q0; apply Qle_refl].
apply (CR_of_Q_lt R) in q0.
apply (CRlt_asym _ _ pmaj).
apply (CRlt_le_trans _ _ _ q0).
apply (CRplus_le_reg_l (-CR_of_Q R r)).
rewrite CR_of_Q_plus, <- CRplus_assoc, CRplus_opp_l, CRplus_0_l.
apply (CRmult_lt_compat_r (CR_of_Q R (1 # Pos.of_nat (S i)))) in imaj.
rewrite CRmult_1_l in imaj.
apply (CRle_trans _ (
(l - CR_of_Q R r) * CR_of_Q R (1 # 2) * CR_of_Q R (Z.of_nat (S i) # 1) *
CR_of_Q R (1 # Pos.of_nat (S i)))).
rewrite CRmult_assoc, <- CR_of_Q_mult.
setoid_replace ((Z.of_nat (S i) # 1) * (1 # Pos.of_nat (S i)))%Q with 1%Q.
rewrite CRmult_plus_distr_r, (CRplus_comm (-CR_of_Q R r)).
rewrite (CRplus_comm (CR_of_Q R r)), CRmult_plus_distr_r.
apply CRplus_le_compat_l.
rewrite <- CR_of_Q_mult, <- CR_of_Q_opp, <- CR_of_Q_mult, <- CR_of_Q_plus.
unfold Qeq, Qmult, Qnum, Qden.
rewrite Z.mul_1_r, Z.mul_1_r.
rewrite Z.mul_1_l, Pos.mul_1_l.
Lemma is_upper_bound_glb :
forall {R : ConstructiveReals} (E:CRcarrier R -> Prop),
sig_not_dec_T
-> sig_forall_dec_T
-> (exists x : CRcarrier R, E x)
-> (exists x : CRcarrier R, is_upper_bound E x)
-> { x : CRcarrier R
| forall r:Q, (x < CR_of_Q R r -> is_upper_bound E (CR_of_Q R r))
/\ (CR_of_Q R r < x -> ~is_upper_bound E (CR_of_Q R r)) }.
intros R E sig_not_dec lpo Einhab Ebound.
destruct (is_upper_bound_epsilon E lpo sig_not_dec Ebound) as [a luba].
destruct (is_upper_bound_not_epsilon E lpo sig_not_dec Einhab) as [b glbb].
pose (fun q => is_upper_bound E (CR_of_Q R q)) as upcut.
assert (forall q:Q, { upcut q } + { ~upcut q } ).
apply is_upper_bound_dec.
assert (forall q r : Q, (q <= r)%Q -> upcut q -> upcut r).
apply (CRle_lt_trans _ (CR_of_Q R r)).
assert (upcut (Z.of_nat a # 1)%Q).
assert (~upcut (- Z.of_nat b # 1)%Q).
assert (forall q r : Q, (q == r)%Q -> upcut q -> upcut r).
destruct (@glb_dec_Q R (Build_DedekindDecCut
upcut H3 (-Z.of_nat b # 1)%Q (Z.of_nat a # 1)
H H0 H1 H2)).
specialize (a0 r) as [_ a0].
Lemma is_upper_bound_closed :
forall {R : ConstructiveReals}
(E:CRcarrier R -> Prop) (sig_forall_dec : sig_forall_dec_T)
(sig_not_dec : sig_not_dec_T)
(Einhab : exists x : CRcarrier R, E x)
(Ebound : exists x : CRcarrier R, is_upper_bound E x),
is_lub
E (proj1_sig (is_upper_bound_glb
E sig_not_dec sig_forall_dec Einhab Ebound)).
destruct (is_upper_bound_glb E sig_not_dec sig_forall_dec Einhab Ebound); simpl.
destruct (CR_Q_dense R x0 x abs) as [q [qmaj H]].
specialize (a q) as [a _].
specialize (a qmaj x Ex).
destruct (is_upper_bound_glb E sig_not_dec sig_forall_dec Einhab Ebound); simpl.
destruct (CR_Q_dense R b x abs) as [q [qmaj H0]].
specialize (a q) as [_ a].
exact (CRlt_trans _ (CR_of_Q R q) _ qmaj abs2).
Lemma sig_lub :
forall {R : ConstructiveReals} (E:CRcarrier R -> Prop),
sig_forall_dec_T
-> sig_not_dec_T
-> (exists x : CRcarrier R, E x)
-> (exists x : CRcarrier R, is_upper_bound E x)
-> { u : CRcarrier R | is_lub E u }.
intros R E sig_forall_dec sig_not_dec Einhab Ebound.
pose proof (is_upper_bound_closed E sig_forall_dec sig_not_dec Einhab Ebound).
destruct (is_upper_bound_glb
E sig_not_dec sig_forall_dec Einhab Ebound); simpl in H.
Definition CRis_upper_bound {R : ConstructiveReals} (E:CRcarrier R -> Prop) (m:CRcarrier R)
:= forall x:CRcarrier R, E x -> CRlt R m x -> False.
Lemma CR_sig_lub :
forall {R : ConstructiveReals} (E:CRcarrier R -> Prop),
(forall x y : CRcarrier R, CReq R x y -> (E x <-> E y))
-> sig_forall_dec_T
-> sig_not_dec_T
-> (exists x : CRcarrier R, E x)
-> (exists x : CRcarrier R, CRis_upper_bound E x)
-> { u : CRcarrier R | CRis_upper_bound E u /\
forall y:CRcarrier R, CRis_upper_bound E y -> CRlt R y u -> False }.
exact (sig_lub E X X0 H0 H1).