The Coq mailing list

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

Le Mon, 18 Jul 2011 16:06:13 +0200,
Julien Tesson 
<julien.tesson AT univ-orleans.fr>
 a écrit :

> Le 18/07/2011 14:37, AUGER Cedric a écrit :
> …
> 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.
> 

Sorry I misunderstood what you wanted.
Note that "__" is not really a kind of unit.
It is a Obj.t, that is, it can be almost anything.

Consider this funny program for instance:

Fixpoint narity n := match n with O => nat | S n => nat -> narity n end.

Fixpoint sum m (k:nat): narity m :=
  match m as n return (narity n) with
  | 0 => k
  | S m0 => fun H : nat => sum m0 (k + H)
  end.

==and its extraction==

type __ = Obj.t

type nat =
| O
| S of nat

(** val plus : nat -> nat -> nat **)

let rec plus n m =
  match n with
  | O -> m
  | S p -> S (plus p m)

type narity = __

(** val sum : nat -> nat -> narity **)

let rec sum m k =
  match m with
  | O -> Obj.magic k
  | S m0 -> Obj.magic (fun h -> sum m0 (plus k h))

====
the "__" is clearly not a unit type!
In this context, as it replaces a "Prop", you can see it as a unit type
only if you believe in proof_irrelevance.

Extraction doesn't need proof_irrelevance to be assumed AFAIK.

For your initial question, well, I guess it is never meaningfull to not
eliminate a "Prop", since you forbid to inspect it.
The only "Prop" you can inspect are singletons, so they don't need to
be matched.

BUT, sometimes it is not eliminated for typing reasons.
For instance in your list example, you cannot remove the "__", since
the constructor of a list always expect an argument.