Software foundations extra Bin - Nat exercise

BinNat.agda

open import Function
open import Data.Nat
open import Relation.Binary.PropositionalEquality
open import Data.Nat.Properties.Simple
open import Data.Unit

data Bin : Set where
  zero : Bin
  2*n 2*n+1 : Bin → Bin

inc : Bin → Bin
inc zero = 2*n+1 zero
inc (2*n b) = 2*n+1 b
inc (2*n+1 b) = 2*n (inc b)

Bin-ℕ : Bin → ℕ
Bin-ℕ zero = zero
Bin-ℕ (2*n b) = let n = Bin-ℕ b in n + n
Bin-ℕ (2*n+1 b) = let n = Bin-ℕ b in suc n + n 

ℕ-Bin : ℕ → Bin
ℕ-Bin zero = zero
ℕ-Bin (suc n) = inc (ℕ-Bin n)

normalize : Bin → Bin
normalize zero = zero
normalize (2*n b) with normalize b
... | zero = zero
... | b' = 2*n b'
normalize (2*n+1 b) = 2*n+1 (normalize b)

-- Proof time !!!

inc-suc : ∀ b → Bin-ℕ (inc b) ≡ suc (Bin-ℕ b)
inc-suc zero = refl
inc-suc (2*n b) = refl
inc-suc (2*n+1 b) rewrite 
  inc-suc b | +-comm (Bin-ℕ b) (suc (Bin-ℕ b)) = refl

ℕ-id : ∀ n → n ≡ Bin-ℕ (ℕ-Bin n) 
ℕ-id zero = refl
ℕ-id (suc n) rewrite inc-suc (ℕ-Bin n) = cong suc (ℕ-id n)

norm-id1 : ∀ n → zero ≡ ℕ-Bin n → n ≡ 0
norm-id1 zero p = refl
norm-id1 (suc n) p with ℕ-Bin n
norm-id1 (suc n) () | zero
norm-id1 (suc n) () | 2*n b
norm-id1 (suc n) () | 2*n+1 b

norm-id2 : ∀ n → 2*n (inc (ℕ-Bin n)) ≡ inc (ℕ-Bin (n + suc n))
norm-id2 zero = refl
norm-id2 (suc n) rewrite 
  sym $ +-assoc n 1 (suc n) | +-comm n 1 
  | sym $ norm-id2 n = refl

norm-id3 : ∀ n → 2*n+1 (ℕ-Bin n) ≡ inc (ℕ-Bin (n + n))
norm-id3 zero = refl
norm-id3 (suc n) rewrite +-comm n (suc n) | sym $ norm-id3 n = refl

norm-id : ∀ b → normalize b ≡ ℕ-Bin (Bin-ℕ b)
norm-id zero = refl
norm-id (2*n b) with norm-id b | normalize b | inspect normalize b
norm-id (2*n b) | rec | zero | [ eq ]  with Bin-ℕ b
... | n with n + n | inspect (_+_ n) n | norm-id1 n (trans (sym eq) rec)
norm-id (2*n b) | rec | zero | [ eq ] | .0 | .0 | [ refl ] | refl = refl
norm-id (2*n b) | rec | 2*n nb | [ eq ] with Bin-ℕ b
... | suc n rewrite eq | rec = norm-id2 n
... | zero  rewrite rec with eq
... | ()
norm-id (2*n b) | rec | 2*n+1 nb | [ eq ] with Bin-ℕ b
... | suc n rewrite eq | rec = norm-id2 n
... | zero rewrite eq with rec
... | ()
norm-id (2*n+1 b) with norm-id b | normalize b | inspect normalize b
norm-id (2*n+1 b) | rec | nb | [ eq ] rewrite eq | rec = norm-id3 (Bin-ℕ b)