如何比较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} 

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

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 

Answer 2

如果你要进去勒柯克实际运行字符串比较，我建议使用布尔版本：

From Coq Require Import Bool Ascii String. 

Definition eq_ascii (a1 a2 : ascii) := 
    match a1, a2 with 
    | Ascii b1 b2 b3 b4 b5 b6 b7 b8, Ascii c1 c2 c3 c4 c5 c6 c7 c8 => 
    (eqb b1 c1) && (eqb b2 c2) && (eqb b3 c3) && (eqb b4 c4) && 
    (eqb b5 c5) && (eqb b6 c6) && (eqb b7 c7) && (eqb b8 c8) 
    end. 

Fixpoint eq_string (s1 s2 : string) := 
    match s1, s2 with 
    | EmptyString, EmptyString => true 
    | String x1 s1, String x2 s2 => eq_ascii x1 x2 && eq_string s1 s2 
    | _, _      => false 
    end. 

他们在我的测试中通常快3倍，但如果涉及hnf策略（这可能在样张中），则可能是一个数量级。

Time Compute if string_dec 
    "Hola como te llamas amigo? Hola como te llamas amigo? Hola como te llamas amigo? 
     Hola como te llamas amigo? Hola como te llamas amigo? Hola como te llamas amigo? 
    " 
    "Hola como te llamas amigo? Hola como te llamas amigo? Hola como te llamas amigo? 
     Hola como te llamas amigo? Hola como te llamas amigo? Hola como te llamas amigo? 
    " then 1 else 0. 
(* around 0.015 *) 

Time Compute eq_string 
    "Hola como te llamas amigo? Hola como te llamas amigo? Hola como te llamas amigo? 
     Hola como te llamas amigo? Hola como te llamas amigo? Hola como te llamas amigo? 
    " 
    "Hola como te llamas amigo? Hola como te llamas amigo? Hola como te llamas amigo? 
     Hola como te llamas amigo? Hola como te llamas amigo? Hola como te llamas amigo? 
    ". 
(* around 0.005 *)