The Coq mailing list

[Randy Pollack <rpollack AT inf.ed.ac.uk>]

How to believe a machine-checked proof. In G. Sambin and J. Smith,
editors, Twenty Five Years of Constructive Type Theory. Oxford Univ.
Press, 1998.

Randy
--
On Tue, May 17, 2011 at 3:33 AM, Georgi Guninski 
<guninski AT guninski.com>
 wrote:
> 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.
>
>