Increment binary value type by one

A quick correction of your algorithm

Your increment function is not correct. Considering your definition of binary numbers:

data Bin : Set where
  ⟨⟩ : Bin
  _O : Bin → Bin
  _I : Bin → Bin

Your increment function should be written as follows:

inc : Bin → Bin
inc ⟨⟩ = ⟨⟩ I
inc (x O) = x I
inc (x I) = (inc x) O

When the right number is zero, you just replace it by one, but you must not forget to keep the left part of the number.

When the right number is 1, you have to keep incrementing its left part, but you also need to transform this 1 into a 0.

A quick validation of the new algorithm

But, don't take my word for it, let us try and (partially) validate our function. After all, we are in a proof assistant, aren't we ?

A good way to validate such a function is to assess which property it should provide. The result of your incremental function has to be equal to 1 plus its input value. Agda provides natural numbers so let us transform your binary numbers into naturals to check such a property. First, some imports:

open import Data.Nat
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality

Then a function which transforms a binary number into a natural number:

_↑ : Bin → ℕ
⟨⟩ ↑ = 0
(x O) ↑ = x ↑ + x ↑
(x I) ↑ = suc (x ↑ + x ↑)

Finally, our validation property:

prop : ∀ {b} → (inc b) ↑ ≡ suc (b ↑)
prop {⟨⟩} = refl
prop {b O} = refl
prop {b I} rewrite prop {b} | +-suc (b ↑) (b ↑) = refl

This validation is of course incomplete (by nature) but at least it gives you confidence in your algorithm. You should always try and prove such assumptions when writing algorithms, which is the whole point of Agda (well, not the whole point, but at least part of it).

More on validation

To further make my point, I decided to try and keep validating your representation of binary numbers by implementing the reciprocal transformation from naturals to binary numbers:

_↓ : ℕ → Bin
zero ↓ = ⟨⟩
suc n ↓ = inc (n ↓)

We can directly prove that the two transformations are reciprocal when going up then down:

↑↓ : ∀ {n} → (n ↓) ↑ ≡ n
↑↓ {zero} = refl
↑↓ {suc n} rewrite prop {n ↓} | ↑↓ {n} = refl

Then I tried to do the other way around:

↓↑ : ∀ {b} → (b ↑) ↓ ≡ b
↓↑ {⟨⟩} = refl
↓↑ {b O} rewrite prop₂ {b ↑} rewrite ↓↑ {b} = refl
↓↑ {b I} rewrite prop₂ {b ↑} rewrite ↓↑ {b} = refl

This side needs prop₂ which has the following signature:

prop₂ : ∀ {n} → (n + n) ↓ ≡ (n ↓) O

This property should be true (in the sense that the binary numbers as we think of them should satisfy it), but it cannot be proven in your formalism because you can represent zero in an infinite number of ways, and all these ways are not prepositionally equal (for instance, the first case of prop₂ when n is equal to 0 requires to prove ⟨⟩ ≡ (⟨⟩ O) which cannot be proven).

All in all, validation not only allows us to find faulty algorithms (or to prove algorithms correct) but it can also reveal inconsistencies or mistakes in the basics of our theories themselves (even though in this case, a quick look could have been enough to see that 0 can be represented an infinite number of different manners).

As a side note, I am not saying that there should always be a single way of representing a specific element of an abstract data type, but it surely helps, especially when working with propositional equality, which is very often required.

On another side note, I am sorry if I got a little carried away but I find these kind of topics very enlightening regarding the use of proof assistants and formal validation.

Please feel free to ask for any further explanation.

The complete (and incomplete in a way) code

module BinaryNumber where

open import Data.Nat
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality

data Bin : Set where
  ⟨⟩ : Bin
  _O : Bin → Bin
  _I : Bin → Bin

inc : Bin → Bin
inc ⟨⟩ = ⟨⟩ I
inc (x O) = x I
inc (x I) = (inc x) O

_↑ : Bin → ℕ
⟨⟩ ↑ = 0
(x O) ↑ = x ↑ + x ↑
(x I) ↑ = suc (x ↑ + x ↑)

prop : ∀ {b} → (inc b) ↑ ≡ suc (b ↑)
prop {⟨⟩} = refl
prop {b O} = refl
prop {b I} rewrite prop {b} | +-suc (b ↑) (b ↑) = refl

_↓ : ℕ → Bin
zero ↓ = ⟨⟩
suc n ↓ = inc (n ↓)

↑↓ : ∀ {n} → (n ↓) ↑ ≡ n
↑↓ {zero} = refl
↑↓ {suc n} rewrite prop {n ↓} | ↑↓ {n} = refl

prop₂ : ∀ {n} → (n + n) ↓ ≡ (n ↓) O
prop₂ {zero} = {!!}
prop₂ {suc n} = {!!}

↓↑ : ∀ {b} → (b ↑) ↓ ≡ b
↓↑ {⟨⟩} = refl
↓↑ {b O} rewrite prop₂ {b ↑} rewrite ↓↑ {b} = refl
↓↑ {b I} rewrite prop₂ {b ↑} rewrite ↓↑ {b} = refl

The standard library

As a last remark, the binary numbers are present in the standard library in the file Data.Nat.Binary.Base with the associated properties (in particular the properties of reciprocity which are not provable in your representation) in the file Data.Nat.Binary.Properties if you feel like looking how they are implemented there.

When we define inc as Bin → Bin, we are saying that it takes values of type Bin and returns values of the same type i.e. Bin. Since we have 3 constructors available for creating Bin, all the values of type Bin would have one of the following 3 forms:

1. ⟨⟩
2. b I where b is some value of type Bin
3. b O where b is some value of type Bin

For case 1, since ⟨⟩ stands for zero.

