The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 08/19/2016 02:00 PM, Robbert Krebbers wrote:
> On 08/19/2016 07:47 PM, Jonathan Leivent wrote:
> > Would you even recognize the decompiled lemma as the one you intended,
> > based on all that would need to be omitted (notations, implicits,
> > unicode translations, coercions, etc.)?
> Depends on the lemma of course. If you ask it to print a lemma whose 
> statement heavily relies on notations and implicit arguments, it will 
> probably be unrecognizable.
>
> However, that does not have to be the case. Take a look at:
>
>
> https://github.com/math-comp/math-comp/blob/master/mathcomp/odd_order/stripped_odd_order_theorem.v 
>
>
> This is a rather small self-contained file that consists of the 
> odd-order theorem and all definitions involved in its statement. It 
> does not rely on notations, implicit arguments, and so on.

But, that was written by humans, not by a decompiler, correct?  I'm 
anticipating that a decompiler - one that is faithful to the 
representation that coqchk is actually checking (not, for instance, one 
that based the decompiler output on some auxiliary info stashed away for 
just this purpose) - would be problematic both in implementation and in 
how readable its output would be.

Also, if one is willing to write such things, then isn't the suggestion 
of a test module that is compiled without plugins sufficient?

-- Jonathan