Addition of Dedekind real numbers

Content created by Louis Wasserman.

Created on 2025-03-27.
Last modified on 2025-03-27.

{-# OPTIONS --lossy-unification #-}

module real-numbers.addition-real-numbers where
Imports
open import elementary-number-theory.addition-rational-numbers
open import elementary-number-theory.additive-group-of-rational-numbers
open import elementary-number-theory.positive-rational-numbers
open import elementary-number-theory.rational-numbers
open import elementary-number-theory.strict-inequality-rational-numbers

open import foundation.action-on-identifications-functions
open import foundation.binary-transport
open import foundation.cartesian-product-types
open import foundation.conjunction
open import foundation.dependent-pair-types
open import foundation.empty-types
open import foundation.equivalences
open import foundation.existential-quantification
open import foundation.function-types
open import foundation.functoriality-cartesian-product-types
open import foundation.identity-types
open import foundation.logical-equivalences
open import foundation.propositional-truncations
open import foundation.transport-along-identifications
open import foundation.universe-levels

open import group-theory.abelian-groups
open import group-theory.commutative-monoids
open import group-theory.groups
open import group-theory.monoids
open import group-theory.semigroups

open import logic.functoriality-existential-quantification

open import real-numbers.addition-lower-dedekind-real-numbers
open import real-numbers.addition-upper-dedekind-real-numbers
open import real-numbers.arithmetically-located-dedekind-cuts
open import real-numbers.dedekind-real-numbers
open import real-numbers.lower-dedekind-real-numbers
open import real-numbers.negation-lower-upper-dedekind-real-numbers
open import real-numbers.negation-real-numbers
open import real-numbers.rational-real-numbers
open import real-numbers.similarity-real-numbers
open import real-numbers.upper-dedekind-real-numbers

Idea

We introduce addition on the Dedekind real numbers and derive its basic properties.

The sum of two Dedekind real numbers is is a Dedekind real number whose lower cut (upper cut) is the the Minkowski sum of their lower (upper) cuts.

module _
  {l1 l2 : Level}
  (x :  l1) (y :  l2)
  where

  lower-real-add-ℝ : lower-ℝ (l1  l2)
  lower-real-add-ℝ = add-lower-ℝ (lower-real-ℝ x) (lower-real-ℝ y)

  upper-real-add-ℝ : upper-ℝ (l1  l2)
  upper-real-add-ℝ = add-upper-ℝ (upper-real-ℝ x) (upper-real-ℝ y)

  abstract
    is-disjoint-lower-upper-add-ℝ :
      is-disjoint-lower-upper-ℝ lower-real-add-ℝ upper-real-add-ℝ
    is-disjoint-lower-upper-add-ℝ p (p<x+y , x+y<p) =
      let open do-syntax-trunc-Prop empty-Prop
      in do
        ((px , py) , px<x , py<y , p=px+py)  p<x+y
        ((qx , qy) , x<qx , y<qy , p=qx+qy)  x+y<p
        irreflexive-le-ℚ
          ( p)
          ( binary-tr
            ( le-ℚ)
            ( inv p=px+py)
            ( inv p=qx+qy)
            ( preserves-le-add-ℚ
              { px}
              { qx}
              { py}
              { qy}
              ( le-lower-upper-cut-ℝ x px qx px<x x<qx)
              ( le-lower-upper-cut-ℝ y py qy py<y y<qy)))

    is-arithmetically-located-lower-upper-add-ℝ :
      is-arithmetically-located-lower-upper-ℝ lower-real-add-ℝ upper-real-add-ℝ
    is-arithmetically-located-lower-upper-add-ℝ ε⁺ =
      let
        open
          do-syntax-trunc-Prop
            (
              (  × )
              ( close-bounds-lower-upper-ℝ
                ( lower-real-add-ℝ)
                ( upper-real-add-ℝ)
                ( ε⁺)))
      in do
        (px , qx) , qx<px+εx , px<x , x<qx 
          is-arithmetically-located-ℝ x (left-summand-split-ℚ⁺ ε⁺)
        (py , qy) , qy<py+εy , py<y , y<qy 
          is-arithmetically-located-ℝ y (right-summand-split-ℚ⁺ ε⁺)
        intro-exists
          ( px +ℚ py , qx +ℚ qy)
          ( le-add-split-ℚ⁺ ε⁺ qx px qy py qx<px+εx qy<py+εy ,
            intro-exists (px , py) (px<x , py<y , refl) ,
            intro-exists (qx , qy) (x<qx , y<qy , refl))

    is-located-lower-upper-add-ℝ :
      is-located-lower-upper-ℝ lower-real-add-ℝ upper-real-add-ℝ
    is-located-lower-upper-add-ℝ =
      is-located-is-arithmetically-located-lower-upper-ℝ
        ( lower-real-add-ℝ)
        ( upper-real-add-ℝ)
        ( is-arithmetically-located-lower-upper-add-ℝ)

  add-ℝ :  (l1  l2)
  add-ℝ =
    real-lower-upper-ℝ
      ( lower-real-add-ℝ)
      ( upper-real-add-ℝ)
      ( is-disjoint-lower-upper-add-ℝ)
      ( is-located-lower-upper-add-ℝ)

infixl 35 _+ℝ_
_+ℝ_ = add-ℝ

Properties

Addition is commutative

module _
  {l1 l2 : Level}
  (x :  l1) (y :  l2)
  where

  abstract
    commutative-add-ℝ : x +ℝ y  y +ℝ x
    commutative-add-ℝ =
      eq-eq-lower-real-ℝ
        ( x +ℝ y)
        ( y +ℝ x)
        ( commutative-add-lower-ℝ (lower-real-ℝ x) (lower-real-ℝ y))

Addition is associative

module _
  {l1 l2 l3 : Level}
  (x :  l1) (y :  l2) (z :  l3)
  where

  abstract
    associative-add-ℝ : (x +ℝ y) +ℝ z  x +ℝ (y +ℝ z)
    associative-add-ℝ =
      eq-eq-lower-real-ℝ
        ( (x +ℝ y) +ℝ z)
        ( x +ℝ (y +ℝ z))
        ( associative-add-lower-ℝ
          ( lower-real-ℝ x)
          ( lower-real-ℝ y)
          ( lower-real-ℝ z))

Unit laws for addition

abstract
  left-unit-law-add-ℝ : {l : Level}  (x :  l)  zero-ℝ +ℝ x  x
  left-unit-law-add-ℝ x =
    eq-eq-lower-real-ℝ
      ( zero-ℝ +ℝ x)
      ( x)
      ( left-unit-law-add-lower-ℝ (lower-real-ℝ x))

  right-unit-law-add-ℝ : {l : Level}  (x :  l)  x +ℝ zero-ℝ  x
  right-unit-law-add-ℝ x =
    eq-eq-lower-real-ℝ
      ( x +ℝ zero-ℝ)
      ( x)
      ( right-unit-law-add-lower-ℝ (lower-real-ℝ x))

Inverse laws for addition

abstract
  right-inverse-law-add-ℝ :
    {l : Level}  (x :  l)  sim-ℝ (x +ℝ neg-ℝ x) zero-ℝ
  right-inverse-law-add-ℝ x =
    sim-rational-ℝ
      ( x +ℝ neg-ℝ x ,
        zero-ℚ ,
        elim-exists
          ( empty-Prop)
          ( λ (p , q) (p<x , x<-q , 0=p+q) 
            is-disjoint-cut-ℝ
              ( x)
              ( p)
              ( p<x ,
                inv-tr
                ( is-in-upper-cut-ℝ x)
                ( unique-left-neg-ℚ p q (inv 0=p+q))
                ( x<-q))) ,
        elim-exists
          ( empty-Prop)
          ( λ (p , q) (x<p , -q<x , 0=p+q) 
            is-disjoint-cut-ℝ
              ( x)
              ( p)
              ( inv-tr
                ( is-in-lower-cut-ℝ x)
                ( unique-left-neg-ℚ p q (inv 0=p+q))
                ( -q<x) ,
                x<p)))

  left-inverse-law-add-ℝ : {l : Level} (x :  l)  sim-ℝ (neg-ℝ x +ℝ x) zero-ℝ
  left-inverse-law-add-ℝ x =
    tr
      ( λ y  sim-ℝ y zero-ℝ)
      ( commutative-add-ℝ x (neg-ℝ x))
      ( right-inverse-law-add-ℝ x)

Addition on the real numbers preserves similarity

module _
  {l1 l2 l3 : Level}
  (z :  l1) (x :  l2) (y :  l3)
  where

  opaque
    unfolding sim-ℝ

    preserves-sim-right-add-ℝ : sim-ℝ x y  sim-ℝ (x +ℝ z) (y +ℝ z)
    pr1 (preserves-sim-right-add-ℝ (lx⊆ly , _)) q =
      map-tot-exists  (qx , _)  map-product (lx⊆ly qx) id)
    pr2 (preserves-sim-right-add-ℝ (_ , ly⊆lx)) q =
      map-tot-exists  (qy , _)  map-product (ly⊆lx qy) id)

    preserves-sim-left-add-ℝ : sim-ℝ x y  sim-ℝ (z +ℝ x) (z +ℝ y)
    preserves-sim-left-add-ℝ x≈y =
      binary-tr
        ( sim-ℝ)
        ( commutative-add-ℝ x z)
        ( commutative-add-ℝ y z)
        ( preserves-sim-right-add-ℝ x≈y)

