standard bijections of Natural numbers

Cubical/Data/Nat/Bijections/FinN.agda

@@ -0,0 +1,53 @@
+module Cubical.Data.Nat.Bijections.FinN 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
+open import Cubical.Data.Nat.MoreOrderProperties
+
+Finℕ = Σ[ k ∈ ℕ ] Σ[ i ∈ ℕ ] (i ≤ k)
+
+triangle : ℕ → ℕ
+triangle zero = zero
+triangle (suc n) = n + suc (triangle n)
+
+increasingTriangle : isIncreasing triangle
+increasingTriangle = strengthenIncreasing 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 increasingTriangle
+
+  Finℕ≅partitionTriangle : Iso Finℕ partitionTriangle
+  Iso.fun Finℕ≅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 Finℕ≅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 Finℕ≅partitionTriangle (k , i , _) = ΣPathP (refl , ΣPathPProp (λ _ → isProp≤) refl)
+  Iso.leftInv Finℕ≅partitionTriangle  (k , i , _) = ΣPathP (refl , ΣPathPProp (λ _ → isProp≤) refl)
+
+  partitionTriangle≅ℕ : Iso partitionTriangle ℕ
+  partitionTriangle≅ℕ = partition≅ℕ triangle refl increasingTriangle
+
+Finℕ≅ℕ : Iso Finℕ ℕ
+Finℕ≅ℕ = (compIso Finℕ≅partitionTriangle partitionTriangle≅ℕ)

Cubical/Data/Nat/Bijections/IncreasingFunction.agda

@@ -0,0 +1,183 @@
+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.Nat.MoreOrderProperties
+
+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)
+
+isIncreasing : (f : ℕ → ℕ) → Type
+isIncreasing f = {m n : ℕ} → (m < n) → f m < f n
+
+weakenIncreasing : {f : ℕ → ℕ} → {m n : ℕ} → isIncreasing f → m ≤ n → f m ≤ f n
+weakenIncreasing {f} {m} {n} fInc m≤n = case (≤-split m≤n) of
+  λ { (inl m<n) → <-weaken  (fInc m<n)
+    ; (inr m=n) → transport (cong (λ { k → f m ≤ f k }) m=n) ≤-refl }
+
+strengthenIncreasing : (f : ℕ → ℕ) → ((n : ℕ) → f n < f (suc n)) → isIncreasing f
+strengthenIncreasing f fInc {m = m} {n = n} (k , m+k+1=n) =
+  strengthenIncreasing' f fInc m n k m+k+1=n where
+
+  strengthenIncreasing' : (f : ℕ → ℕ) → ((n : ℕ) → f n < f (suc n)) →
+                          (m : ℕ) → (n : ℕ) → (k : ℕ) → (k + suc m ≡ n) →
+                          f m < f n
+
+  strengthenIncreasing' f fInc m n zero    m+1=n   =
+    transport (cong (λ { n' → f m < f n' }) m+1=n  ) (fInc m)
+
+  strengthenIncreasing' f fInc m n (suc k) sk+sm=n =
+    transport (cong (λ { n' → f m < f n' }) sk+sm=n) (
+      f m
+        <⟨ strengthenIncreasing' f fInc m (k + suc m) k refl  ⟩
+      f (k + suc m)
+        <≡⟨ fInc (k + suc m) ⟩
+      f(suc k + suc m) ∎)
+
+private
+  kIsUnique : (f : ℕ → ℕ ) → isIncreasing 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)
+       ≤⟨ weakenIncreasing 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) → isIncreasing 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 = =→≤ 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 , =→≤ 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 : isIncreasing 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.FinN
+
+Finℕ≅ℕ×ℕ : Iso Finℕ (ℕ × ℕ)
+Iso.fun Finℕ≅ℕ×ℕ (_ , k , m , _) = m , k
+Iso.inv Finℕ≅ℕ×ℕ (m , k)         = m + k , k , m , refl
+Iso.rightInv Finℕ≅ℕ×ℕ _ = refl
+Iso.leftInv  Finℕ≅ℕ×ℕ (n , k , m , p) = J
+  (λ { n q → (Iso.inv Finℕ≅ℕ×ℕ (Iso.fun Finℕ≅ℕ×ℕ (n , k , m , q))) ≡ (n , k , m , q) }) refl p
+
+ℕ×ℕ≅ℕ : Iso (ℕ × ℕ) ℕ
+ℕ×ℕ≅ℕ = compIso (invIso Finℕ≅ℕ×ℕ) Finℕ≅ℕ

Cubical/Data/Nat/Bijections/Sum.agda

@@ -0,0 +1,75 @@
+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
+open import Cubical.Data.Nat.MoreOrderProperties
+
+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 : isIncreasing double
+doubleInc = strengthenIncreasing 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/MoreOrderProperties.agda

@@ -0,0 +1,20 @@
+module Cubical.Data.Nat.MoreOrderProperties where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Data.Nat
+open import Cubical.Data.Sigma
+open import Cubical.Data.Nat.Order
+open <-Reasoning
+open import Cubical.Tactics.NatSolver
+
+<SumLeft : {n k : ℕ } → n < n + suc (k)
+<SumLeft {n} {k} = k , solveℕ!
+
+<SumRight : {n k : ℕ } → n < suc (k) + n
+<SumRight {n} {k} = k , solveℕ!
+
+<-suc : {n : ℕ} → n < suc n
+<-suc = 0 , refl
+
+=→≤ : {m n : ℕ} → m ≡ n → m ≤ n
+=→≤ p = 0 , p