The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Also, on a side note, I've been toying with the idea of making the
"Extraction Ignore" mechanism more flexible by being able to tag
certain arguments of constructors or functions as something like
"noextract N" and having Coq reject definitions where the extraction
would depend on the value of the parameter -- similar to what's
currently done with forbidding extracting proof structure to Type,
though I haven't worked out the full details of what rules would be
needed.  So for example, I would be able to eliminate the "wildcard'"
and "n0" arguments in the above.  Any thoughts on how hard it would be
to implement something like this as an extension to the Coq kernel?

I have no idea about the optimisation issue. As per what you are looking for in this side note. In a way, it already exists:

Inductive squash (A:Type) : Prop := squash_intro (x:A).

The problem with this approach is that it turns your type into a proposition, and there is no way, then, to prove that "squash_intro 0 <> squash_intro 1", as Coq is consistent with the axiom of proof irrelevance ( forall (P:Prop) (p q:P), p=q ). Yet, you probably want to prove something like that at some point, typically to prove the totality of random access.

The only way I know how to complement Prop with a disequality property ( exists (P:Prop) (p q:P), p<>q ) without getting the whole power of impredicative Set is to just assert it as an axiom. It's not very satisfying, but I believe it isn't risky. In ( http://www.pps.univ-paris-diderot.fr/~letouzey/download/Letouzey_Spitters_05.pdf ) Pierre Letouzey and Bas Spitters propose a slightly stronger axiom: forall (A:Type) (a b:A), squash_intro a = squash_intro b -> a=b .

A more serious attempt at this sort of things is the work by Bruno Barras and Bruno Bernardo ( http://link.springer.com/chapter/10.1007/978-3-540-78499-9_26 ) which adds precisely the construction you need. There used to be a prototype of Coq with this feature, but I believe it has been out of sync with Coq for years.

So I guess the answer to your question is: "pretty hard" if you want an elegant solution.


Arnaud