The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Wed, 13 Jul 2011 10:53:52 +0200,
Julien Tesson 
<julien.tesson AT univ-orleans.fr>
 a écrit :

> Thank you for your clear answer :)
> 
> The only thing I miss is an example of extracted program where a
> structure containing only elements in Prop would be really
> meaningful, but I am sure that such thing exists ....
> 

Such programs exist, a great example is one produced by a fixpoint with
a non structurally decreasing argument (for the extracted program),
using the Acc predicate.

For instance a "for" using binary integers would look like:

Lemma wf_succ: forall x, Acc (fun x y => x = Ppred y).
…

Fixpoint for n (H: Acc (fun x y => x = Ppred y) n) … :=
 match H with
 | Acc_intro H =>
   match n with
   | xH => …
   | _ => … (for (Ppred n) (H (Ppred n) (eq_refl _)) …) …
   end
 end.

Will give as extracted program:

let rec for n … =
 match n with
 | Coq_xH => …
 | _ => … (for (Ppred n) …) …

I am not sure to have such an example on the cocorico! wiki at the
extraction page.