The Coq mailing list

[Bruno Barras <bruno.barras AT inria.fr>]

On 05/14/2011 12:47 PM, Georgi Guninski wrote:
> how a client should check a Coq proof for cheating?
> 
> please excuse my dumbness, i am new to Coq.
> 
> i am trying to convince a client a bit counterintuitive proof is valid.
> 
> it is my understanding there must be no axioms (coqchk -o) and in coqtop 
> "Print lemma_X." should print after ":" the statement of the .v source file.

You could also use Check lemma_X to avoid printing the proof term you
probably don't want to see at that point, since you've already checked
out for the axioms used.

> 
> should the client do other checks in the example below?
> 

If I were the client I would disable all customized notations with
Unset Printing All.
Then I would do Print on all the definitions involved directly or
indirectly in the type of lemma_X, to check they are what they're
supposed to be. It remains to see that symbols like -> forall match etc.
are not fake (see below).

> should i take any action to improve the example? (if it happens 
> valid/invalid i suppose i can change it a lot...):
> 
> (* coqtop is not fiddled by me, no east european plugins. coqchk -o passed 
> genuinely and showed no axioms.).
> 
> fuck_m$>coqtop
> Welcome to Coq 8.2pl1 (February 2010)
> Coq < Require Import fib10.
> Coq < Print c1.
> c1 = SOME_STUF ending in ')\n'
>   : True -> forall x : Prop, True -> x
> 
> Coq < Lemma l1: True -> forall x : Prop, True -> x.
> l1 < apply c1.
> Proof completed.
> 

Here I would try to do
Check (@c1 I False I).
to see if the arrows and forall in the type of c1 are not fake.

All of this inspection could be made easier with a tool that displays
the content of .vo files in a structured way (e.g. an xml tree with all
kind of annotations) as opposed to a mere character sequence.

Bruno.