How should the left and the right inverse for binary conversion be proved?

Question

{-# OPTIONS --cubical #-}

open import Cubical.Core.Everything
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Data.Nat
open import Data.Product using (_,_; _×_)

data Pos : Set where
  one : Pos
  2*_ : Pos → Pos
  2*_+1 : Pos → Pos

_+1 : Pos → Pos
one +1 = 2* one
(2* d) +1 = 2* d +1
(2* d +1) +1 = 2* (d +1)

ℕ→Pos : ℕ → Pos
ℕ→Pos zero = one
ℕ→Pos (suc n) = ℕ→Pos n +1

data Bin : Set where
  zero : Bin
  Pos→Bin : Pos → Bin

ℕ→Bin : (n : ℕ) → Bin
ℕ→Bin (suc n) = Pos→Bin (ℕ→Pos n)
ℕ→Bin zero = zero

Pos→ℕ : Pos → ℕ
Pos→ℕ one = 1
Pos→ℕ (2* x) = 2 * (Pos→ℕ x)
Pos→ℕ (2* x +1) = suc (2 * (Pos→ℕ x))

Bin→ℕ : Bin → ℕ
Bin→ℕ zero = 0
Bin→ℕ (Pos→Bin x) = Pos→ℕ x

ℕ≃Bin : ℕ ≃ Bin
ℕ≃Bin = isoToEquiv (iso ℕ→Bin Bin→ℕ ℕ→Bin→ℕ-inv Bin→ℕ→Bin-inv) where
  ℕ→Bin→ℕ-inv : (x : Bin) → ℕ→Bin (Bin→ℕ x) ≡ x
  ℕ→Bin→ℕ-inv zero i = zero
  ℕ→Bin→ℕ-inv (Pos→Bin one) i = Pos→Bin one
  ℕ→Bin→ℕ-inv (Pos→Bin (2* x)) i = {!!}
  ℕ→Bin→ℕ-inv (Pos→Bin (2* x +1)) i = {!!}

  Bin→ℕ→Bin-inv : (x : ℕ) → Bin→ℕ (ℕ→Bin x) ≡ x

This is related to the first part of the intro to Agda paper. I am quite sure I could do this in Coq and probably regular Agda, but as it turns out not knowing even the basics of theorem proving in a new type system makes things a lot harder and I am not sure how to proceed here. I definitely need to see some moderately complex beginner's examples before I can get a grasp on this.

There is in fact a Cubical.Data.BinNat module in the Cubical library that has all the proofs for binary conversion in cubical style. This answers my question. — Marko Grdinić

Marko Grdinić Marko Grdinić · Accepted Answer · 2019-08-08T12:47:45

Here is the regular Agda solution to the question I posed to show that I am not being lazy. This exercise was not that easy. I said that this would be easy in Coq, but I am not that sure anymore even though I have over 2 months of experience in it and only two weeks in Agda. Agda was really smart while proving the ℕ→Pos→ℕ-inv part.

During the proving of ℕ→Pos→ℕ-inv (2* x) with Pos→ℕ x | ℕ→Pos→ℕ-inv x and ℕ→Pos→ℕ-inv 2* x +1 with Pos→ℕ x | ℕ→Pos→ℕ-inv x, I was surprised to see that it knew that suc n was the only possible case for Pos→ℕ x. After that I had trouble figuring out how to prove Pos→Bin a ≡ Pos→Bin b → a ≡ b. Injectivity depends on the what the function's construction and I did not think that just inverting the equality would be enough to make it go through, but it was and it made things a lot easier. It allowed me to add ℕ→Pos→ℕ-inv x in the with pattern and then invert it. Edit: Uf, now I realize the reason why it worked is because Pos→Bin is not a function, but a constructor. I got too smart with the syntax.

import Relation.Binary.PropositionalEquality as Eq
open Eq
open Eq.≡-Reasoning
open import Data.Nat
open import Data.Nat.Properties
open import Data.Product

data Pos : Set where
  one : Pos
  2*_ : Pos → Pos
  2*_+1 : Pos → Pos

_+1 : Pos → Pos
one +1 = 2* one
(2* d) +1 = 2* d +1
(2* d +1) +1 = 2* (d +1)

ℕ→Pos : ℕ → Pos
ℕ→Pos zero = one
ℕ→Pos (suc n) = ℕ→Pos n +1

data Bin : Set where
  zero : Bin
  Pos→Bin : Pos → Bin

ℕ→Bin : (n : ℕ) → Bin
ℕ→Bin (suc n) = Pos→Bin (ℕ→Pos n)
ℕ→Bin zero = zero

Pos→ℕ : Pos → ℕ
Pos→ℕ one = 1
Pos→ℕ (2* x) = Pos→ℕ x + Pos→ℕ x
Pos→ℕ (2* x +1) = suc (Pos→ℕ x + Pos→ℕ x)

Bin→ℕ : Bin → ℕ
Bin→ℕ zero = 0
Bin→ℕ (Pos→Bin x) = Pos→ℕ x

ℕ→Pos≡dup : ∀ n → ℕ→Pos (n + n) +1 ≡ 2* (ℕ→Pos n)
ℕ→Pos≡dup zero = refl
ℕ→Pos≡dup (suc n) =
  ℕ→Pos (n + suc n) +1 +1
    ≡⟨ subst (λ x → ℕ→Pos x +1 +1 ≡ ℕ→Pos (n + n) +1 +1 +1) (+-comm (suc n) n) refl ⟩
  ℕ→Pos (n + n) +1 +1 +1
    ≡⟨ cong (λ x → x +1 +1) (ℕ→Pos≡dup n) ⟩
  (2* (ℕ→Pos n)) +1 +1
    ≡⟨⟩
  2* (ℕ→Pos n +1)
    ∎

ℕ→Pos→ℕ-inv : (x : Pos) → ℕ→Bin (Pos→ℕ x) ≡ Pos→Bin x
ℕ→Pos→ℕ-inv one = refl
ℕ→Pos→ℕ-inv (2* x) with Pos→ℕ x | ℕ→Pos→ℕ-inv x
ℕ→Pos→ℕ-inv (2* .(ℕ→Pos n)) | suc n | refl = 
  cong Pos→Bin (
    ℕ→Pos (n + suc n)
      ≡⟨ subst (λ v → ℕ→Pos v ≡ ℕ→Pos (n + n) +1) (+-comm (suc n) n) refl ⟩
    ℕ→Pos (n + n) +1
      ≡⟨ ℕ→Pos≡dup n ⟩
    2* ℕ→Pos n
    ∎)
ℕ→Pos→ℕ-inv 2* x +1 with Pos→ℕ x | ℕ→Pos→ℕ-inv x
ℕ→Pos→ℕ-inv 2* .(ℕ→Pos n) +1 | suc n | refl =
  cong Pos→Bin (
    ℕ→Pos (n + suc n) +1
      ≡⟨ subst (λ v → ℕ→Pos v +1 ≡ ℕ→Pos (n + n) +1 +1) (+-comm (suc n) n) refl ⟩
    ℕ→Pos (n + n) +1 +1
      ≡⟨ cong (_+1) (ℕ→Pos≡dup n) ⟩
    2* ℕ→Pos n +1
    ∎)

ℕ→Bin→ℕ-inv : (x : Bin) → ℕ→Bin (Bin→ℕ x) ≡ x
ℕ→Bin→ℕ-inv zero = refl
ℕ→Bin→ℕ-inv (Pos→Bin x) = ℕ→Pos→ℕ-inv x

Pos→ℕ≡+1 : ∀ n → Pos→ℕ (n +1) ≡ suc (Pos→ℕ n)
Pos→ℕ≡+1 one = refl
Pos→ℕ≡+1 (2* n) = refl
Pos→ℕ≡+1 2* n +1 =
  Pos→ℕ (n +1) + Pos→ℕ (n +1)
    ≡⟨ subst (λ v → v + v ≡ suc (Pos→ℕ n) + suc (Pos→ℕ n)) (sym (Pos→ℕ≡+1 n)) refl ⟩
  suc (Pos→ℕ n) + suc (Pos→ℕ n)
    ≡⟨⟩
  suc (Pos→ℕ n + suc (Pos→ℕ n))
    ≡⟨ subst (λ v → suc v ≡ suc (suc (Pos→ℕ n + Pos→ℕ n))) (+-comm (suc (Pos→ℕ n)) (Pos→ℕ n)) refl ⟩
  suc (suc (Pos→ℕ n + Pos→ℕ n))
    ∎

Bin→ℕ→Bin-inv : (x : ℕ) → Bin→ℕ (ℕ→Bin x) ≡ x
Bin→ℕ→Bin-inv zero = refl
Bin→ℕ→Bin-inv (suc zero) = refl
Bin→ℕ→Bin-inv (suc (suc x)) =
  Pos→ℕ (ℕ→Pos x +1)
    ≡⟨ Pos→ℕ≡+1 (ℕ→Pos x) ⟩
  suc (Pos→ℕ (ℕ→Pos x))
    ≡⟨ cong suc (Bin→ℕ→Bin-inv (suc x)) ⟩
  suc (suc x)
    ∎

How should the left and the right inverse for binary conversion be proved?

1 Answers