Powers of two

Content created by Fredrik Bakke, Egbert Rijke, Elif Uskuplu, Jonathan Prieto-Cubides and Victor Blanchi.

Created on 2023-04-26.
Last modified on 2024-03-20.

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.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.equality-cartesian-product-types
open import foundation.function-types
open import foundation.split-surjective-maps
open import foundation.transport-along-identifications
open import foundation.universe-levels

open import foundation-core.cartesian-product-types
open import foundation-core.coproduct-types
open import foundation-core.empty-types
open import foundation-core.equivalences
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-ℕ _)

abstract
  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 →
      ( λ where
        ( 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 (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-injective-pairing-map : is-injective pairing-map
is-injective-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-injective-pairing-map
    is-split-surjective-pairing-map

Recent changes