Swapping laws for addition on real numbers

module _
  {l1 l2 l3 : Level} (x :  l1) (y :  l2) (z :  l3)
  where

  abstract
    right-swap-add-ℝ :
      (x +ℝ y) +ℝ z  (x +ℝ z) +ℝ y
    right-swap-add-ℝ =
      equational-reasoning
        (x +ℝ y) +ℝ z
         x +ℝ (y +ℝ z) by associative-add-ℝ x y z
         x +ℝ (z +ℝ y) by ap (x +ℝ_) (commutative-add-ℝ y z)
         (x +ℝ z) +ℝ y by inv (associative-add-ℝ x z y)

    left-swap-add-ℝ :
      x +ℝ (y +ℝ z)  y +ℝ (x +ℝ z)
    left-swap-add-ℝ =
      equational-reasoning
        x +ℝ (y +ℝ z)
         (x +ℝ y) +ℝ z by inv (associative-add-ℝ x y z)
         (y +ℝ x) +ℝ z by ap (_+ℝ z) (commutative-add-ℝ x y)
         y +ℝ (x +ℝ z) by associative-add-ℝ y x z

module _
  {l1 l2 : Level} (x :  l1) (y :  l2)
  where

  abstract
    cancel-right-add-diff-ℝ : sim-ℝ ((x +ℝ y) +ℝ neg-ℝ y) x
    cancel-right-add-diff-ℝ =
      binary-tr
        ( sim-ℝ)
        ( inv (associative-add-ℝ x y (neg-ℝ y)))
        ( right-unit-law-add-ℝ x)
        ( preserves-sim-left-add-ℝ
          ( x)
          ( y +ℝ neg-ℝ y)
          ( zero-ℝ)
          ( right-inverse-law-add-ℝ y))

    cancel-right-diff-add-ℝ : sim-ℝ ((x +ℝ neg-ℝ y) +ℝ y) x
    cancel-right-diff-add-ℝ =
      tr
        ( λ z  sim-ℝ z x)
        ( right-swap-add-ℝ x y (neg-ℝ y))
        ( cancel-right-add-diff-ℝ)

