The Coq mailing list

[Randy Pollack <rpollack0 AT gmail.com>]

Hi Jason,

This is a good question.

On a slightly different point, much can be gained by paying attention
to the structures being compared.  E.g strings can be long lists of
ascii, so optimizing ascii comparison can make a measurable
difference.

Here is what I have been using for string comparison:

Definition xor (b1 b2:bool) : bool :=
  match b1, b2 with
    | true, true => true
    | false, false => true
    | _, _ => false
  end.
Definition ascii_dec_bool (a b:ascii): bool :=
  match a, b with
    | Ascii a0 a1 a2 a3 a4 a5 a6 a7,
      Ascii b0 b1 b2 b3 b4 b5 b6 b7 =>
      andb (andb (andb (xor a0 b0) (xor a1 b1))
                 (andb (xor a2 b2) (xor a3 b3)))
           (andb (andb (xor a4 b4) (xor a5 b5))
                 (andb (xor a6 b6) (xor a7 b7)))
  end.
Function string_eq_bool (a1 a2:string) : bool :=
  match a1, a2 with
    | String b1 (String b2 bs), String c1 (String c2 cs) =>
      (ascii_dec_bool b1 c1) && (ascii_dec_bool b2 c2) &&
                             (string_eq_bool bs cs)
    | String b bs, String c cs =>
      (ascii_dec_bool b c) && (string_eq_bool bs cs)
    | EmptyString, EmptyString => true
    | _, _ => false
  end.

This is entirely ad hoc, based on intuition, but measures to be much
faster than String.string_dec.

Best,
--Randy

On Thu, Dec 22, 2016 at 11:39 PM, Jason Gross 
<jasongross9 AT gmail.com>
 wrote:
> Hey,
>
> Are there any case studies (or informal studies) on the relative performance
> of *_beq vs *_eq_dec in vm_compute, assuming that the proofs are unused and
> all that's done is a case on the result?  I've been sticking to the *_beq
> lemmas, at a slight proof-obligation overhead, based on a hunch that they're
> somewhat more efficient than *_eq_dec (and certainly they shouldn't be any
> slower), but I'm curious if anyone has concrete numbers or graphs.
>
> Thanks,
> Jason