The Coq mailing list

["Carlos.SIMPSON" <carlos AT math.unice.fr>]

>I do not  know of any such work.  Could you be a bit  more precise, by
>the way:  would you  like to generate  theorems' proofs or  just their
>statements;

It would be good to generate the proofs too! Here is what I was wondering
about: given a certain context (and a certain database of Hints), 
could  one generate a file containing
a filtered list of Theorems with the property that EAuto succeeds in
proving them? One would also want to generate the proof terms at the
same time in order to avoid waiting for EAuto to prove all of them.
The word `filtered' indicates that some type of filter would seem necessary
--(a) to insure that the list of theorems is well-defined and finite
--(b) to avoid duplication in as much as possible
--(c) to prune out ``uninteresting'' results, whatever that means.

The first part of the definition of the filter is that we only consider
theorems of type (P X) where P is a constructor to Prop which is
already explicitly defined somewhere in the loaded modules and context; and
X is a vector of terms which again are already explicitly defined
somewhere in the loaded modules and context.
(I guess this condition yields finiteness (a) already).

It shouldn't be difficult to write a program which theoretically does the
above just by creating the list of theorems in question and sending them
to coqtop with the tactic EAuto. So to be precise there are two questions:
(1) does somebody have a program with the capability of doing that?
(2) is there a way to do that more efficiently than just asking Coq for
an EAuto for each individual theorem? 

The next step would be to declare all of the resulting theorems as Hints
and to iterate. This would necessitate a good filter in order to avoid
things getting too big. 

Iterating a very basic version of the construction might be a basis for
a more efficient answer to (2) above.

---Carlos