Addition reflects similarity

module _
  {l1 l2 l3 : Level}
  (z :  l1) (x :  l2) (y :  l3)
  where

  abstract
    reflects-sim-right-add-ℝ : sim-ℝ (x +ℝ z) (y +ℝ z)  sim-ℝ x y
    reflects-sim-right-add-ℝ x+z≈y+z =
      similarity-reasoning-ℝ
        x
        ~ℝ (x +ℝ z) +ℝ neg-ℝ z
          by symmetric-sim-ℝ (cancel-right-add-diff-ℝ x z)
        ~ℝ (y +ℝ z) +ℝ neg-ℝ z
          by preserves-sim-right-add-ℝ (neg-ℝ z) (x +ℝ z) (y +ℝ z) x+z≈y+z
        ~ℝ y by cancel-right-add-diff-ℝ y z

    reflects-sim-left-add-ℝ : sim-ℝ (z +ℝ x) (z +ℝ y)  sim-ℝ x y
    reflects-sim-left-add-ℝ z+x≈z+y =
      reflects-sim-right-add-ℝ
        ( binary-tr
          ( sim-ℝ)
          ( commutative-add-ℝ z x)
          ( commutative-add-ℝ z y)
          ( z+x≈z+y))

module _
  {l1 l2 l3 : Level}
  (z :  l1) (x :  l2) (y :  l3)
  where

  iff-translate-right-sim-ℝ : sim-ℝ x y  sim-ℝ (x +ℝ z) (y +ℝ z)
  pr1 iff-translate-right-sim-ℝ = preserves-sim-right-add-ℝ z x y
  pr2 iff-translate-right-sim-ℝ = reflects-sim-right-add-ℝ z x y

  iff-translate-left-sim-ℝ : sim-ℝ x y  sim-ℝ (z +ℝ x) (z +ℝ y)
  pr1 iff-translate-left-sim-ℝ = preserves-sim-left-add-ℝ z x y
  pr2 iff-translate-left-sim-ℝ = reflects-sim-left-add-ℝ z x y

