The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

gbush wrote:
> Hello,
>
> I've been experimenting with a proof of a simple parser that I want to
> extract into a nice program.  I can complete the proof using well-founded
> induction on the length of the string being parsed, but the proof extracts
> to something like...
>
> let rec parse x =
>    func x (fun y _ -> parse y).
>
> ... which is not very satisfying from my perspective.
>
>
>   
Your problem is that you want to define a nested recursive function 
using a ad-hoc predicate.
The only reference to work where this is done that I know of is the work 
of Bove and Capretta,
and they argue that this problem can be solved using simultaneous 
induction-recursion, whereby
you define simultaneously an inductive predicate and a recursive 
function.   This was described
by Peter Dybjer in 1991 and I believe (although I am not sure) that it 
is provided in Alfa.

So I believe you have to revert to a well-founded definition.  But life 
is not so bleak, since you can
configure the Extraction facility so that you recognize you parsing 
function.  This is what I obtained:

let rec parse = function
 | Nil -> None
 | Cons (x0, xs) ->
     (match x0 with
        | AtomToken -> Some (Pair (Atom, xs))
        | ImpToken ->
            (match parse xs with
               | Some p ->
                   let Pair (p0, s) = p in
                   (match parse s with
                      | Some p1 ->
                          let Pair (q, s0) = p1 in
                          Some (Pair ((Imp (p0, q)), s0))
                      | None -> None)
               | None -> None))


The Coq development is given below (I did not perform the obvious 
proofs).  I used Fix
instead of well_founded_induction because Fix comes with a side theorem 
named Fix_eq, which will
be handy later if you want to reason about what your parse function does 
(for now, its only specification
is its code, and if it was defined using well_founded_induction, it 
would be difficult to prove that it
satisfies the natural fixpoint equation).  My opinion is that we should 
stop using well_founded_induction
(or rename Fix into well_founded_induction), because they have the same 
type but Fix has the nice
companion theorem and Fix should be inlined by default (like 
well_founded_induction).

<<<<< Begin Coq code.

Require Import List Wf_nat.

Inductive Token : Set := AtomToken | ImpToken.
Inductive Term : Set :=  Atom | Imp(t1 t2:Term).

Definition t' (s l:list Token) := length l <= length s.

Definition t (s:list Token) :=
  option(Term * {l:list Token | length l <= length s}).

Lemma th : forall s (x:Token) xs, x::xs=s -> length xs <= length s.
Admitted.

Lemma th1 : forall s (x:Token) xs, x::xs=s -> length xs < length s.
Admitted.

Lemma th2 : forall s (x:Token) xs, x::xs=s -> forall s':list Token,
  length s' <= length xs -> length s' < length s.
Admitted.

Lemma th3 : forall s (x:Token) xs, x::xs=s -> forall s':list Token,
  length s' <= length xs -> forall s'':list Token, length s'' <= length 
s' ->
  length s'' <= length s.
Admitted.

Definition parse_F (s:list Token)
 (parse : forall l: list Token, length l < length s-> t l) : t s :=
match s as x
 return x = s -> t s with
 nil => fun _ => None
| x::xs => fun hxs : x :: xs = s =>
 match x with
   AtomToken => Some (Atom, exist (t' s) xs (th s x xs hxs))
 | ImpToken => match parse xs (th1 s x xs hxs) with
   | None => None
   | Some (P,exist s' hs') =>
     match parse s' (th2  s x xs hxs s' hs') with
     | None => None
     | Some(Q, exist s'' hs'') =>
       Some(Imp P Q, exist (t' s) s'' (th3 s x xs hxs s' hs' s'' hs''))
     end
   end
 end
end (refl_equal s).

Definition parse := Fix
 (well_founded_ltof _ (@length Token))
 t parse_F.

Extraction Inline parse_F Fix.

Extraction "parse.ml" parse.