Recursive definitions best practices

Using Coq
1

Hi all. I am returning to Coq after a long pause, and I am wondering what are the best practices when it comes to defining recursive functions.
In my situation, I am trying to write a function that checks if a needle string is a substring of a haystack.
I can think of at least 7 different ways of expressing that, using either Inductive or Fixpoint, Prop or bool and whatnot.
Ultimately I want to write an optimized function that does the same thing, and to prove it’s correct w.r.t a naive and obviously correct function.
Here’s my progress so far:

Inductive sub_1 : string -> string -> Prop :=
| S1 : forall pre post needle, sub_1 needle (pre ++ needle ++ post)%string
.

Inductive sub_2 : string -> string -> Prop :=
| S2_Prefix : forall needle haystack, prefix_1 needle haystack -> sub_2 needle haystack
| S2_pN : forall needle haystack c, sub_2 (String c needle) haystack -> sub_2 needle haystack
.

Inductive sub_3 : string -> string -> Prop :=
| S3_Prefix : forall needle haystack, prefix_1 needle haystack -> sub_3 needle haystack
| S3_sH : forall needle haystack, sub_3 needle haystack -> forall c, sub_3 needle (String c haystack)
.

Inductive sub_4 : string -> string -> Prop :=
| S4 : forall needle haystack pre post, haystack = (pre ++ needle ++ post)%string -> sub_4 needle haystack
.

Fixpoint sub_5 needle haystack :=
  match needle, haystack with
  | EmptyString, _ => true
  | _, EmptyString => false
  | _, String _ haystack' => (prefix needle haystack || sub_5 needle haystack')%bool
  end.

Fixpoint sub_6 needle haystack :=
  match needle, haystack with
  | EmptyString, _ => True
  | _, EmptyString => False
  | _, String _ haystack' => prefix needle haystack = true \/ sub_6 needle haystack'
  end.

Fixpoint sub_7 needle haystack :=
  match haystack with
  | EmptyString => needle = EmptyString
  | String _ haystack' => prefix needle haystack = true \/ sub_7 needle haystack'
  end.

Fixpoint sub_optimized (needle haystack : string) :=
  (* Needs to be extractable to OCaml *) True
.

Theorem correct : forall needle haystack, sub_optimized needle haystack <-> sub_? needle haystack.
Proof.
Admitted.

Also it could be noted that I use the standard library’s prefix function here, but I could also define it in the Prop “space” if needed.

2

sub_1 or Definition sub needle haystack := exists pre post, haystack = (pre ++ needle ++ post)%string. feel more like a specification than the others.

3

I agree with SkySkimmer that sub_1 or an equivalent definition are the ones that look the most like specs to me.

However, depending on your usage, you might still want to introduce something like sub_2 or sub_3 and show its equivalence with sub_1. Indeed, these come with an induction principle, and depending on what you want to do with you specification, having such an induction principle at hand might make some proofs more streamlined. An alternative to this would be to show directly that sub_1 satisfies the induction principle of sub_2 and/or sub_3.

The good part about having some sub_5 or sub_6 at hand is that they give you an executable reference implementation, which you might want to use in tests – but if you end up giving an optimized version and showing its equivalence with the spec, then this has relatively little value.

4

I did something like that here:

substring search game

–
Ian