The Coq mailing list

[Andreas Abel <andreas.abel AT ifi.lmu.de>]

Hello Frank,

I think this has nothing to do with Prop or not Prop, it is just that 
rank-2 arguments are never eliminated.  That means, if you have a 
function type in a "higher-order" position, like the type

    (forall {S : Prop}, A ->  A)

which is the type of an argument of foo, then its arity is preserved by 
the extraction.

Here are more examples:

Definition g : forall C : Type,  (forall A : Type, bool -> bool) -> bool
 := fun C h => h bool true.

Extraction g.
(* results in
(** val g : (__ -> bool -> bool) -> bool **)

let g h =
  h __ True

The rank-1 "forall C" is removed, but not the rank-2 "forall A".
*)

Definition g' : forall p : False,  (forall q : False, bool -> bool) -> bool
 := fun p h => h p true.

Extraction g'.
(* results in
(** val g' : (__ -> bool -> bool) -> bool **)

let g' h =
  h __ True

The proof argument "forall q" is not removed because it is a rank-2 
quantification.
*)

Cheers,
Andreas


On 7/6/11 5:52 PM, frank maltman wrote:
> Axiom foo : forall {A : Set}, A ->  (forall {S : Prop}, A ->  A) ->  A.
> Extract Constant foo =>  "foo".
>
> Definition bar (a : bool) :=
>    foo a (fun {S} x =>  x).
>
> Recursive Extraction bar.
>
> (*
>
> Result:
>     ...
>     let bar a =
>       foo a (fun _ x ->  x)
>
> *)
>
> --8<--
>
> Why does the '_' argument of type 'Prop' appear above? Shouldn't all
> arguments in Prop be erased during extraction? How can this be prevented,
> if at all?

--
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel AT ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/