如何比較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 *)