standard bijections of Natural numbers

Cubical/Data/Nat/Bijections/IncreasingFunction.agda

@@ -0,0 +1,155 @@
+module Cubical.Data.Nat.Bijections.IncreasingFunction where
+
+{- Consider an increasing function f : ℕ → ℕ with f 0 ≡ 0.
+-- Note that we can partition ℕ into the pieces [f k , f (suc k) ) for k ∈ ℕ
+-- 0=f0 ..... f1 ..... f2 ..... f3 ...
+-- [          )[       )[       )[ ...
+-- This module formalizes this idea.
+-}
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.HLevels
+
+open import Cubical.Data.Nat
+open import Cubical.Data.Nat.Order
+open <-Reasoning
+
+open import Cubical.Data.Sigma
+open import Cubical.Data.Sum
+open import Cubical.Relation.Nullary
+open import Cubical.Data.Empty renaming (rec to ex-falso)
+
+private
+  kIsUnique : (f : ℕ → ℕ ) → isStrictlyIncreasing f → (n : ℕ) →
+              (k  : ℕ) →  ((f k  ≤ n) × (n < f (suc k ))) →
+              (k' : ℕ) →  ((f k' ≤ n) × (n < f (suc k'))) →
+              k ≡ k'
+  kIsUnique f fInc n k (fk≤n , n<fsk ) k' (fk'≤n , n<fsk') = k=k' where
+    compare : (l : ℕ) → (l' : ℕ) →
+              n < f (suc l) → f l' ≤ n →
+              ¬ l < l'
+    compare l l' n<fsl fl'≤n l<l' = ¬m<m $
+     n
+       <≤⟨ n<fsl ⟩
+     f (suc l)
+       ≤⟨ strictlyIncreasing→Increasing fInc l<l' ⟩
+     f l'
+       ≤≡⟨ fl'≤n  ⟩
+     n ∎
+
+    k=k' : k ≡ k'
+    k=k' with k ≟ k'
+    ... | lt k<k' = ex-falso (compare k k' n<fsk fk'≤n k<k')
+    ... | eq k=k' = k=k'
+    ... | gt k'<k = ex-falso (compare k' k n<fsk' fk≤n k'<k)
+
+  approxFunction : (f : ℕ → ℕ) → (f 0 ≡ 0) → isStrictlyIncreasing f →
+                   (n : ℕ) → Σ[ k ∈ ℕ ]  (f k ≤ n) × (n < f (suc k))
+  approxFunction f f0=0 fInc zero = 0 , f0≤0 , 0<f1 where
+
+    f0≤0 : f 0 ≤ 0
+    f0≤0 = ≤-reflexive f0=0
+
+    f0<f1 : f 0 < f 1
+    f0<f1 = fInc <-suc
+
+    0<f1 : 0 < f 1
+    0<f1 = 0 ≡<⟨ sym f0=0 ⟩ f 0 <≡⟨ f0<f1 ⟩ f 1 ∎
+
+  approxFunction f f0=0 fInc (suc n) = newsol $ f (suc k) ≟ suc n where
+
+    oldsol : Σ[ k ∈ ℕ ] ( (f k ≤ n) ×  (n < f (suc k)))
+    oldsol = approxFunction f f0=0 fInc n
+
+    k : ℕ
+    k = fst oldsol
+
+    fk≤n : f k ≤ n
+    fk≤n = fst (snd oldsol)
+
+    n<fsk : n < f (suc k)
+    n<fsk = snd (snd oldsol)
+
+    newsol : Trichotomy (f (suc k)) (suc n) → Σ[ k' ∈ ℕ ] (f k' ≤ suc n) × (suc n < f (suc k'))
+    newsol (lt fsk<sn) = ex-falso (¬squeeze< (n<fsk , fsk<sn))
+    newsol (eq fsk=sn) = suc k , ≤-reflexive fsk=sn , (
+      suc n
+        ≡<⟨ sym fsk=sn ⟩
+      f (suc k)
+        <≡⟨ fInc <-suc ⟩
+      f (suc (suc k)) ∎ )
+    newsol (gt fsk>sn) = k , (f k
+                               ≤⟨ fk≤n ⟩
+                              n
+                               ≤≡⟨ <-weaken <-suc ⟩
+                              suc n ∎) ,            fsk>sn
+
+module _ (f : ℕ → ℕ) (f0=0 : f 0 ≡ 0) (fInc : isStrictlyIncreasing f) where
+  nearestValues : (n : ℕ) → ∃![ k ∈ ℕ ] (f k ≤ n) × (n < f (suc k))
+  nearestValues n = uniqueExists k p goalIsProp (kIsUnique f fInc n k p) where
+
+    solution : Σ[ k ∈ ℕ ] ( (f k ≤ n) ×  (n < f (suc k)))
+    solution = approxFunction f f0=0 fInc n
+
+    k : ℕ
+    k = fst solution
+
+    p : (f k ≤ n) × (n < f (suc k))
+    p = snd solution
+
+    goalIsProp : (k : ℕ) → isProp ( (f k ≤ n ) × (n < f (suc k)))
+    goalIsProp _ = isProp× isProp≤ isProp≤
+
+  partition : Type
+  partition = Σ[ k ∈ ℕ ] Σ[ i ∈ ℕ ] i + (f k) < f (suc k)
+
+  partition≅ℕ : Iso partition ℕ
+  Iso.fun partition≅ℕ (k , i , _) = i + f k
+  Iso.inv partition≅ℕ n = k , i , (
+    i + f k
+      ≡<⟨ i+fk=n ⟩
+    n
+      <≡⟨ n<fsk ⟩
+    f (suc k) ∎) where
+      incApprox = nearestValues n
+
+      k : ℕ
+      k = fst (fst incApprox)
+
+      i : ℕ
+      i = fst (fst (snd (fst incApprox)))
+
+      i+fk=n : i + f k ≡ n
+      i+fk=n = snd (fst (snd (fst incApprox)))
+
+      n<fsk : n < f (suc k)
+      n<fsk = snd (snd (fst incApprox))
+
+  Iso.rightInv partition≅ℕ n =
+    snd (fst (snd (fst (nearestValues n))))
+
+  Iso.leftInv  partition≅ℕ  y@(k , i , i+fk<fsk) =
+    ΣPathP (k'=k , ΣPathPProp (λ a → isProp≤) i'=i) where
+
+      inv = Iso.inv partition≅ℕ
+      n   = i + f k
+
+      k'  = fst (inv n)
+      i'  = fst (snd (inv n))
+
+      fk≤n : f k ≤ n
+      fk≤n = ≤SumRight
+
+      n<fsk : n < f (suc k )
+      n<fsk = i+fk<fsk
+
+      ans : (k' , (i' , _ ) , _ ) ≡ (k , (i , _ ) , _ )
+      ans = snd (nearestValues n) (k , fk≤n , n<fsk)
+
+      k'=k : k' ≡ k
+      k'=k = fst (PathPΣ ans)
+
+      i'=i : i' ≡ i
+      i'=i = fst (PathPΣ (fst (PathPΣ (snd (PathPΣ ans)))))

Cubical/Data/Nat/Bijections/Product.agda

@@ -0,0 +1,17 @@
+module Cubical.Data.Nat.Bijections.Product where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Data.Nat
+open import Cubical.Data.Sigma
+open import Cubical.Data.Nat.Bijections.Triangle
+
+Triangle⊂ℕ×ℕ≅ℕ×ℕ : Iso Triangle⊂ℕ×ℕ (ℕ × ℕ)
+Iso.fun Triangle⊂ℕ×ℕ≅ℕ×ℕ (_ , k , m , _) = m , k
+Iso.inv Triangle⊂ℕ×ℕ≅ℕ×ℕ (m , k)         = m + k , k , m , refl
+Iso.rightInv Triangle⊂ℕ×ℕ≅ℕ×ℕ _ = refl
+Iso.leftInv  Triangle⊂ℕ×ℕ≅ℕ×ℕ (n , k , m , p) = J
+  (λ n q → (Iso.inv Triangle⊂ℕ×ℕ≅ℕ×ℕ (Iso.fun Triangle⊂ℕ×ℕ≅ℕ×ℕ (n , k , m , q))) ≡ (n , k , m , q)) refl p
+
+ℕ×ℕ≅ℕ : Iso (ℕ × ℕ) ℕ
+ℕ×ℕ≅ℕ = compIso (invIso Triangle⊂ℕ×ℕ≅ℕ×ℕ) Triangle⊂ℕ×ℕ≅ℕ

Cubical/Data/Nat/Bijections/Sum.agda

@@ -0,0 +1,74 @@
+module Cubical.Data.Nat.Bijections.Sum where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.Isomorphism
+
+open import Cubical.Data.Sigma
+open import Cubical.Data.Sum
+open import Cubical.Relation.Nullary
+open import Cubical.Data.Empty renaming (rec to ex-falso)
+
+open import Cubical.Data.Nat
+open import Cubical.Data.Nat.Order
+open <-Reasoning
+
+open import Cubical.Tactics.NatSolver
+open import Cubical.Data.Nat.Bijections.IncreasingFunction
+
+double : ℕ → ℕ
+double n = n + n
+
+private
+  2Sn=2n+2 : {n : ℕ} → double (suc n) ≡ double n + 2
+  2Sn=2n+2 = solveℕ!
+
+  doubleGrows : (n : ℕ) → double n < double (suc n)
+  doubleGrows n = double n
+                    ≡<⟨ refl ⟩
+                  n + n
+                    <≡⟨ <SumLeft ⟩
+                  n + n + 2
+                    ≡⟨ sym 2Sn=2n+2 ⟩
+                  double (suc n) ∎
+
+  ¬2n+2+k<2n : (n : ℕ) → (k : ℕ) → ¬ ( suc (suc k) + double n < double (suc n))
+  ¬2n+2+k<2n n k p = ex-falso (¬-<-zero k<0) where
+      2n+k+2<2n+2 : double n + suc (suc k) < double n + 2
+      2n+k+2<2n+2 = double n + suc (suc k)
+                      ≡<⟨ +-comm (n + n) (suc (suc k)) ⟩
+                    suc (suc k) + double n
+                      <≡⟨ p ⟩
+                    double (suc n)
+                      ≡⟨ 2Sn=2n+2 ⟩
+                    double n + 2 ∎
+      k+2<2 : suc (suc k) < suc (suc 0)
+      k+2<2 = <-k+-cancel 2n+k+2<2n+2
+      k<0 : k < 0
+      k<0 = pred-≤-pred (pred-≤-pred k+2<2)
+
+doubleInc : isStrictlyIncreasing double
+doubleInc = sucIncreasing→StrictlyIncreasing double doubleGrows
+
+private
+  partitionDouble≅ℕ⊎ℕ : Iso (partition double refl doubleInc) (ℕ ⊎ ℕ)
+  Iso.fun partitionDouble≅ℕ⊎ℕ (n , zero        , p) = inl n
+  Iso.fun partitionDouble≅ℕ⊎ℕ (n , suc zero    , p) = inr n
+  Iso.fun partitionDouble≅ℕ⊎ℕ (n , suc (suc k) , p) = ex-falso (¬2n+2+k<2n n k p)
+  Iso.inv partitionDouble≅ℕ⊎ℕ (inl n) = n , zero , doubleGrows n
+  Iso.inv partitionDouble≅ℕ⊎ℕ (inr n) = n , 1 , (
+                 1 + n + n <≡⟨ <SumRight {k = 0} ⟩
+                 2 + n + n  ≡⟨ +-comm 2 (n + n)  ⟩
+                 n + n + 2  ≡⟨ sym 2Sn=2n+2      ⟩
+                 double (suc n) ∎         )
+  Iso.rightInv partitionDouble≅ℕ⊎ℕ (inl n) = refl
+  Iso.rightInv partitionDouble≅ℕ⊎ℕ (inr n) = refl
+  Iso.leftInv partitionDouble≅ℕ⊎ℕ (k , zero        , p) = ΣPathP (refl , ΣPathPProp (λ a → isProp≤) refl)
+  Iso.leftInv partitionDouble≅ℕ⊎ℕ (k , suc zero    , p) = ΣPathP (refl , ΣPathPProp (λ a → isProp≤) refl)
+  Iso.leftInv partitionDouble≅ℕ⊎ℕ (k , suc (suc i) , p) = ex-falso $ ¬2n+2+k<2n k i p
+
+  partitionDouble≅ℕ : Iso (partition double refl doubleInc) ℕ
+  partitionDouble≅ℕ = partition≅ℕ double refl doubleInc
+
+ℕ⊎ℕ≅ℕ : Iso (ℕ ⊎ ℕ) ℕ
+ℕ⊎ℕ≅ℕ = compIso (invIso partitionDouble≅ℕ⊎ℕ) partitionDouble≅ℕ

Cubical/Data/Nat/Bijections/Triangle.agda

@@ -0,0 +1,52 @@
+module Cubical.Data.Nat.Bijections.Triangle where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Data.Sigma
+
+open import Cubical.Data.Nat
+open import Cubical.Data.Nat.Order
+open <-Reasoning
+open import Cubical.Tactics.NatSolver
+open import Cubical.Data.Nat.Bijections.IncreasingFunction
+
+Triangle⊂ℕ×ℕ = Σ[ k ∈ ℕ ] Σ[ i ∈ ℕ ] (i ≤ k)
+
+triangle : ℕ → ℕ
+triangle zero = zero
+triangle (suc n) = n + suc (triangle n)
+
+strictIncTriangle : isStrictlyIncreasing triangle
+strictIncTriangle = sucIncreasing→StrictlyIncreasing triangle triangleN<triangleSN where
+  triangleN<triangleSN : (n : ℕ) → triangle n < triangle (suc n)
+  triangleN<triangleSN n = n , refl
+
+private
+  1+k+t=k+t+1 : (n : ℕ) → (t : ℕ ) → suc (n + t) ≡ n + suc t
+  1+k+t=k+t+1 n t = solveℕ!
+  1+k+tk=tsk : (n : ℕ) → suc (n + triangle n) ≡ triangle (suc n)
+  1+k+tk=tsk n = 1+k+t=k+t+1 n (triangle n)
+
+  partitionTriangle = partition triangle refl strictIncTriangle
+
+  Triangle⊂ℕ×ℕ≅partitionTriangle : Iso Triangle⊂ℕ×ℕ partitionTriangle
+  Iso.fun Triangle⊂ℕ×ℕ≅partitionTriangle (k , i , i≤k) = k , i , i+tk<tsk where
+      i+tk<tsk : i + triangle k < triangle (suc k)
+      i+tk<tsk = i + triangle k <≤⟨ suc-≤-suc (≤-+k {k = triangle k} i≤k) ⟩
+                 k + triangle k <≡⟨ <-suc ⟩ 1+k+tk=tsk k
+
+  Iso.inv Triangle⊂ℕ×ℕ≅partitionTriangle (k , i , i+tk<tsk) = k , i , i≤k where
+      i+tk<k+tk+1 : i + triangle k < suc (k + triangle k)
+      i+tk<k+tk+1 = i + triangle k <≡⟨ i+tk<tsk ⟩ sym (1+k+tk=tsk k)
+      i+tk≤k+tk : i + triangle k ≤ k + triangle k
+      i+tk≤k+tk = pred-≤-pred i+tk<k+tk+1
+      i≤k : i ≤ k
+      i≤k = ≤-+k-cancel i+tk≤k+tk
+  Iso.rightInv Triangle⊂ℕ×ℕ≅partitionTriangle (k , i , _) = ΣPathP (refl , ΣPathPProp (λ _ → isProp≤) refl)
+  Iso.leftInv Triangle⊂ℕ×ℕ≅partitionTriangle  (k , i , _) = ΣPathP (refl , ΣPathPProp (λ _ → isProp≤) refl)
+
+  partitionTriangle≅ℕ : Iso partitionTriangle ℕ
+  partitionTriangle≅ℕ = partition≅ℕ triangle refl strictIncTriangle
+
+Triangle⊂ℕ×ℕ≅ℕ : Iso Triangle⊂ℕ×ℕ ℕ
+Triangle⊂ℕ×ℕ≅ℕ = (compIso Triangle⊂ℕ×ℕ≅partitionTriangle partitionTriangle≅ℕ)

Cubical/Data/Nat/Order.agda

@@ -96,6 +96,9 @@ suc-< p = pred-≤-pred (≤-suc p)
 ≤-predℕ {zero} = ≤-refl
 ≤-predℕ {suc n} = ≤-suc ≤-refl
 
+≤-reflexive : {m n : ℕ} → m ≡ n → m ≤ n
+≤-reflexive p = 0 , p
+
 ≤-trans : k ≤ m → m ≤ n → k ≤ n
 ≤-trans {k} {m} {n} (i , p) (j , q) = i + j , l2 ∙ (l1 ∙ q)
   where
@@ -200,6 +203,15 @@ predℕ-≤-predℕ {suc m} {suc n} ineq = pred-≤-pred ineq
 <-+-≤ : m < n → k ≤ l → m + k < n + l
 <-+-≤ p q = <≤-trans (<-+k p) (≤-k+ q)
 
+<-suc : {n : ℕ} → n < suc n
+<-suc = 0 , refl
+
+<SumLeft : {n k : ℕ} → n < n + suc k
+<SumLeft {n} {k} = k , +-suc k n ∙ +-comm (suc k) n
+
+<SumRight : {n k : ℕ} → n < suc k + n
+<SumRight {n} {k} = k , +-suc k n
+
 ¬squeeze< : {n m : ℕ} → ¬ (n < m) × (m < suc n)
 ¬squeeze< {n = n} ((zero , p) , t) = ¬m<m (subst (_< suc n) (sym p) t)
 ¬squeeze< {n = n}  ((suc diff1 , p) , q) =
@@ -545,3 +557,36 @@ pattern s<s {m} {n} m<n = s≤s {m} {n} m<n
 ≤-∸-≥ n (suc l)  zero   r = ⊥.rec (¬-<-zero r)
 ≤-∸-≥  zero   (suc l) (suc k) r = ≤-refl
 ≤-∸-≥ (suc n) (suc l) (suc k) r = ≤-∸-≥ n l k (pred-≤-pred r)
+
+-- Some facts about increasing functions
+
+isStrictlyIncreasing : (f : ℕ → ℕ) → Type
+isStrictlyIncreasing f = {m n : ℕ} → (m < n) → f m < f n
+
+isIncreasing : (f : ℕ → ℕ) → Type
+isIncreasing f = {m n : ℕ} → m ≤ n → f m ≤ f n
+
+strictlyIncreasing→Increasing : {f : ℕ → ℕ} → isStrictlyIncreasing f → isIncreasing f
+strictlyIncreasing→Increasing {f} fInc {m} {n} m≤n = case (≤-split m≤n) of
+  λ { (inl m<n) → <-weaken  (fInc m<n)
+    ; (inr m=n) → ≤-reflexive (cong f m=n) }
+
+module _ (f : ℕ → ℕ) (fInc : ((n : ℕ) → f n < f (suc n))) where
+  open <-Reasoning
+  sucIncreasing→StrictlyIncreasing : isStrictlyIncreasing f
+  sucIncreasing→StrictlyIncreasing {m = m} {n = n} (k , m+k+1=n) =
+    sucIncreasing→strictlyIncreasing' m n k m+k+1=n where
+
+      sucIncreasing→strictlyIncreasing' :
+        (m : ℕ) → (n : ℕ) → (k : ℕ) → (k + suc m ≡ n) → f m < f n
+
+      sucIncreasing→strictlyIncreasing' m _ zero m+1=n =
+        subst (λ n' → f m < f n') m+1=n (fInc m)
+
+      sucIncreasing→strictlyIncreasing' m _ (suc k) sk+sm=n =
+        subst (λ n' → f m < f n') sk+sm=n $
+          f m
+            <⟨ sucIncreasing→strictlyIncreasing' m (k + suc m) k refl ⟩
+          f (k + suc m)
+            <≡⟨ fInc (k + suc m) ⟩
+          f (suc k + suc m) ∎