如何证明关于原始字符串的事情？答案

【问题标题】：How to prove things about primitive strings?如何证明关于原始字符串的事情？
【发布时间】：2026-01-16 07:35:01
【问题描述】：

在 Idris 上，无法对原始字符串执行模式匹配。因此，如何证明关于它们的事情并不明显。例如，此函数可能会返回一个字符列表的第一个字符是“a”的证明：

f : (l : List Char) -> Maybe (head' l = Just 'a')
f ('a' :: []) = Just Refl
f xs          = Nothing

这非常简单并且通过了类型检查器。但是，如果我们尝试为原生字符串实现相同的功能，我们将编写如下内容：

g : (s : String) -> Maybe (prim__strHead s = 'a')
g s = if prim__strHead s == 'a'
  then Just Refl 
  else Nothing

这无法进行类型检查，因为编译器显然不能仅仅从它通过prim__strHead s == 'a' 测试的事实得出结论prim__strHead s == 'a'。

因此，证明原始字符串的正确方法是什么？

【问题讨论】：

不要使用Maybe作为证明，而是使用Dec: f : (l : List Char) -> Dec (head' l = Just 'a') f ('a' : : xs) = 是 Refl f [] = 不荒谬
@asandroq 任何解释什么是Dec 以及何时/为什么要使用它的链接？

标签： idris

【解决方案1】：

按照 IRC 的建议，您可以使用 Data.String.Views.strList 对字符串进行模式匹配：

import Data.String.Views

g : (s : String) -> ...
g s with (strList s) 
 g ""            | SNil = ?no
 g (strCons x _) | SCons x _ with (decEq x 'a') 
   g (strCons 'a' _) | SCons 'a' _ | Yes Refl = ?yes
   g (strCons  x  _) | SCons  x  _ | No contra = ?no2

【讨论】：