The Coq mailing list

[Claude Marche <Claude.Marche AT inria.fr>]

Dear Coq list,

Le 02/04/2013 17:19, Kristopher Micinski a écrit :
> Interesting that there hasn't been any work on this: it was my
> intuition that someone *had* done this (I look forward to someone here
> to pointing me to better refs if has been indeed done).  The best of
> which I know is:
>
> @MISC{Ayache06combiningthe,
>      author = {Nicolas Ayache},
>      title = {Combining the Coq proof assistant with first-order
> decision procedures},
>      year = {2006}
> }
>
> http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.64.4549

Just to inform you that this work of Nicolas Ayache is an early 
predecessor of what became now the Why3 tactics for Coq. This tactic is 
installed when you install the Why3 environment (http://why3.lri.fr, see 
the doc http://why3.lri.fr/doc-0.81/manual011.html). This tactic aims at 
calling external automated provers to solve the current goal. In that 
sense, it is I think quite similar to what Sledgehammer offers in Isabelle.

Although it is initially designed to discharge goals that are generated 
by Why3, it can perfectly be used on goals written directly by the Coq 
user.

Nevertheless, one should be aware of an important point: when the 
external prover answers that the goal is valid, then the Why3 tactic 
introduces an axiom in Coq to discharge the original goal. There is no 
Coq proof generated. This is an important issue if you want to restrict 
your trusted code base to the Coq kernel only. As far as I understand, 
this is not a issue in Isabelle/sledgehammer since Isabelle does not 
build proof terms internally (am I wrong ?)

All the best,

- Claude


--
Claude Marché                          | tel: +33 1 72 92 59 69
INRIA Saclay - Île-de-France           |
Université Paris-sud, Bat. 650         | http://www.lri.fr/~marche/
F-91405 ORSAY Cedex                    |