How do I compare two ASCII strings in Coq?

Question

I want to compare two ASCII strings s1 and s2 in Coq.

It seems like the standard library contains no functions for this purpose?

What is the canonical way of proving strings equal?

Answer 1

You can use the string_dec function, which decides (hence the suffix _dec) if two strings are equal. Incidentally, this name slightly violates the usual Coq naming style -- it should've been named string_eq_dec -- _eq_dec stands for decidable equality. string_dec has the following type:

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

Let me provide a concrete example. Coq lets you use string_dec in if-expressions like an ordinary boolean value:

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

If you are going to actually run string comparison inside Coq, I recommend to use the boolean versions:

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.

They are usually 3x faster in my tests, but can be one order of magnitude if the hnf strategy is involved (which happens in proofs).

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 *)