```
{-# OPTIONS --cubical-compatible #-}
module Padova2025.VerifiedAlgorithms.Binary where
```

# Case study: Binary representation of natural numbers

We have defined the natural numbers in an unary manner, freely generating ℕ by
`zero` and `succ`; this approach is logically pleasing, but computationally
inefficient. Let us introduce binary representations of natural numbers, define
the basic arithmetical operations on binary representations, and then prove
these operations correct with respect to the unary model.

```
open import Padova2025.ProgrammingBasics.Naturals.Base
open import Padova2025.ProgrammingBasics.Naturals.Arithmetic
open import Padova2025.ProgrammingBasics.Booleans
open import Padova2025.ProgrammingBasics.Lists
open import Padova2025.ProvingBasics.Negation
open import Padova2025.ProvingBasics.Equality.Base
open import Padova2025.ProvingBasics.Equality.General
open import Padova2025.ProvingBasics.Equality.NaturalNumbers
open import Padova2025.ProvingBasics.Equality.Reasoning.Core
```

A binary representation is just a list of zeros and ones (with leading zeros allowed):

```
BitString : Set
BitString = List Bool
```

For instance, we represent the number 12 (binary `1100`) as `false ∷ false ∷
true ∷ true ∷ []`, i.e. with the least significant bit in the front. Every bit
string represents some natural number:

```
decode : BitString → ℕ
decode = {!!}
```


## Exercise: Binary successor

Implement the successor operation on bit strings, then prove it correct with
respect to the model.

```
succᵇ : BitString → BitString
succᵇ = {!!}
```

```
succᵇ-correct : (xs : BitString) → decode (succᵇ xs) ≡ succ (decode xs)
succᵇ-correct = {!!}
```


## Exercise: Encoding natural numbers

Implement a function which encodes a given natural number as a bit
string, then prove your implementation correct.

```
encode : ℕ → BitString
encode = {!!}
```

::: Hint :::
The function `succᵇ` from above might come in handy.
:::

```
decode-encode : (x : ℕ) → decode (encode x) ≡ x
decode-encode = {!!}
```


## Exercise: Uniqueness of binary representations

Every natural number admits infinitely many binary representations, as
we can always add trailing zeros. Let us prove that such trailing
zeros are the only source of non-uniqueness of binary representations.

To this end, we first define a predicate `AllZero : BitString → Set`
expressing that a given bit string consists just of zeros. Think about
how this could be done, then have a look at the following reference
definition.

::: More :::
```
data AllZero : BitString → Set where
  triv : AllZero []
  cons : {xs : BitString} → AllZero xs → AllZero (false ∷ xs)
```
:::

With the predicate `AllZero` at hand, we can define what it means that
two bit strings are equivalent:

```
infix 4 _≈_
data _≈_ : BitString → BitString → Set where
  base : {xs ys : BitString} → AllZero xs → AllZero ys → xs ≈ ys
  -- "Equivalent because both strings just consist of zeros."

  cons : {xs ys : BitString} {b : Bool} → xs ≈ ys → b ∷ xs ≈ b ∷ ys
  -- "Equivalent because both strings have the same least significant digit,
  -- and then continue in an equivalent manner."
```

As a warm-up, let us prove that equivalent bit strings represent the
same natural number.

```
decode-allZero : {xs : BitString} → AllZero xs → decode xs ≡ zero
decode-allZero = {!!}
```

```
decode-≈ : {xs ys : BitString} → xs ≈ ys → decode xs ≡ decode ys
decode-≈ = {!!}
```

Now let us prove that bit strings which represent the same number are equivalent.

```
unique-zero : {xs : BitString} → decode xs ≡ zero → AllZero xs
unique-zero = {!!}
```

```
unique : {xs ys : BitString} → decode xs ≡ decode ys → xs ≈ ys
unique = {!!}
```


## Exercise: Binary addition

Implement the addition operation on bit strings, then prove it correct with respect to the unary model.

```
addᵇ : BitString → BitString → BitString
addᵇ = {!!}
```

```
addᵇ-correct : (xs ys : BitString) → decode (addᵇ xs ys) ≡ decode xs + decode ys
addᵇ-correct = {!!}
```


## Exercise: Commutativity of binary addition

Let us check, without using that addition of natural numbers is
commutative, that `addᵇ` is commutative:

```
addᵇ-comm : (xs ys : BitString) → addᵇ xs ys ≡ addᵇ ys xs
addᵇ-comm = {!!}
```

Alternatively, we could also translate to the unary model and use the
commutativity of `_+_`:

```
addᵇ-comm' : (xs ys : BitString) → addᵇ xs ys ≈ addᵇ ys xs
addᵇ-comm' = {!!}
```

As a curiosity, we can rederive commutativity of addition in the unary model, by
translating to binary representations and using commutativity of `addᵇ`:

```
+-comm' : (x y : ℕ) → x + y ≡ y + x
+-comm' = {!!}
```