The inclusion of rational numbers preserves addition

abstract
  add-real-ℚ : (p q : )  real-ℚ p +ℝ real-ℚ q  real-ℚ (p +ℚ q)
  add-real-ℚ p q =
    eq-sim-ℝ
      ( sim-rational-ℝ
        ( real-ℚ p +ℝ real-ℚ q ,
          p +ℚ q ,
          elim-exists
            ( empty-Prop)
            ( λ (pl , ql) (pl<p , ql<q , p+q=pl+ql) 
              irreflexive-le-ℚ
                ( p +ℚ q)
                ( inv-tr
                  ( λ r  le-ℚ r (p +ℚ q))
                  ( p+q=pl+ql)
                  ( preserves-le-add-ℚ {pl} {p} {ql} {q} pl<p ql<q))) ,
          elim-exists
            ( empty-Prop)
            ( λ (pu , qu) (p<pu , q<qu , p+q=pu+qu) 
              irreflexive-le-ℚ
                ( p +ℚ q)
                ( inv-tr
                  ( le-ℚ (p +ℚ q))
                  ( p+q=pu+qu)
                  ( preserves-le-add-ℚ {p} {pu} {q} {qu} p<pu q<qu)))))

abstract
  combine-right-add-two-real-ℚ :
    {l : Level}  (x :  l)  (p q : ) 
    x +ℝ real-ℚ p +ℝ real-ℚ q  x +ℝ real-ℚ (p +ℚ q)
  combine-right-add-two-real-ℚ x p q =
    equational-reasoning
      x +ℝ real-ℚ p +ℝ real-ℚ q
       x +ℝ (real-ℚ p +ℝ real-ℚ q) by associative-add-ℝ _ _ _
       x +ℝ real-ℚ (p +ℚ q) by ap (x +ℝ_) (add-real-ℚ p q)

Interchange laws for addition on real numbers

