The Coq mailing list

[Adam Koprowski <adam.koprowski AT gmail.com>]

  ... or if you are not a huge fun of 'refine' and you don't like to define things by means of tactics, then the new Program feature of Coq is your friend. You can define your function in pretty much the same way as you'd do in some functional programming language and then you can prove properties about this function; and the two steps are nicely coupled together with Program (see solution below, which gives exactly the same program as the previous solution but I think the definitions & proofs are cleaner; although that's always a matter of taste). 

   Cheers,
    Adam

======
Require Import Coq.Lists.List.
Require Import Program.

Definition Decide (P : Prop) := { P } + { ~P }.

Section IsPrefix.

  Variable A : Type.
  Variable eqA_dec : forall x y : A, Decide (x = y).

  Definition is_prefix (pre list : list A) := exists tail, pre ++ tail = list.

  Program Fixpoint is_prefix_dec (pre list : list A) : Decide (is_prefix pre list) :=
    match pre with
    | nil => left _
    | cons x xs => 
        match list with
        | nil => right _
        | cons y ys => 
            if eqA_dec x y then
              match is_prefix_dec xs ys with
              | left _ => left _
              | right _ => right _
              end
            else
              right _
        end
    end.

  Next Obligation.
    exists list. auto.
  Qed.
  Next Obligation.
    intro xp. destruct xp. discriminate.
  Qed.
  Next Obligation.
    inversion wildcard'. exists x. subst. auto.
  Defined.
  Next Obligation.
    intro xp. destruct xp. simpl in H. apply wildcard'. exists x. congruence.
  Defined.
  Next Obligation.
    intro xp. destruct xp. simpl in H0. injection H0. auto.
  Qed.

End IsPrefix.

Extraction is_prefix_dec.

[...]
     Definition Prefix_dec (pre list : list A) : Prefix_spec pre list.
     refine (
       fix Prefix_dec (pre list : list A) : Prefix_spec pre list := _
     ).
     refine (
       match pre as pre return Prefix_spec pre list with
         | nil => left _ _
         | p :: ps => _
       end
     ).
[...]

-- 
=====================================================
Adam.Koprowski AT gmail.com, http://www.cs.ru.nl/~Adam.Koprowski
The difference between impossible and possible
lies in determination (Tommy Lasorda)
=====================================================