The Coq mailing list

[Julien Tesson <julien.tesson AT univ-orleans.fr>]

Le 18/07/2011 14:37, AUGER Cedric a écrit :

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.

There, the Prop part is eliminated in the extracted term isn't it ?
I was looking for an example where it is *not* eliminated *and* it is meaning full.
For example
   

Definition A : Prop :=  1=1.
Definition a : A.
reflexivity.
Qed.

 Definition aList := a::a::a::nil.

Here aList is a structure containing elements in Prop, but it is in Set, and at extraction it gives

Extraction aList.

(** val aList : __ list **)
let aList =
  Cons (__, (Cons (__, (Cons (__, Nil)))))

where __ is a kind of unit. So  I suppose that such structure could be useful, but I am curious to see a real exemple using such things.

--

Julien Tesson

Doctorant - ATER
Laboratoire d'Informatique Fondamentale d'Orléans
Département Informatique
Université d'Orléans

Tel : 02 38 49 25 81
Fax : 09 56 45 86 27
http://tesson.julien.free.fr/