module _
  {l1 l2 l3 l4 : Level} (x :  l1) (y :  l2) (z :  l3) (w :  l4)
  where

  abstract
    interchange-law-add-add-ℝ : (x +ℝ y) +ℝ (z +ℝ w)  (x +ℝ z) +ℝ (y +ℝ w)
    interchange-law-add-add-ℝ =
      equational-reasoning
        (x +ℝ y) +ℝ (z +ℝ w)
         x +ℝ (y +ℝ (z +ℝ w)) by associative-add-ℝ _ _ _
         x +ℝ (z +ℝ (y +ℝ w)) by ap (x +ℝ_) (left-swap-add-ℝ y z w)
         (x +ℝ z) +ℝ (y +ℝ w) by inv (associative-add-ℝ x z (y +ℝ w))

Negation is distributive across addition

module _
  {l1 l2 : Level} (x :  l1) (y :  l2)
  where

  abstract
    distributive-neg-add-ℝ : neg-ℝ (x +ℝ y)  neg-ℝ x +ℝ neg-ℝ y
    distributive-neg-add-ℝ =
      eq-sim-ℝ
        ( similarity-reasoning-ℝ
          neg-ℝ (x +ℝ y)
          ~ℝ neg-ℝ (x +ℝ y) +ℝ x +ℝ neg-ℝ x
            by symmetric-sim-ℝ (cancel-right-add-diff-ℝ _ x)
          ~ℝ (((neg-ℝ (x +ℝ y) +ℝ x) +ℝ neg-ℝ x) +ℝ y) +ℝ neg-ℝ y
            by symmetric-sim-ℝ (cancel-right-add-diff-ℝ _ y)
          ~ℝ (((neg-ℝ (x +ℝ y) +ℝ x) +ℝ y) +ℝ neg-ℝ x) +ℝ neg-ℝ y
            by sim-eq-ℝ (ap (_+ℝ neg-ℝ y) (right-swap-add-ℝ _ (neg-ℝ x) y))
          ~ℝ ((neg-ℝ (x +ℝ y) +ℝ (x +ℝ y)) +ℝ neg-ℝ x) +ℝ neg-ℝ y
            by
              sim-eq-ℝ
                ( ap
                  ( _+ℝ neg-ℝ y)
                  ( ap (_+ℝ neg-ℝ x) (associative-add-ℝ _ _ _)))
          ~ℝ (zero-ℝ +ℝ neg-ℝ x) +ℝ neg-ℝ y
            by
              preserves-sim-right-add-ℝ
                ( neg-ℝ y)
                ( _)
                ( _)
                ( preserves-sim-right-add-ℝ
                  ( neg-ℝ x)
                  ( _)
                  ( _)
                  ( left-inverse-law-add-ℝ _))
          ~ℝ neg-ℝ x +ℝ neg-ℝ y
            by sim-eq-ℝ (ap (_+ℝ neg-ℝ y) (left-unit-law-add-ℝ _)))

The Abelian group of real numbers at lzero under addition

semigroup-add-ℝ-lzero : Semigroup (lsuc lzero)
semigroup-add-ℝ-lzero =
  ( ℝ-Set lzero ,
    add-ℝ ,
    associative-add-ℝ)

monoid-add-ℝ-lzero : Monoid (lsuc lzero)
monoid-add-ℝ-lzero =
  ( semigroup-add-ℝ-lzero ,
    zero-ℝ ,
    left-unit-law-add-ℝ ,
    right-unit-law-add-ℝ)

commutative-monoid-add-ℝ-lzero : Commutative-Monoid (lsuc lzero)
commutative-monoid-add-ℝ-lzero =
  ( monoid-add-ℝ-lzero ,
    commutative-add-ℝ)

group-add-ℝ-lzero : Group (lsuc lzero)
group-add-ℝ-lzero =
  ( ( semigroup-add-ℝ-lzero) ,
    ( zero-ℝ , left-unit-law-add-ℝ , right-unit-law-add-ℝ) ,
    ( neg-ℝ ,
      eq-sim-ℝ  left-inverse-law-add-ℝ ,
      eq-sim-ℝ  right-inverse-law-add-ℝ))

abelian-group-add-ℝ-lzero : Ab (lsuc lzero)
abelian-group-add-ℝ-lzero =
  ( group-add-ℝ-lzero ,
    commutative-add-ℝ)

Recent changes