inc ⟨⟩ = ⟨⟩ I

For case 2, we know that adding one to a number ending with zero will just change the last digit to one, so

inc (x O) = x I

and for case 3, when a number is ending with 1, on incrementing it we get zero at the end, and carryover is generated that needs to be passed forward. Carryover can be passed by using our same inc function. Assuming (inc x) gives a binary number, we take that output and append zero at the end.

inc (x I) = (inc x) O 

Also, just to extent upon the excellent answer given by MrO, who correctly pointed out that since there are infinitely many ways to represent zeros (and all numbers)

(b ↓) ↑ = b

can't be proved for b with leading zeros before the first significant digit. But if we restrict domain of ↓↑ to only binary numbers which are only canonical i.e binary number without any leading zeros, proof can be derived.

Proof of (b ↓) ↑ = b for canonical b

Extending MrO's code,

module BinaryNumber where

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

data Bin : Set where
  ⟨⟩ : Bin
  _O : Bin → Bin
  _I : Bin → Bin

inc : Bin → Bin
inc ⟨⟩ = ⟨⟩ I
inc (x O) = x I
inc (x I) = (inc x) O

_↑ : Bin → ℕ
⟨⟩ ↑ = 0
(x O) ↑ = x ↑ + x ↑
(x I) ↑ = suc (x ↑ + x ↑)

prop : ∀ {b} → (inc b) ↑ ≡ suc (b ↑)
prop {⟨⟩} = refl
prop {b O} = refl
prop {b I} rewrite prop {b} | +-suc (b ↑) (b ↑) = refl

_↓ : ℕ → Bin
zero ↓ = ⟨⟩ O
suc n ↓ = inc (n ↓)

↑↓ : ∀ {n} → (n ↓) ↑ ≡ n
↑↓ {zero} = refl
↑↓ {suc n} rewrite prop {n ↓} | ↑↓ {n} = refl


-- One b -> b start with ⟨⟩ I
data One : Bin → Set where

  first : One (⟨⟩ I)

  nextO  : ∀ { b : Bin }
        → One b
        ------------
        → One (b O)      

  nextI  : ∀ { b : Bin }
        → One b
        ------------
        → One (b I)


-- Can i.e Canonical representing binary numbers without extras leading zeros after ⟨⟩. For e.g ⟨⟩ O O I I and ⟨⟩ I I both represents binary form of number 3 but only ⟨⟩ I I is the canonical
data Can : Bin → Set where

  startWithZero : Can (⟨⟩ O)

  startWithOne : ∀ {b : Bin }
        → One b
        ------------
        → Can b


-- If m ≤ n then m ≤ (n + 1)
≤-sucʳ : ∀ {m n : ℕ }
       → m ≤ n
       -----------
       → m ≤ suc n
≤-sucʳ z≤n = z≤n
≤-sucʳ (s≤s m≤n) = s≤s (≤-sucʳ m≤n)


-- If m ≤ n then m ≤ (n + p)
≤-addʳ : ∀ (m n p : ℕ)
       → m ≤ n
       --------
       → m ≤ n + p
≤-addʳ m n zero m≤n rewrite +-comm n zero = m≤n
≤-addʳ m n (suc p) m≤n rewrite +-comm n (suc p) | +-comm p n  = ≤-sucʳ (≤-addʳ m n p m≤n)


-- If a natural number n has eqivalent binary form (⟨⟩ I b) then 1 ≤ n
1-≤-oneb : ∀ { b : Bin }
         → One b
         ---------
         → suc zero ≤ b ↑
1-≤-oneb first = s≤s z≤n
1-≤-oneb {b O} (nextO oneb) = ≤-addʳ 1 ((b ↑)) ((b ↑)) (1-≤-oneb oneb)
1-≤-oneb {b I} (nextI oneb) = ≤-sucʳ (≤-addʳ 1 ((b ↑)) ((b ↑)) (1-≤-oneb oneb))


-- If 0 ≤ (n + 1) then 1 ≤ n
0-≤-suc : ∀ (n : ℕ)
        → 0 ≤ suc n
        -----------
        → 1 ≤ suc n
0-≤-suc n z≤n = s≤s z≤n


-- If 1 ≤ n and binary form of n is b then binary form of (n + n) using ↓ is b O
↓-over-+ : ∀ (n : ℕ)
     → 1 ≤ n
     -----------------------
     → (n + n) ↓ ≡ (n ↓) O

↓-over-+ (suc zero) s≤n = refl
↓-over-+ (suc (suc n)) (s≤s s≤n)  = begin
                                 (suc (suc n) + (suc (suc n))) ↓
                               ≡⟨⟩
                                 inc (( suc n + (suc (suc n))) ↓)                      
                               ≡⟨ cong (inc) (cong (_↓) (+-comm (suc n) (suc (suc n)))) ⟩
                                 inc (inc ((suc n + suc n) ↓))
                               ≡⟨ cong (inc) (cong inc (↓-over-+ (suc n) (0-≤-suc n s≤n))) ⟩
                                 refl                               


-- For all binary numbers that are canonical, ↑↓ is identity (returns same b)
↑↓-canb : ∀ ( b : Bin )
      → Can b
      --------------
      → (b ↑) ↓ ≡ b


↑↓-canb _ startWithZero = refl
↑↓-canb _ (startWithOne first) = refl
↑↓-canb (b O) (startWithOne (nextO x)) rewrite ↓-over-+ (b ↑) (1-≤-oneb x) | ↑↓-canb b (startWithOne x) = refl
↑↓-canb (b I) (startWithOne (nextI x)) rewrite ↓-over-+ (b ↑) (1-≤-oneb x) | ↑↓-canb b (startWithOne x) = refl