The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 04/29/2015 10:09 AM, David MENTRE wrote:
> Hello,
>
> Le 29/04/2015 15:53, Jonathan Leivent a écrit :
> > On 04/28/2015 03:37 PM, Evelyne Contejean wrote:
> > > There is also the "ergo" tactic, due to Stéphane Lescuyer, as a part
> > > of his thesis when he was a PhD student of mine.
> > >
> > > www.lix.polytechnique.fr/coq/pylons/.../Ergo/v8.3
> >
> > I get a "404 Not Found" error for that link.
>
> Following URL is working (found with Google):
>
> http://www.lix.polytechnique.fr/coq/pylons/contribs/files/Ergo/v8.4/Ergo.tar.gz 
>
>
> Best regards,
> david

I found the description here:

http://www.lix.polytechnique.fr/coq/pylons/contribs/view/Ergo/trunk

which says "This extension is limited to non-dependent types." - are 
there any SMT solvers that can work with dependent types?


But, regardless...

The ability to link to SMT solvers and use them as decision procedures 
is certainly interesting and helpful - but I was hoping for a different 
kind of synergy between SMT and Coq - that would perhaps allow Coq to 
achieve a more comprehensive proof search capability over any 
dependently-typed theory by using approaches that SMT solvers use to 
build and test alternative models for the existential variables tying 
together multiple subgoals.

-- Jonathan