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
private
2Sn=2n+2 : {n : ℕ} → doubleℕ (suc n) ≡ doubleℕ n + 2
2Sn=2n+2 = +-comm 2 (doubleℕ _)
doubleGrows : (n : ℕ) → doubleℕ n < doubleℕ (suc n)
doubleGrows n = <-trans <-suc <-suc
¬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 (doubleℕ 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 , <-suc
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ℕ≅ℕ