The Coq mailing list

[Georgi Guninski <guninski AT guninski.com>]

thank you, very helpful answer.

On Mon, May 16, 2011 at 05:43:49PM +0200, Bruno Barras wrote:
> 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.