如何在Coq中创建可用于函数或变量的具体字符串？

Coq的字符串系统基于归纳类型，和常规编程语言的原生字符串逻辑不同，默认打印会显示构造子而非友好字面量，以下是具体解决步骤：

1. 正确导入库并开启字符串作用域 #

首先导入标准库的String模块，同时开启字符串作用域，这样才能直接用双引号写字面量：

Require Import String.
Open Scope string_scope.

2. 让Compute输出友好的字符串字面量 #

默认情况下，Compute会输出字符串的归纳构造形式（比如String "h" (String "e" ...)），开启以下设置可以让它显示熟悉的双引号格式：

Set Printing Strings.

现在测试：

Definition my_str := "hello world".
Compute my_str. (* 输出："hello world" *)

3. 创建可传递/存储的字符串变量 #

直接用Definition或Let绑定字符串到变量，就能传给自定义函数或存储：

(* 定义字符串变量 *)
Let greet := "Hello".
Definition name := "Alice".

(* 自定义接收字符串的函数 *)
Definition combine_greet (g n : string) := g ++ ", " ++ n ++ "!".

(* 调用函数并计算结果 *)
Compute combine_greet greet name. (* 输出："Hello, Alice!" *)

4. 常用字符串操作示例 #

利用String库自带的函数可以完成基础操作：

• 拼接：Compute "foo" ++ "bar". → "foobar"
• 获取长度：Compute length "test". → 4
• 按索引取字符（索引从0开始，默认返回指定默认字符）：Compute nth 2 "abcde" "?". → "c"
• 字符转字符串：Compute String "x" EmptyString. → "x"

关于自定义"符号"的补充 #

如果你的需求是创建可复用的符号标识，直接用Definition绑定字符串即可，比如：

Definition error_symbol := "[ERROR]".
Compute error_symbol ++ " Invalid input". (* 输出："[ERROR] Invalid input" *)

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