如何在Agda中为`Vec`写一个安全的`length`函数？

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,我已经引入了一个相等的顺序,指定这样的函数返回a m,这样n ? m.希望它能帮到你.使用你的类型签名,我有一个解析错误并开发了这个.

Answer 2

你可以在vec??定义上等于长度:

vec?? : ? {n} ? Vec ? n ? ?
vec?? {n} _ = n

然后我认为这对Agda来说是足够透明的,无论你需要哪个属性,?你得到的属性都是正确的,它会自动为你提供(即通过缩减).

编辑添加:您可能认为这是vec??未指定的,因为它的类型没有规定?它返回的确切的atural.但是,Agda会看到这个定义,所以例如,如果你需要,你可以证明以下外部正确性证明(但我认为它不会增加任何价值):

open import Relation.Binary.PropositionalEquality

vec??-correct : ? {n} {xs : Vec ? n} ? vec?? xs ? n
vec??-correct = refl

请注意,因为vec?? xs在定义上等于n,我们不需要查看任何一个n或xs在证明中.