Powers of Two

module elementary-number-theory.powers-of-two where

Imports

open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.divisibility-natural-numbers
open import elementary-number-theory.exponentiation-natural-numbers
open import elementary-number-theory.inequality-natural-numbers
open import elementary-number-theory.multiplication-natural-numbers
open import elementary-number-theory.natural-numbers
open import elementary-number-theory.parity-natural-numbers
open import elementary-number-theory.strong-induction-natural-numbers

open import foundation.split-surjective-maps
open import foundation.universe-levels

open import foundation-core.cartesian-product-types
open import foundation-core.coproduct-types
open import foundation-core.dependent-pair-types
open import foundation-core.empty-types
open import foundation-core.equality-cartesian-product-types
open import foundation-core.equivalences
open import foundation-core.functions
open import foundation-core.identity-types
open import foundation-core.injective-maps

Idea

Any natural number x can be written as (2^u(2v-1))-1 for some pair of natural numbers (u , v)

pair-expansion : ℕ → UU lzero
pair-expansion n =
  Σ (ℕ × ℕ)
    ( λ p →
      ( (exp-ℕ 2 (pr1 p)) *ℕ (succ-ℕ ((pr2 p) *ℕ 2))) ＝
        succ-ℕ n)

is-nonzero-pair-expansion :
  (u v : ℕ) →
  is-nonzero-ℕ ((exp-ℕ 2 u) *ℕ (succ-ℕ (v *ℕ 2)))
is-nonzero-pair-expansion u v =
  is-nonzero-mul-ℕ _ _
    ( is-nonzero-exp-ℕ 2 u is-nonzero-two-ℕ)
    ( is-nonzero-succ-ℕ _)

has-pair-expansion-is-even-or-odd :
  (n : ℕ) → is-even-ℕ n + is-odd-ℕ n → pair-expansion n
has-pair-expansion-is-even-or-odd n =
  strong-ind-ℕ
  ( λ m → (is-even-ℕ m + is-odd-ℕ m) → (pair-expansion m))
  ( λ x → (0 , 0) , refl)
  ( λ k f →
    ( λ {
      ( inl x) →
        ( let s = has-odd-expansion-is-odd k (is-odd-is-even-succ-ℕ k x)
          in pair
            ( 0 , (succ-ℕ (pr1 s)))
            ( ( ap ((succ-ℕ ∘ succ-ℕ) ∘ succ-ℕ) (left-unit-law-add-ℕ _)) ∙
            ( ( ap (succ-ℕ ∘ succ-ℕ) (pr2 s))))) ;
      ( inr x) →
        ( let e : is-even-ℕ k
              e = is-even-is-odd-succ-ℕ k x

              t : (pr1 e) ≤-ℕ k
              t = leq-quotient-div-ℕ' 2 k is-nonzero-two-ℕ e

              s : (pair-expansion (pr1 e))
              s = f (pr1 e) t (is-decidable-is-even-ℕ (pr1 e))
          in
            pair
              ( succ-ℕ (pr1 (pr1 s)) , pr2 (pr1 s))
              ( ( ap
                  ( _*ℕ (succ-ℕ ((pr2 (pr1 s)) *ℕ 2)))
                  ( commutative-mul-ℕ (exp-ℕ 2 (pr1 (pr1 s))) 2)) ∙
                ( ( associative-mul-ℕ 2
                    ( exp-ℕ 2 (pr1 (pr1 s)))
                    ( succ-ℕ ((pr2 (pr1 s)) *ℕ 2))) ∙
                  ( ( ap (2 *ℕ_) (pr2 s)) ∙
                    ( ( ap succ-ℕ
                        ( left-successor-law-add-ℕ (0 +ℕ (pr1 e)) (pr1 e))) ∙
                      ( ( ap
                          ( succ-ℕ ∘ succ-ℕ)
                          ( ap (_+ℕ (pr1 e)) (left-unit-law-add-ℕ (pr1 e)))) ∙
                        ( ( ap
                            ( succ-ℕ ∘ succ-ℕ)
                            ( inv (right-two-law-mul-ℕ (pr1 e)))) ∙
                            ( ( ap (succ-ℕ ∘ succ-ℕ) (pr2 e))))))))))}))
  ( n)

has-pair-expansion : (n : ℕ) → pair-expansion n
has-pair-expansion n =
  has-pair-expansion-is-even-or-odd n (is-decidable-is-even-ℕ n)

If `(u , v)` and `(u' , v')` are the pairs corresponding the same number `x`, then `u ＝ u'` and `v ＝ v'`

is-pair-expansion-unique :
  (u u' v v' : ℕ) →
  ((exp-ℕ 2 u) *ℕ (succ-ℕ (v *ℕ 2))) ＝
    ((exp-ℕ 2 u') *ℕ (succ-ℕ (v' *ℕ 2))) →
  (u ＝ u') × (v ＝ v')
