A simple example of how to use Coq as a programming language - how to compute more efficient programs out of declarative programs, and then extract the efficient programs to ML. This facility is very obvious to serious users of Coq, but it took me a while as a beginner to realize this is practical and how can it be done. Compilers like Haskell d…

Opt.v

Require Import String.

Definition Parser (a : Type) :=
  string -> option (a * string).

Definition Return {a} (x: a) : Parser a :=
  fun s => Some (x, s).

Definition Bind {a b} (x: Parser a) (f: a -> Parser b) : Parser b :=
  fun s =>
    match x s with
      | None => None
      | Some (x, s) => f x s
    end.

Definition Map {a b} (f : a -> b) (x : Parser a) : Parser b :=
  Bind x (fun x => Return (f x)).

Definition MapOptimized {a b} (f: a -> b) (x: Parser a) : Parser b.
Proof.
  let r := (eval compute in (@Map a b f x)) in set (R := r).
  unfold Parser.
  apply R.
Defined.

Recursive Extraction MapOptimized.

On Coq 8.13, this needs Require Import Extraction. just before the extraction.