如何在Idris中对原生字符串进行属性证明？

这个问题确实戳中了Idris中原生字符串的一个核心痛点：作为底层实现的primitive类型，它们没法直接做模式匹配，而且普通布尔等式（==）和类型层面的命题相等（=）是完全脱节的——编译器没办法仅通过布尔检查的结果，自动推导出命题相等的证明项。

下面给你几个实用的解决方案：

1. 转成字符列表利用模式匹配 #

Idris的Data.String库提供了unpack函数，可以把原生字符串转换成List Char。既然列表支持模式匹配，我们就能复用你一开始处理列表的思路：

import Data.String

g : (s : String) -> Maybe (prim__strHead s = 'a')
g s with (unpack s)
  g s | [] = Nothing  -- 空字符串，没有首字符
  g s | ('a' :: _) = Just Refl  -- 首字符是'a'，Refl直接证明命题相等
  g s | (c :: _) = Nothing  -- 首字符不是'a'

这里的关键是：Idris标准库保证了unpack得到的列表首字符，和prim__strHead返回的结果是完全一致的，所以当我们匹配到'a' :: _时，Refl可以直接用来证明prim__strHead s = 'a'，编译器能顺利通过类型检查。

2. 用可判定相等（Decidable Equality）桥接布尔检查和命题证明 #

对于Char这种具有可判定相等性的类型，Idris提供了decEq函数，它能在类型层面判断两个值是否相等，并返回对应的证明（或否定证明）。我们可以用它来重构你的函数：

g : (s : String) -> Maybe (prim__strHead s = 'a')
g s = case decEq (prim__strHead s) 'a' of
  Yes prf => Just prf  -- prf就是`prim__strHead s = 'a'`的证明项
  No _ => Nothing      -- 不相等，返回Nothing

decEq x y会返回Yes prf（当x和y命题相等时，prf就是x = y的具体证明）或者No contra（当x和y不相等时，contra是一个矛盾证明）。用这个函数就能完美把运行时的相等检查，转换成类型层面的证明，编译器完全认可这种写法。

3. 手动封装原生操作的证明（进阶用法） #

如果你想更底层地处理，也可以手动构造一个辅助函数，把布尔检查和证明绑定起来。比如：

strHeadIs : (c : Char) -> (s : String) -> Maybe (prim__strHead s = c)
strHeadIs c s = if prim__strHead s == c then Just ?prf else Nothing

然后在Idris REPL里用:solve prf命令，让编译器自动帮你填充证明项（因为Char的可判定相等性，编译器能自动构造出对应的Refl）。不过这种方法不如前两种优雅，一般只在需要自定义底层逻辑时使用。

为什么你的原始代码不工作？ #

再补充解释一下：你写的if prim__strHead s == 'a' then Just Refl else Nothing里，==返回的是一个Bool值——这是运行时的布尔判断，而Refl需要的是类型层面的prim__strHead s = 'a'命题成立的证据。编译器没办法从“布尔值为真”推导出“命题相等成立”，除非你用decEq这样的可判定相等工具来桥接两者。

内容的提问来源于stack exchange，提问作者MaiaVictor