is-pair-expansion-unique zero-ℕ zero-ℕ v v' p =
  ( pair refl
    ( is-injective-right-mul-ℕ 2 is-nonzero-two-ℕ
      ( is-injective-left-add-ℕ 0 (is-injective-succ-ℕ p))))
is-pair-expansion-unique zero-ℕ (succ-ℕ u') v v' p = ex-falso (s t)
  where
    s : is-odd-ℕ (succ-ℕ (0 +ℕ (v *ℕ 2)))
    s = is-odd-has-odd-expansion _
      ( v , ap succ-ℕ (inv (left-unit-law-add-ℕ _)))

    t : is-even-ℕ (succ-ℕ (0 +ℕ (v *ℕ 2)))
    t = tr is-even-ℕ (inv p) (div-mul-ℕ' _ 2 _ ((exp-ℕ 2 u') , refl))
is-pair-expansion-unique (succ-ℕ u) zero-ℕ v v' p = ex-falso (s t)
  where
    s : is-odd-ℕ (succ-ℕ (0 +ℕ (v' *ℕ 2)))
    s = is-odd-has-odd-expansion _
      ( v' , ap succ-ℕ (inv (left-unit-law-add-ℕ _)))

    t : is-even-ℕ (succ-ℕ (0 +ℕ (v' *ℕ 2)))
    t = tr is-even-ℕ p (div-mul-ℕ' _ 2 _ ((exp-ℕ 2 u) , refl))
is-pair-expansion-unique (succ-ℕ u) (succ-ℕ u') v v' p = pu , pv
  where
    q :
      ((exp-ℕ 2 u) *ℕ (succ-ℕ (v *ℕ 2))) ＝
        ((exp-ℕ 2 u') *ℕ (succ-ℕ (v' *ℕ 2)))
    q = is-injective-left-mul-ℕ 2 is-nonzero-two-ℕ
      ( inv (associative-mul-ℕ 2 (exp-ℕ 2 u) (succ-ℕ (v *ℕ 2))) ∙
      ( ( ap (_*ℕ (succ-ℕ (v *ℕ 2)))
        ( commutative-mul-ℕ 2 (exp-ℕ 2 u))) ∙
      ( ( p) ∙
      ( ( ap (_*ℕ (succ-ℕ (v' *ℕ 2)))
        ( commutative-mul-ℕ (exp-ℕ 2 u') 2)) ∙
      ( associative-mul-ℕ 2 (exp-ℕ 2 u') (succ-ℕ (v' *ℕ 2)))))))

    pu : (succ-ℕ u) ＝ (succ-ℕ u')
    pu = ap succ-ℕ (pr1 (is-pair-expansion-unique u u' v v' q))

    pv : v ＝ v'
    pv = pr2 (is-pair-expansion-unique u u' v v' q)

A pairing function is a bijection between ℕ × ℕ and ℕ.

Definition

pairing-map : ℕ × ℕ → ℕ
pairing-map (u , v) = pr1 p
  where
    p = is-successor-is-nonzero-ℕ (is-nonzero-pair-expansion u v)

Pairing function is split surjective

is-split-surjective-pairing-map : is-split-surjective pairing-map
is-split-surjective-pairing-map n = (u , v) , is-injective-succ-ℕ (q ∙ s)
  where
    u = pr1 (pr1 (has-pair-expansion n))
    v = pr2 (pr1 (has-pair-expansion n))

    s = pr2 (has-pair-expansion n)

    r = is-successor-is-nonzero-ℕ (is-nonzero-pair-expansion u v)

    q :
      ( succ-ℕ (pairing-map (u , v))) ＝
      ( (exp-ℕ 2 u) *ℕ (succ-ℕ (v *ℕ 2)))
    q = inv (pr2 r)

Pairing function is injective

is-injecitve-pairing-map : is-injective pairing-map
is-injecitve-pairing-map {u , v} {u' , v'} p =
  ( eq-pair' (is-pair-expansion-unique u u' v v' q))
  where
    r = is-successor-is-nonzero-ℕ (is-nonzero-pair-expansion u v)
    s = is-successor-is-nonzero-ℕ (is-nonzero-pair-expansion u' v')

    q :
      ( (exp-ℕ 2 u) *ℕ (succ-ℕ (v *ℕ 2))) ＝
        ( (exp-ℕ 2 u') *ℕ (succ-ℕ (v' *ℕ 2)))
    q = (pr2 r) ∙ (ap succ-ℕ p ∙ inv (pr2 s))

Pairing function is equivalence

is-equiv-pairing-map : is-equiv pairing-map
is-equiv-pairing-map =
  is-equiv-is-split-surjective-is-injective
    pairing-map
    is-injecitve-pairing-map
    is-split-surjective-pairing-map