The Coq mailing list

[Brandon Moore <brandon_m_moore AT yahoo.com>]

> From: Georgi Guninski 
>Â <guninski AT guninski.com>
>  May 31, 2011

> Subject: Re: [Coq-Club] Abuse of coercions gives weird results in coqtop.
> 
> On Mon, May 30, 2011 at 11:39:07AM -0400, Adam Chlipala wrote:
>>  Georgi Guninski wrote:
>>  >how a client should check a Coq proof for cheating?
>>  >[...]
>>  >
>>  >all of a sudden, coqtop doesn't see a contradiction, possibly due 
> to
>>  >what coq fanboys call "Anomaly" in your source.
>>  >
>>  >the error message coqtop gives is borderline insane "X is not 
> X" (or sthg very close to this).
>>  >
>>  >which parts of coq should i trust?
>> 
>>  I think you're discovering that Coq hasn't been engineered to
>>  provide a separate, trustworthy proof checker.  However, there is no
>>  deep technical reason why that wouldn't be easy to put together.  If
>>  you have an application where this is important, you could be the
>>  first to spend the few days (my estimate) needed to produce what's
>>  needed.
> 
> I got email which settled this thread for me.
> 
> Pollack-inconsistency
> Freek Wiedijk
> 
> http://www.cs.ru.nl/~freek/pubs/rap.pdf
> 5 Coq is weakly Pollack-super-inconsistent
> page 11

Does that settle your original question of how a client
should check a proof for cheating? It seems rather to
specifically point out a sort of cheating to guard against.

Brandon