The Coq mailing list

[Xavier Leroy <Xavier.Leroy AT inria.fr>]

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