How to write a safe `length` function to a `Vec` in Agda?

Question

Since we have Data.Vec, we know what Vec is.

I want to prove that Nat and Vec are isomorphic.

I've successfully created a function that proves Nat can be converted to Vec:

ℕ→vec : (n : ℕ) → Vec ⊤ n
ℕ→vec  zero   = []
ℕ→vec (suc a) = tt ∷ ℕ→vec a

While when I'm trying to write a corresponding vec→ℕ, I failed.

I want to write something like this (it doesn't compile but it's readable):

vec→ℕ : ∀ {n} → Vec ⊤ n → (n : ℕ)
vec→ℕ  []      = zero
vec→ℕ (tt ∷ a) = suc (vec→ℕ a)

In the first code, it's ensured that the argument is exactly the length of the return value. However, how can I ensure that the length of the first argument is exactly the return value?

Answer 1

I do not know, if it is the best solution, but is what I had figured out.

open import Data.Vec
open import Data.Unit
open import Data.Nat
open import Data.Product

open import Relation.Binary.PropositionalEquality

vec→ℕ : ∀ {n} → Vec ⊤ n → ∃ (λ m → n ≡ m)
vec→ℕ  []      = zero , refl
vec→ℕ (tt ∷ a) with vec→ℕ a
vec→ℕ (tt ∷ a) | m , refl = suc m , refl

Instead of saying that the result is exactly n, I've introduced a equality in order that specifies that such function return a m, such that n ≡ m. Hope that it helps you. Using your type signature, I've got a parse error and developed this.

Answer 2

You could make vec→ℕ definitionally equal to the length:

vec→ℕ : ∀ {n} → Vec ⊤ n → ℕ
vec→ℕ {n} _ = n

and then I think this is sufficiently transparent to Agda that anywhere you'd need the property that the ℕ you get is the right one, it will be available to you automatically (i.e. by reduction).

Edited to add: you might think this is underspecified, since vec→ℕ's type doesn't prescribe which exact ℕatural it returns. However, Agda sees through this definition, so e.g. you can prove the following external correctness proof if you need it (but I'd argue it doesn't add any value):

open import Relation.Binary.PropositionalEquality

vec→ℕ-correct : ∀ {n} {xs : Vec ⊤ n} → vec→ℕ xs ≡ n
vec→ℕ-correct = refl

Note that because vec→ℕ xs is definitionally equal to n, we don't need to look at either n or xs in the proof.