Coq development to state the correctness of Knuth-Morris-Pratt string matching. A bit abortive so far :-)

kmp.v

Require Import Utf8.

Require Import Coq.Vectors.Fin.

Require Import Coq.Lists.List.

Open Scope list_scope.

Import ListNotations.

Notation "s '/:' n" := (skipn n s) (at level 60).

Notation "s ':/' n" := (firstn n s) (at level 60).

Notation "c1 '*=*' c2" := (Coq.Vectors.Fin.eqb c1 c2) (at level 70).

Parameter max_chr : nat.

Definition Char := Coq.Vectors.Fin.t max_chr.

Definition cstr : Type := list Char.

Fixpoint cstr_eq_dec (s1: cstr) (s2: cstr) :=
  match (s1, s2) with
  | ([ ], [ ]) => true
  | (_, [ ]) => false
  | ([], _) => false
  | (c1 :: r1, c2 :: r2) =>
  if c1 *=* c2 then cstr_eq_dec r1 r2 else false
  end.

Notation "s1 ':=:' s2" := (cstr_eq_dec s1 s2) (at level 70).

Definition slice (s: cstr) : (nat * nat) → cstr :=
  λ p , let (offset, len) := p in firstn len (skipn offset s)
.

Notation "s ':/:' p" := (slice s p) (at level 60).

Definition occurs_p (s1: cstr) (s2: cstr) (i: nat): bool :=
  let l1 := length s1 in s1 :=: s2 :/: (i, l1)
.

Definition natopt_lift f : option nat → option nat :=
  λ opt , match opt with
  | None => None
  | Some x => Some (f x)
  end.

Fixpoint brute (s1: cstr) (s2: cstr) : option nat := 
  match (s1, s2) with
  | ([ ], [ ]) => Some 0
  | (_, [ ]) => None
  | (_, _ :: rest) =>
  let l1 := length s1 in
    if s1 :=: s2 :/ l1 then Some 0
    else natopt_lift S (brute s1 rest)
  end.

Fixpoint mismatch (s1: cstr) (s2: cstr) : option nat :=
  match (s1, s2) with
  | ([ ], [ ]) => None
  | (_, [ ]) => Some 0
  | ([ ], _) => None
  | (c1 :: r1, c2 :: r2) =>
  if c1 *=* c2 then natopt_lift S (mismatch r1 r2)
  else Some 0
  end.

Definition partial_match_p (s1: cstr) (s2: cstr) : bool :=
  let l := min (length s1) (length s2) in
  s1 :/ l :=: s2 :/ l
.

Fixpoint min_partial_match (s1: cstr) (s2: cstr) (base: nat) :=
  match s2 with
  | [ ] => base
  | _ :: rest =>
  if partial_match_p s1 s2 then base
  else min_partial_match s1 rest (base + 1)
  end.

Fixpoint KMP_search_wf (skip: nat) (pat: cstr) (subject: cstr) : option nat :=
  match (pat, subject, skip) with
  | ([ ], _, _) => Some 0
  | (_, [ ], _) => None
  | (_, _ :: rest, S n) => KMP_search_wf n pat rest
  | (_ :: rpat, _ :: rest, 0) =>
    let nextfn l := min_partial_match (pat :/ (l+1)) (rpat :/ l) 0 in
    match mismatch pat subject with
    | None => Some 0
    | Some 0 => KMP_search_wf 0 pat rest
    | Some (S j) =>
      let next := nextfn j in
      KMP_search_wf next pat rest
    end
  end.

Definition KMP_search := KMP_search_wf 0.

Theorem KMP :
  ∀(pat subject : cstr) , KMP_search pat subject = brute pat subject.
Abort.