agda - 如何在 Agda 中将安全的 `length` 函数写入 `Vec`？

Question

因为我们有 Data.Vec ，我们知道什么Vec是。

我想证明 Nat 和 Vec 是同构的。

我已经成功创建了一个证明 Nat 可以转换为 Vec 的函数:

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

而当我试图写一个相应的 vec→ℕ ， 我失败了。

我想写这样的东西(它不能编译但它是可读的):

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

在第一个代码中，确保参数正好是返回值的长度。
但是，如何确保第一个参数的长度恰好是返回值？

Answer 1

我不知道这是否是最好的解决方案，但这是我想出来的。

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

而不是说结果正是 n , 我已经引入了一个等式来指定这样的函数返回一个 m ，使得 n ≡ m .希望对你有帮助。使用您的类型签名，我有一个解析错误并开发了这个。