# 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
Dedekind reals. Logic and Analysis.
I first prove the equivalence between these two definitions, then I prove the equivalence between the non-negative numbers of the one-sided definition and the set Dcuts

Require Export UniMath.NumberSystems.RationalNumbers.
Require Import UniMath.RealNumbers.Prelim.
Require Import UniMath.RealNumbers.NonnegativeRationals.
Require Import UniMath.RealNumbers.NonnegativeReals.

Unset Kernel Term Sharing.

## Usual definitions

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).

## Equivalence between these two definitions

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.

## Equivalence of Dcuts with usual definitions

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.