# Recursive definitions best practices

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.
``````

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.

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

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.

I did something like that here:

substring search game

Ian