Library UniMath.RealNumbers.DedekindCuts
Usual constructive Dedekind cuts
Catherine LELAY. July 2017 This file formalizes the usual definitions of constructive Dedekind cuts.- The two-sided definition come from the HoTT-book
- The one-sided definition come from Robert S Lubarsky and Michael Rathjen. On the constructive
Require Export UniMath.NumberSystems.RationalNumbers.
Require Import UniMath.RealNumbers.Prelim.
Require Import UniMath.RealNumbers.NonnegativeRationals.
Require Import UniMath.RealNumbers.NonnegativeReals.
Unset Kernel Term Sharing.
Local Open Scope hq_scope.
Definition isTwoSided (L U : hq → hProp) : UU :=
((∏ q : hq, L q ↔ ∃ r : hq, L r ∧ hqlth q r)
× (∏ q : hq, U q ↔ ∃ r : hq, U r ∧ hqlth r q))
× ((∃ q : hq, L q) × (∃ q : hq, U q))
× (∏ q : hq, ¬ (U q ∧ L q))
× (∏ q r : hq, hqlth q r → L q ∨ U r).
Definition isOneSided (S : hq → hProp) : UU :=
((∃ r : hq, S r) ∧ (∃ r : hq, ¬ S r))
× (∏ r : hq, S r → ∃ q : hq, S q ∧ hqlth r q)
× (∏ r s : hq, hqlth r s → S r ∨ ¬ S s).
Lemma isTwoSided_OneSided :
∏ (L U : hq → hProp), isTwoSided L U → isOneSided L.
Proof.
intros L U H.
split ; split.
- exact (pr1 (pr1 (pr2 H))).
- generalize (pr1 (pr2 (pr2 H))) (pr2 (pr1 (pr2 H))) ; intros H0.
apply hinhfun.
intros q.
∃ (pr1 q).
intros Lq.
apply (H0 (pr1 q)).
split.
+ exact (pr2 q).
+ exact Lq.
- intros r Lr.
generalize (pr1 (pr1 H)) ; intros H0.
exact (pr1 (H0 r) Lr).
- intros r s Hrs.
generalize (pr1 (pr2 (pr2 H))) (pr2 (pr2 (pr2 H))) ; intros H0 H1.
generalize (H1 _ _ Hrs).
apply hinhfun, sumofmaps.
+ exact ii1.
+ intros Us.
apply ii2.
intros Ls.
apply (H0 s).
split.
exact Us.
exact Ls.
Qed.
Lemma isOneSided_TwoSided :
∏ (S : hq → hProp),
isOneSided S → isTwoSided S (λ s : hq, ∃ r : hq, hqlth r s × ¬ S r).
Proof.
intros S H.
split ; split ; [ | | split | split].
- intros q ; split.
+ exact (pr1 (pr2 H) q).
+ apply hinhuniv ; intros r.
generalize (pr2 (pr2 H) _ _ (pr2 (pr2 r))).
apply hinhuniv, sumofmaps.
intros Sq ; apply Sq.
intros Sr.
apply fromempty.
apply Sr, (pr1 (pr2 r)).
- intros q ; split.
+ apply hinhfun.
intros r.
set (s := Prelim.hqlth_between _ _ (pr1 (pr2 r))).
∃ (pr1 s).
split.
× apply hinhpr.
∃ (pr1 r).
{ split.
- exact (pr1 (pr2 s)).
- exact (pr2 (pr2 r)).
}
× exact (pr2 (pr2 s)).
+ apply hinhuniv.
intros r.
generalize (pr1 (pr2 r)).
apply hinhfun.
intros s.
∃ (pr1 s).
split.
× apply istranshqlth with (pr1 r).
exact (pr1 (pr2 s)).
exact (pr2 (pr2 r)).
× exact (pr2 (pr2 s)).
- exact (pr1 (pr1 H)).
- generalize (pr2 (pr1 H)).
apply hinhfun.
intros r.
∃ (pr1 r+1).
apply hinhpr.
∃ (pr1 r).
split.
+ exact (hqlthnsn _).
+ exact (pr2 r).
- intros q Hq.
generalize (pr1 Hq).
apply (hinhuniv (P := make_hProp _ isapropempty)).
intros r.
generalize (pr2 (pr2 H) _ _ (pr1 (pr2 r))).
apply hinhuniv, sumofmaps.
+ exact (pr2 (pr2 r)).
+ intros Sq ; apply Sq.
exact (pr2 Hq).
- intros q r Hqr.
set (s := Prelim.hqlth_between _ _ Hqr).
generalize (pr2 (pr2 H) _ _ (pr1 (pr2 s))).
apply hinhfun, sumofmaps.
+ exact ii1.
+ intros Sr.
apply ii2, hinhpr.
∃ (pr1 s).
split.
× exact (pr2 (pr2 s)).
× exact Sr.
Qed.
Lemma weqTwoSidedOneSided :
(∑ L U : hq → hProp, isTwoSided L U) ≃ (∑ S : hq → hProp, isOneSided S).
Proof.
set (f := (λ (LU : ∑ L U : hq → hProp, isTwoSided L U),
pr1 LU,, isTwoSided_OneSided (pr1 LU) (pr1 (pr2 LU)) (pr2 (pr2 LU)))
: (∑ L U : hq → hProp, isTwoSided L U) → ∑ S, isOneSided S).
set (g := (λ S : (∑ S : hq → hProp, isOneSided S),
pr1 S ,, (λ s : hq, ∃ r : hq, r < s × ¬ pr1 S r)
,, isOneSided_TwoSided (pr1 S) (pr2 S))
: (∑ S, isOneSided S) → ∑ L U : hq → hProp, isTwoSided L U).
apply (weq_iso f g).
- intros LU.
change (pr1 (g (f LU)),, pr2 (g (f LU)) = pr1 LU,, pr2 LU).
apply pair_path_in2.
simple refine (subtypePath_prop (B := λ _, make_hProp _ _) _).
+ apply isapropdirprod.
apply isapropdirprod ;
apply impred_isaprop ; intro q ;
apply isapropdirprod ; apply isapropimpl, propproperty.
apply isapropdirprod.
apply isapropdirprod ; apply propproperty.
apply isapropdirprod.
apply impred_isaprop ; intro q.
apply isapropneg.
apply impred_isaprop ; intro q.
apply impred_isaprop ; intro r.
apply isapropimpl, propproperty.
+ apply funextfun ; intros q.
apply hPropUnivalence.
× apply hinhuniv.
intros r.
generalize (pr2 (pr2 (pr2 (pr2 (pr2 LU)))) _ _ (pr1 (pr2 r))).
apply hinhuniv, sumofmaps.
intro Lr ; apply fromempty, (pr2 (pr2 r)), Lr.
intros Uq ; apply Uq.
× intros Uq.
generalize (pr1 (pr2 (pr1 (pr2 (pr2 LU))) _) Uq).
apply hinhfun.
intros r.
∃ (pr1 r).
split.
apply (pr2 (pr2 r)).
intros Lr.
apply (pr1 (pr2 (pr2 (pr2 (pr2 LU)))) (pr1 r)).
split.
apply (pr1 (pr2 r)).
apply Lr.
- intros S.
simple refine (subtypePath_prop (B := λ _, make_hProp _ _) _).
+ apply isapropdirprod.
apply propproperty.
apply isapropdirprod.
apply impred_isaprop ; intro r.
apply isapropimpl, propproperty.
apply impred_isaprop ; intro r.
apply impred_isaprop ; intro s.
apply isapropimpl, propproperty.
+ reflexivity.
Qed.
Lemma isOneSided_Dcuts_bot :
∏ D, isOneSided D → Dcuts_def_bot (λ r, D (pr1 r)).
Proof.
intros D H r Dr q Hq.
generalize (le_eqorltNonnegativeRationals _ _ Hq) ; clear Hq.
apply sumofmaps ; intros H0.
- rewrite H0.
exact Dr.
- rewrite ltNonnegativeRationals_correct in H0.
generalize (pr2 (pr2 H) _ _ H0).
apply hinhuniv, sumofmaps ; intros Dq.
+ exact Dq.
+ apply fromempty, Dq, Dr.
Qed.
Lemma isOneSided_Dcuts_open :
∏ D, isOneSided D → Dcuts_def_open (λ r, D (pr1 r)).
Proof.
intros D H r Dr.
generalize ((pr1 (pr2 H)) (pr1 r) Dr).
apply hinhfun.
intros q.
assert (Hq : 0 ≤ pr1 q).
{ apply istranshqleh with (pr1 r).
exact (pr2 r).
apply hqlthtoleh, (pr2 (pr2 q)). }
∃ (pr1 q,,Hq).
split.
- change (D (NonnegativeRationals_to_Rationals
(pr1 q,,Hq))).
exact (pr1 (pr2 q)).
- rewrite ltNonnegativeRationals_correct.
change (pr1 r < (NonnegativeRationals_to_Rationals (pr1 q,,Hq))).
exact (pr2 (pr2 q)).
Qed.
Lemma isOneSided_translation :
∏ (D : hq → hProp) (c : hq),
isOneSided D → isOneSided (λ q, D (q + c)).
Proof.
intros D c Hd.
split ; split.
- generalize (pr1 (pr1 Hd)).
apply hinhfun.
intros r.
∃ (pr1 r - c).
unfold hqminus.
rewrite hqplusassoc, hqlminus, hqplusr0.
exact (pr2 r).
- generalize (pr2 (pr1 Hd)).
apply hinhfun.
intros r.
∃ (pr1 r - c).
unfold hqminus.
rewrite hqplusassoc, hqlminus, hqplusr0.
exact (pr2 r).
- intros r D'r.
generalize (pr1 (pr2 Hd) _ D'r).
apply hinhfun.
intros q.
∃ (pr1 q - c).
split.
+ unfold hqminus.
rewrite hqplusassoc, hqlminus, hqplusr0.
exact (pr1 (pr2 q)).
+ apply hqlthandplusrinv with c.
unfold hqminus.
rewrite hqplusassoc, hqlminus, hqplusr0.
exact (pr2 (pr2 q)).
- intros r s Hrs.
apply (pr2 (pr2 Hd)).
apply hqlthandplusr, Hrs.
Qed.
Lemma isOneSided_Dcuts_corr :
∏ D, isOneSided D → Dcuts_def_corr (λ r, D (pr1 r)).
Proof.
intros D H c Hc.
rewrite ltNonnegativeRationals_correct in Hc.
generalize (pr2 (pr2 H) _ _ Hc).
apply hinhuniv ; intros H0.
apply coprodcomm in H0.
revert H0 ; apply sumofmaps ; intros H0.
apply hinhpr, ii1, H0.
enough (Hq : ∃ q : NonnegativeRationals, D (pr1 q) × ¬ D (pr1 (q + c)%NRat)).
{ revert Hq.
apply hinhfun, ii2. }
generalize (pr2 (pr1 H)).
apply hinhuniv.
intros r.
generalize (isarchhq (hqdiv (pr1 r) (hqdiv (pr1 c) 2%hq))).
apply hinhuniv.
intros n.
assert (Hc' : hqdiv (pr1 c) 2 > 0).
{ apply hqmultgth0gth0.
exact Hc.
apply hqgthandmultlinv with 2.
exact hq2_gt0.
rewrite hqmultx0, hqisrinvmultinv.
exact hq1_gt0.
apply hqgth_hqneq, hq2_gt0. }
assert (H1 : hqlth (pr1 r) (nattoring (pr1 n) × (hqdiv (pr1 c) 2))).
{ unfold hqlth in Hc.
apply hqgthandmultrinv with (/ (hqdiv (pr1 c) 2)).
- apply hqgthandmultlinv with (hqdiv (pr1 c) 2).
+ exact Hc'.
+ rewrite hqmultx0, hqisrinvmultinv.
exact hq1_gt0.
apply hqgth_hqneq, Hc'.
- rewrite hqmultassoc, hqisrinvmultinv.
rewrite hqmultr1.
unfold hqdiv in n.
exact (pr2 n).
apply hqgth_hqneq, Hc'. }
assert (Hn : ¬ D (nattoring (pr1 n) × hqdiv (pr1 c) 2)).
{ generalize (pr2 (pr2 H) _ _ H1).
apply (hinhuniv (P := hneg _)), sumofmaps ; intro H2.
apply fromempty, (pr2 r), H2.
apply H2. }
assert (H2 : ∏ (m : nat),
nattoring m × hqdiv (pr1 c) 2 + pr1 c = nattoring (m + 2) × hqdiv (pr1 c) 2).
{ intros m.
unfold nattoring.
rewrite 2!(@nattorig_natmult hq).
rewrite natmult_plus.
apply maponpaths.
simpl.
unfold hqdiv.
rewrite <- hqmult2r, hqmultassoc.
rewrite hqislinvmultinv.
apply pathsinv0, hqmultr1.
apply hqgth_hqneq, hq2_gt0. }
generalize (pr1 n) Hn.
clear -H H0 Hc Hc' H2 ; intros n Hn.
assert (Hm : D (nattoring O × hqdiv (pr1 c) 2)).
{ rewrite hqmult0x.
exact H0. }
destruct n.
{ apply fromempty, Hn, Hm. }
rewrite <- (natplusl0 n), plus_n_Sm in Hn.
revert Hm Hn.
set (m := O).
change (D (nattoring m × hqdiv (pr1 c) 2)
→ ¬ D (nattoring (m + S n) × hqdiv (pr1 c) 2)
→ ∃ q : NonnegativeRationals, D (pr1 q) × ¬ D (pr1 (q + c)%NRat)).
generalize m ; clear m H0.
revert D H.
induction n as [ | n IHn] ; intros D H m Hm Hn.
- apply hinhpr.
use tpair.
use tpair.
apply (nattoring m × hqdiv (pr1 c) 2).
abstract (apply hq0lehandmult ;
[ clear ;
induction m ;
[ apply isreflhqleh
| unfold nattoring ;
rewrite nattorigS ;
apply hq0lehandplus ;
[ exact hq1ge0 | exact IHm ]]
| apply hqlthtoleh, Hc' ]).
simpl.
split.
exact Hm.
change (¬ D ((nattoring m × hqdiv (pr1 c) 2) + (pr1 c))).
intros H0.
refine (hinhuniv' _ _ _).
apply isapropempty.
2: apply (pr2 (pr2 H) (nattoring (m + 1) × hqdiv (pr1 c) 2) (nattoring m × hqdiv (pr1 c) 2 + pr1 c)).
apply sumofmaps.
exact Hn.
intros H1 ; apply H1, H0.
rewrite H2.
apply hqlthandmultr.
exact Hc'.
unfold nattoring.
rewrite <- (plus_n_Sm m 1%nat).
rewrite nattorigS, hqpluscomm.
apply hqlthnsn.
- refine (hinhuniv _ _).
2: apply (pr2 (pr2 H) (nattoring (m + 1) × hqdiv (pr1 c) 2) (nattoring (m + 2) × hqdiv (pr1 c) 2)).
apply sumofmaps ; intros Hm'.
+ apply IHn with (m + 1)%nat.
× exact H.
× exact Hm'.
× rewrite natplusassoc.
exact Hn.
+ apply hinhpr.
use tpair.
use tpair.
apply (nattoring m × hqdiv (pr1 c) 2).
abstract (apply hq0lehandmult ;
[ clear ;
induction m ;
[ apply isreflhqleh
| unfold nattoring ;
rewrite nattorigS ;
apply hq0lehandplus ;
[ exact hq1ge0 | exact IHm ]]
| apply hqlthtoleh, Hc' ]).
simpl.
split.
exact Hm.
change (¬ D ((nattoring m × hqdiv (pr1 c) 2) + (pr1 c))).
rewrite H2.
exact Hm'.
+ apply hqlthandmultr.
exact Hc'.
unfold nattoring.
rewrite <- (plus_n_Sm m 1%nat).
rewrite nattorigS, hqpluscomm.
apply hqlthnsn.
Qed.
Lemma isDcuts_OneSided :
∏ (D : NonnegativeRationals → hProp),
Dcuts_def_bot D → Dcuts_def_open D → Dcuts_def_corr D
→ isOneSided (λ q : hq, sumofmaps (λ _ : 0 > q, htrue) (λ Hq : 0 ≤ q, D (q,, Hq)) (hqgthorleh 0 q)).
Proof.
intros D Hbot Hopen Hcorr.
split ; split.
- apply hinhpr.
∃ (-(1)).
induction (hqgthorleh 0 (- (1))) as [H | H].
+ exact tt.
+ apply fromempty.
refine (hqlehtoneghqgth _ _ _ _).
apply H.
apply hqgthandplusrinv with 1.
rewrite hqlminus, hqplusl0.
exact hq1_gt0.
- generalize (Hcorr _ ispositive_oneNonnegativeRationals).
apply hinhfun, sumofmaps ; intros H.
+ ∃ 1.
induction (hqgthorleh 0 1) as [H0 | H0].
× apply fromempty.
refine (hqgthtoneghqleh _ _ _ _).
exact H0.
exact hq1ge0.
× assert (H1 : 1%NRat = (1 ,, H0))
by (apply subtypePath_prop ; reflexivity).
rewrite H1 in H.
exact H.
+ rename H into q.
∃ (pr1 (pr1 q) + 1).
induction (hqgthorleh 0 (pr1 (pr1 q) + 1)) as [H0 | H0].
× apply fromempty.
refine (hqgthtoneghqleh _ _ _ _).
apply H0.
apply hq0lehandplus.
exact (pr2 (pr1 q)).
exact hq1ge0.
× assert (Hq1 : (pr1 q + 1)%NRat = (pr1 (pr1 q) + 1 ,, H0))
by (apply subtypePath_prop ; reflexivity).
generalize (pr2 (pr2 q)) ; intro Hq.
rewrite Hq1 in Hq.
exact Hq.
- intros r Dr.
induction (hqgthorleh 0 r) as [Hr | Hr].
+ set (q := hqlth_between _ _ Hr).
apply hinhpr.
∃ (pr1 q).
split.
induction (hqgthorleh 0 (pr1 q)) as [Hq | Hq].
× exact tt.
× apply fromempty.
refine (hqlehtoneghqgth _ _ _ _).
exact Hq.
unfold hqlth in q.
exact (pr2 (pr2 q)).
× exact (pr1 (pr2 q)).
+ generalize (Hopen _ Dr).
apply hinhfun.
intros q.
∃ (pr1 (pr1 q)).
induction (hqgthorleh 0 (pr1 (pr1 q))) as [Hq | Hq].
× apply fromempty.
refine (hqgthtoneghqleh _ _ _ _).
apply Hq.
exact (pr2 (pr1 q)).
× split.
assert (Hq1 : pr1 q = (pr1 (pr1 q) ,, Hq))
by (apply subtypePath_prop ; reflexivity).
generalize (pr1 (pr2 q)) ; intro Hq'.
rewrite Hq1 in Hq'.
exact Hq'.
generalize (pr2 (pr2 q)) ; intro Hq'.
rewrite ltNonnegativeRationals_correct in Hq'.
exact Hq'.
-intros r q Hrq.
induction (hqgthorleh 0 r) as [Hr | Hr].
apply hinhpr, ii1, tt.
induction (hqgthorleh 0 q) as [Hq | Hq].
+ apply fromempty.
refine (hqlehtoneghqgth _ _ _ _).
apply Hr.
apply istranshqgth with q.
exact Hq.
unfold hqlth in Hrq.
exact Hrq.
+ apply (Dcuts_locatedness (D,,Hbot,,Hopen,,Hcorr)).
rewrite ltNonnegativeRationals_correct.
exact Hrq.
Qed.
Lemma weqOneSidedDcuts :
weq (∑ S : hq → hProp, isOneSided S × ∏ q : hq, q < 0 → S q) Dcuts.
Proof.
set (f := (λ (D : ∑ S : hq → hProp, isOneSided S × (∏ q : hq, q < 0 → S q)),
make_Dcuts (λ r : NonnegativeRationals, pr1 D (pr1 r))
(isOneSided_Dcuts_bot (pr1 D) (pr1 (pr2 D)))
(isOneSided_Dcuts_open (pr1 D) (pr1 (pr2 D)))
(isOneSided_Dcuts_corr (pr1 D) (pr1 (pr2 D))))
: (∑ S : hq → hProp, isOneSided S × (∏ q : hq, q < 0 → S q)) → Dcuts).
assert (Hg : ∏ (D : Dcuts) (q : hq),
q < 0
→ sumofmaps (λ _ : 0 > q, htrue) (λ Hq : 0 ≤ q, pr1 D (q,, Hq)) (hqgthorleh 0 q)).
{ intros D q Hq.
induction (hqgthorleh 0 q) as [Hq' | Hq'].
exact tt.
apply fromempty.
refine (hqlehtoneghqgth _ _ _ _).
apply Hq'.
unfold hqlth in Hq.
exact Hq. }
set (g := (λ D : Dcuts,
(λ q : hq,
sumofmaps (λ _ : 0 > q, htrue) (λ Hq : 0 ≤ q, pr1 D (q,, Hq))
(hqgthorleh 0 q)),,
isDcuts_OneSided (pr1 D) (is_Dcuts_bot D) (is_Dcuts_open D)
(is_Dcuts_corr D),, Hg D)
: Dcuts → ∑ S : hq → hProp, isOneSided S × (∏ q : hq, q < 0 → S q)).
apply (weq_iso f g).
- intros D.
simple refine (subtypePath_prop (B := λ _, make_hProp _ _) _).
+ apply isapropdirprod.
apply isapropdirprod.
apply propproperty.
apply isapropdirprod.
apply impred_isaprop ; intro r.
apply isapropimpl, propproperty.
apply impred_isaprop ; intro r.
apply impred_isaprop ; intro s.
apply isapropimpl, propproperty.
apply impred_isaprop ; intro q.
apply isapropimpl, propproperty.
+ apply funextfun ; intros q.
apply hPropUnivalence.
× change (sumofmaps (λ _ : 0 > q, htrue) (λ _ : ¬ (0 > q), pr1 D q) (hqgthorleh 0 q) → pr1 D q).
induction (hqgthorleh 0 q) as [Hq | Hq].
intros _.
apply (pr2 (pr2 D)).
exact Hq.
intros H ; apply H.
× change (pr1 D q → sumofmaps (λ _ : 0 > q, htrue) (λ _ : ¬ (0 > q), pr1 D q) (hqgthorleh 0 q)).
intros Dq.
induction (hqgthorleh 0 q) as [Hq | Hq].
exact tt.
exact Dq.
- intros D.
apply subtypePath_prop.
apply funextfun ; intros q.
apply hPropUnivalence.
+ change (sumofmaps (λ _ : 0 > pr1 q, htrue)
(λ Hq : ¬ (0 > pr1 q), pr1 D (pr1 q,, Hq)) (hqgthorleh 0 (pr1 q))
→ pr1 D q).
induction (hqgthorleh 0 (pr1 q)) as [Hq | Hq].
apply fromempty.
refine (hqlehtoneghqgth _ _ _ _).
exact (pr2 q).
exact Hq.
intros H.
assert (Hq1 : q = (pr1 q,, Hq))
by (apply subtypePath_prop ; reflexivity).
rewrite Hq1 ; exact H.
+ change (pr1 D q
→ sumofmaps (λ _ : 0 > pr1 q, htrue)
(λ Hq : ¬ (0 > pr1 q), pr1 D (pr1 q,, Hq)) (hqgthorleh 0 (pr1 q))).
intros Dq.
induction (hqgthorleh 0 (pr1 q)) as [Hq | Hq].
apply fromempty.
refine (hqlehtoneghqgth _ _ _ _).
exact (pr2 q).
exact Hq.
assert (Hq1 : q = (pr1 q,, Hq))
by (apply subtypePath_prop ; reflexivity).
rewrite Hq1 in Dq ; exact Dq.
Qed.