The Coq mailing list

[frank maltman <frank.maltman AT googlemail.com>]

On Wed, 6 Jul 2011 13:52:26 +0200
AUGER Cedric 
<Cedric.Auger AT lri.fr>
 wrote:

> > 
> > Inductive read_mode : Prop :=
> >   | Read      : read_mode
> >   | Read_None : read_mode.
> > 
> > Inductive write_mode : Prop :=
> >   | Write      : write_mode
> >   | Write_None : write_mode.
> > 
> 
> I don't see any interest in providing such propositionnal types, as
> you won't be able to use them effectively.
> 
> For instance, you won't be able to prove that "Read <> Read_None"
> (unless you use an axiom, but if so, you should have put it in Set/Type)
>

We wanted to guarantee erasure. Placing them in Set/Type caused them to
appear in extracted code. They exist solely to make it a type error
to attempt to read from a handle of type 'handle Read_None W S' or
write to a handle of type 'handle R Write_None S'.

> > 
> > Extracting this function results in:
> > 
> > let test =
> >   open_truncate file_name (fun _ handle ->
> >     order (write handle message) (pure ()))
> > 
> > Note that the argument to the function passed to
> > open_truncate is in the Prop sort but hasn't been removed
> > by extraction. The type of this function obviously doesn't
> > match what the O'Caml definition is expecting!
> 
> I don't understand why you need this Prop parameter; have you read the
> manual about extraction? Have you tried Extraction Implicit?
> If not, do it; you may also consider taking a look in the Cocorico!
> wiki, about Extraction, or send a more complete (and parsable) file to
> give better explanations of what you want.

Yes, we've read it. Yes, we've tried Extraction Implicit.

Forget everything said above. The questions can be reduced to these:

--8<--

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?