Verified Element Index

Prerequisites

A basic aptitude in Coq. Being able to complete all the non-advanced, non-optional exercises in the first 7 chapters of Logical Foundations (i.e. up to and including Inductively Defined Propositions (IndProp)) will suffice.

Task

The Haskell standard library provides a useful utility function elemIndex for searching for an element in a list and returning the index at which it first occurs (if it is present in the list) or reports that the element cannot be found in the list.

An implementation of elemIndex in Coq (renamed elem_index to better suit Coq naming conventions) is as follows:

Fixpoint elem_index {A : Type}
  (eq_dec : forall x y : A, {x = y} + {x <> y})
  (n : A) (l : list A) : option nat :=
  match l with
  | [] => None
  | x :: xs =>
      if eq_dec n x
        then Some O
        else
          match elem_index eq_dec n xs with
          | Some idx => Some (S idx)
          | None => None
          end
  end.

A complete specification of the (expected) behavior of elemIndex is as follows - given some element x that we want to search for and a list xs to search for x in:

• If elemIndex returns some index i then all of the following conditions must hold simultaneously:
  • The input list xs must contain at least i + 1 elements
  • The first i elements in xs cannot be x
  • The i + 1th element in xs must be x
• Otherwise, if elemIndex reports that x cannot be found in xs then xs cannot contain x

Convince yourself that the specification outlined above fully describes the expected behavior of elemIndex and then proceed to formally verify in Coq that the implementation of elemIndex given above correctly implements this specification.

Preloaded

The full source code of the Preloaded section is displayed below for your reference:

From Coq Require Import List.
Import ListNotations.

Fixpoint elem_index {A : Type}
  (eq_dec : forall x y : A, {x = y} + {x <> y})
  (n : A) (l : list A) : option nat :=
  match l with
  | [] => None
  | x :: xs =>
      if eq_dec n x
        then Some O
        else
          match elem_index eq_dec n xs with
          | Some idx => Some (S idx)
          | None => None
          end
  end.

Too easy?

Then here's an open challenge for you that you might find interesting ;-)