The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 09/12/2014 03:34 PM, Ömer Sinan Ağacan wrote:
> 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.)

Take a look at the chapter 23.2 in the reference manual, entitled 
"Extraction options".  Also note that Coq provides some useful settings 
for extraction that you can get via:

Require Import ExtrOcamlBasic.

There are richer versions of that library file as well - to be found in 
coq/plugins/extraction.  Much of what they do is based on chapter 23.2.4 
"Realizing axioms" .

In some cases, Coq can remove arguments for you via the "Extraction 
Implicit ..." command.  However, I have not had very good luck with this 
command.

> > 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.

Yes - you certainly lose the "simple programs" in Coq aspect, but with 
erasability can keep the "simple programs" in OCaml.  Like I said, this 
isn't for everyone.  But, by making the types of your functions more 
informative, you actually lose the need for many external proofs - as 
most properties are part the types themselves. Those properties don't 
appear by magic - they were proved by the tactic-script implementation 
of the function - and so many would consider that as complicating the 
business of programming with the business of proving.  However, I think 
an interesting thing happens when you really bundle all the properties 
you can think of into a function's type - the implementation can 
actually become easier in a sense, though certainly containing more 
proof-centric drudgery (much of which is automatable).

> > 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.

Well, that makes two of us!

I have read proposals for Coq that would enhance the match construct to 
reduce or eliminate the need for convoy patterns - and get something 
more along the lines of what Agda and Idris accomplish with their 
pattern matching mechanisms, which track the necessary type changes in 
the branches.

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


Note that Coq does a fine job of removing a great many things already - 
related to types and the Prop universe.  It just doesn't remove non-Prop 
type indices - such as the index for Vector.t - because it can't do that 
without further compile-time erasability analysis (something being 
aggressively pursued in Idris - see 
https://github.com/idris-lang/Idris-dev/wiki/Erasure-by-usage-analysis). 
For instance, to remove the nat index from Vector.t requires knowing 
that there is no runtime usage of it anywhere - such as by a fast vector 
length function.

But, if one is willing, one can exploit the Prop universe to get such 
things erased.  This can complicate things a bit - for example, you 
would need an alternate definition of Vector - but that is fairly easy 
(if lengthy) to achieve.  To exploit the Prop universe this way requires 
adding an axiom - with the usual consistency risks of doing so - but it 
is a very simple axiom that, as far as I know, is only incompatible with 
general proof-irrelevance (among the typical other axioms that are 
frequently added to Coq), but not with specific proof-irrelevance 
(defined separately for each Prop one wishes to be irrelevant, such as 
equality).  The idea of this axiom is to make a single Prop relevant by 
adding an injectivity axiom to its sole constructor, and to use "lifted" 
(into that single Prop) versions of types and values you want erased in 
those spots where you want them erased - and then allow Coq's normal 
Prop removal to do its thing.  With careful handling, one can get OCaml 
output from Coq with this addition that is quite clean.

In my github project https://github.com/jonleivent/mindless-coding, the 
file erasable.v does the work of adding erasability along these lines, 
along with some useful tactics and notations for dealing with it.

> > 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.

Yes - take a look at the recent thread (2 weeks ago?) with the subject 
"Program" - for some cases of human vs. Coq authored convoy patterns.  
If you only object to writing, and not reading, convoy patterns, then 
inducing Coq to write them for you is a viable alternative.

-- Jonathan