The Coq mailing list

[Kristopher Micinski <krismicinski AT gmail.com>]

I'd be interested in seeing the resulting development, just because it
sounds like a good example of larger tactic development that might fit
in with some work I've been playing around with lately.

Kris

On Thu, Apr 4, 2013 at 9:03 AM, Gabriel Scherer
<gabriel.scherer AT gmail.com>
 wrote:
> I'm not very familiar with the field but I would also mention Stéphane
> Lescuyer's 2011 PhD thesis, "Formalizing and Implementing a Reflexive
> Tactic for Automated Deduction in Coq", which daringly implemented a
> core SMT solver (a kernel of Alt-Ergo) directly in Coq. I'm not sure
> if/where the resulting development is maintained.
>
> On Wed, Apr 3, 2013 at 2:13 PM, Chantal Keller 
> <Chantal.Keller AT inria.fr>
>  wrote:
>> Thanks Arnaud for pointing this out. SMTCoq indeed provide tactics to
>> call SMT solvers. This is a recent work, so it currently requires the
>> goal to be a Boolean, not a proposition (we are currently improving
>> this). It is entirely safe and does not require classical logic.
>>
>> There is no Coq tactic as powerful as Sledgehammer in Coq. To my
>> knowledge, the more powerful is what Claude presented, but it is indeed
>> unsafe.
>>
>> Chantal.
>>
>>
>>
>> Le 03/04/2013 10:24, Arnaud Spiwack a écrit :
>>> On interfacing external theorem provers with Coq in a safer manner, there
>>> is recent work like this one: with
>>> http://hal.inria.fr/docs/00/63/91/30/PDF/cpp11.pdf
>>>
>>>
>>> On 3 April 2013 10:16, Jonathan Heras 
>>> <jonathan.heras AT unirioja.es>
>>>  wrote:
>>>
>>>> On 03/04/13 08:58, Claude Marche wrote:
>>>>
>>>>> 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 ?)
>>>>>
>>>>
>>>> In Isabelle, when the external prover answers that a goal is valid, it
>>>> also returns the lemmas which have been used for that proof. Then, those
>>>> lemmas are given as input to a program called Metis that tries to 
>>>> reproduce
>>>> the proof in Isabelle. In some cases, Metis cannot generate the proof 
>>>> even
>>>> if external prover says that a goal is valid; in those cases, the goal is
>>>> not admitted and in this way you always work with trusted code.
>>>>
>>>> Cheers,
>>>> Jonathan
>>>>
>>>>
>>>>
>>>