logic - Idris 中的 Forall 量词和复杂的 bool 命题

Question

我是依赖类型的新手，有 Haskell 经验，正在慢慢学习 Idris。作为练习，我想编写霍夫曼编码。目前我正在尝试编写一个证明，证明代码树的“扁平化”会产生一个前缀代码，但被量词卡住了。

我有一个简单的归纳命题，即一个列表是另一个列表的前缀:

using (xs : List a, ys : List a)
    data Prefix : List a -> List a -> Type where
        pEmpty : Prefix Nil ys
        pNext  : (x : a) -> Prefix xs ys -> Prefix (x :: xs) (x :: ys)

1. 这是一种有效的方法吗？或者类似“xs 是 ys 的前缀，如果存在 zs 这样 xs++ zs = ys"会更好吗？

2. 引入“forall”量词是否正确(据我所知，在 Agda 中它类似于 pNext : ∀ {x xs ys} → Prefix xs ys → Prefix (x::xs) (y::ys))？ pNext 第一个参数应该是隐式的吗？两种变体之间的语义差异是什么？

然后，我想为一个没有元素构成另一个元素的前缀的向量构建一个:

data PrefVect : Vect n (List a) -> Type where

空向量没有前缀:

    pvEmpty : PrefVect Nil

给定一个元素 x，一个向量 xs，并证明 xs 的任何元素都不是 x 的前缀(反之亦然)，x::xs 将拥有该属性:

    pvNext  : (x : [a]) -> (xs : Vect n [a]) ->
              All (\y => Not (Prefix x y)) xs ->
              All (\y => Not (Prefix y x)) xs ->
              PrefVect (x :: xs)

这是一个无效的类型，我希望在处理完第一个类型后修复它，但是在 pvNext 中也有关于量词的类似问题:这个变体是否可以接受，或者有更好的方法来形成“对关系的否定”？

谢谢。

Answer 1

我认为这里唯一的问题是您使用 [a] 作为 a 列表的类型，在 Haskell 风格中，而在 Idris 中它需要成为 List a。

你的 Prefix 类型对我来说看起来不错，虽然我会把它写成:

data Prefix : List a -> List a -> Type where
     pEmpty : Prefix [] ys
     pNext : Prefix xs ys -> Prefix (x :: xs) (x :: ys)

即 x 可以是隐式的，你不需要 using 因为 Idris 可以推断出 xs 和 是。这是否是正确的方法实际上取决于您打算将 Prefix 类型用于什么目的。测试一个列表是否是另一个列表的前缀当然很容易。像这样的东西:

testPrefix : DecEq a => (xs : List a) -> (ys : List a) -> Maybe (Prefix xs ys)
testPrefix [] ys = Just pEmpty
testPrefix (x :: xs) [] = Nothing
testPrefix (x :: xs) (y :: ys) with (decEq x y)
  testPrefix (x :: xs) (x :: ys) | (Yes Refl) = Just (pNext !(testPrefix xs ys
  testPrefix (x :: xs) (y :: ys) | (No contra) = Nothing

如果你想证明这个否定，你可能需要这样的类型:

testPrefix : DecEq a => (xs : List a) -> (ys : List a) -> Dec (Prefix xs ys)

我会把那个留作练习 :)。