The Coq mailing list

[Randy Pollack <rpollack0 AT gmail.com>]

Hi Xavier,

I don't have any answer for Coq, but you can see slightly more
discussion of the question in my paper:

[1] @INPROCEEDINGS{Pollack:belief,
  AUTHOR = {Robert Pollack},
  TITLE = {How to Believe a Machine-Checked Proof},
  BOOKTITLE = {Twenty Five Years of Constructive Type Theory},
  EDITOR = {G. Sambin and J. Smith},
  YEAR = 1998,
  PUBLISHER = {Oxford Univ. Press},
  URL = {http://homepages.inf.ed.ac.uk/rpollack/export/believing.ps.gz}
}

Best,
Randy
--
On Thu, Apr 12, 2012 at 1:30 PM, Xavier Leroy 
<Xavier.Leroy AT inria.fr>
 wrote:
> Hello Coq-list,
>
> I have a question to ask this resourceful community.  The question is
> rather vague, so please bear with me.
>
> Short form: is there a tool / how would you go about writing a tool
> that, given the *statement* of a Coq theorem, shows all *definitions*
> involved in this statement, omitting all the stuff that contribute
> only to the *proof* of the theorem?
>
> Long form: assume, for the sake of example, that I (or more
> realistically Georges Gonthier) managed to mechanize a proof of
> Fermat's last theorem.  We'd have a very long development, shock-full
> of higher mathematics, that concludes:
>
> Theorem Fermat:
>  forall (x y z n: nat),
>  n >= 3 -> x >= 1 -> y >= 1 -> z >= 1 ->
>  power x n + power y n <> power z n.
> Proof.
>  (* bla bla bla *)
> Qed.
>
> Further assume that I now need to convince skeptical mathematicians
> (or a certification authority) that I have indeed proved Fermat's last
> theorem.
>
> The skeptics agree that my *proof* is valid: they re-ran the
> proof, possibly with different Coq proof checkers; they trust those
> checkers; they reviewed the axioms involved and found them OK; etc.
>
> However, the skeptics now ask whether the *statement* of the
> theorem above is really Fermat's last theorem.  For instance, what
> guarantees that "power", "+", etc, were defined the correct way?
> For if I defined "power" as "power x n = 1", the statement would be
> trivially true, and its (correct) proof rather useless.
>
> One possible answer would be to show skeptics all the definitions that
> are involved in the statement, and nothing more, so that they can
> review them at their leisure, without being overwhelmed by all the
> higher mathematics needed to prove the statement.
>
> In this particular example, these definitions are few and they can be
> chased by hand:
>
> Inductive nat : Set :=
>  | O : nat
>  | S : nat -> nat.
>
> Fixpoint plus (n m:nat) : nat :=
>  match n with
>  | O => m
>  | S p => S (p + m)
>  end
> where "n + m" := (plus n m) : nat_scope.
>
> Fixpoint mult (n m:nat) : nat :=
> Fixpoint power ...
> Inductive le ...
> Definition lt ...
> Definition gt ...
> Inductive eq ...
>
> That could be enough to convince the skeptics.  But wouldn't it be
> possible to have an automatic mechanism to perform this kind of
> slicing?  After all, Coq's extraction does a similar kind of slicing,
> only along a different criterion.  How would the Coq experts go about
> implementing such a slicing mechanism?
>
> Thanks for your attention and any constructive :-) hints you could
> provide.
>
> - Xavier Leroy
>
>