The Coq mailing list

[Ömer Sinan Ağacan <omeragacan AT gmail.com>]

Thanks for both answers.

Jonathan,

> It is possible to remove such things as well.  Some of this can be done
> using Coq's extraction options.  But, for others, it takes a more
> comprehensive form of erasability than Coq currently has built in.

Can you elaborate on this? Are there any languages that can do that?
Can I somehow guide Coq to remove some arguments? (maybe by providing
some hints or proving/showing some properties etc.)

> This leads to a different style of proving, where
> one has to make sure that the type of a function encodes everything
> interesting about it - so that the function can remain opaque (you could
> just use Qed instead of Defined).  This is not a style that everyone would
> appreciate, but it has other benefits.  As long as one considers the
> extracted OCaml program to be what is being developed, and not the Coq
> "Gallina code" itself.  It is also a more modular style of programming -
> because the only thing that depends on how a function is implemented is the
> function itself, not proofs about it (which depend only on the function's
> type).

Interesting. This sounds to me like moving the proof from the
proposition to the definition by giving definition a rich type that
contains all I need in my Prop term. While this sounds interesting,
one problem that I can think of about this approach is that I'll lose
programs vs. properties distinction. Currently I can have very simple
typed programs and then in a separate module I can prove all kinds of
useful properties. If I understand correctly, this approach will give
fancy types to all definitions. If all I care about is extracted
programs, this should not be a problem though.(assuming those are
erased in extracted code) I should try this sometime.

> The alternative is to learn about the "convoy pattern" that Adam Chlipala
> uses extensively in his CPDT book.  However, when I was reading (a draft of)
> that CPDT book, it was precisely because of the convoy pattern and what
> weakness of Coq it covers up that I gave up Coq and learned Agda.  I only
> came back to Coq when I realized I could use tactics to program effectively,
> use an added erasability feature to generate nice OCaml, and keep the types
> of functions sufficiently comprehensive that I never unfold/simpl/compute
> them within proofs.

Convoy pattern is where I stopped reading the book. It's very ugly,
and most of the time I find the code very hard to understand and I
have no idea how to write such code.

Can you tell me more about "added erasability feature"?

> By the way, inversion tactics use the convoy pattern themselves internally -
> they're just not very good about tailoring each usage of that pattern
> precisely to the specific need.

I didn't know that. That may help me understanding the convoy pattern,
I can use it to see how Coq handles the situation at hand. Thanks.

---
Ömer Sinan Ağacan
http://osa1.net