如何在Coq中比较两个ASCII字符串？

Question

我想在Coq中比较两个ASCII字符串s1和s2。

似乎标准库不包含用于此目的的函数？

证明字符串相等的规范方法是什么？

Answer 1

您可以使用该string_dec函数来确定（因此后缀为_dec）两个字符串是否相等。顺便说一句，此名称略有违反通常的Coq命名方式-应该命名string_eq_dec- _eq_dec代表可判定的相等性。string_dec具有以下类型：

string_dec
     : forall s1 s2 : string, {s1 = s2} + {s1 <> s2}

让我提供一个具体的例子。勒柯克让您使用string_dec在if像普通的布尔值-expressions：

Require Import String.
Open Scope string_scope.

Coq < Compute if string_dec "abc" "abc" then 1 else 0.
     = 1
     : nat

Coq < Compute if string_dec "ABC" "abc" then 1 else 0.
     = 0
     : nat