The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Claude,

I agree that a SMT solver is the perfect tool for the kind of goals it was 
made for, and
an integration into Coq which checks proof terms using Coq's type checker 
would be very helpful.

What I don't like are approaches which try to map everything to SMT, like 
Dafny. Finding proofs is similar to playing games like chess: there is a 
strategic and a tactical component. You can play chess with pure tactics, and 
you can get quite far with it, but there is a limit beyond which a system 
will fail miserably without a strategic component, and this is where it gets 
interesting.

For this reason I wouldn't identify the state of the art in proof automation 
just with tactical components like a SMT solver or a rewriting systems, as is 
implied by the original post. The real challenge is to get strategic 
descisions automated, or to at least have a system which interacts seamlessly 
with strategic desicisons made by humans. The latter was my main critics on 
the Dafny Schorr Waite paper and where I think your paper is much cleaner, 
because with Coq you had the choice of using different tactics.

Or to put it differently: even the most powerfull automated tatctic won't 
help you, if you have to bend your strategy too far in order to be able to 
use it.

Best regards,

Michael

-----Original Message-----
From: 
coq-club-request AT inria.fr
 
[mailto:coq-club-request AT inria.fr]
 On Behalf Of Claude Marche
Sent: Monday, May 18, 2015 11:49 AM
To: 
coq-club AT inria.fr
Subject: Re: [Coq-Club] Pointers regarding the state of the art of automation 
in Coq


Hi Coq Club,

Since I'm one of the author of one of the papers cited, let me add my two 
cents on this matter.

If you look at our paper on the proof of Schoor-Waite algorithm, you will see 
that not all the proof obligations are discharged using Coq.
Indeed, among the verification conditions generated by the Caduceus tool (now 
superseded by Frama-C/Jessie/Why3 tool chain, and close to Dafny in its basic 
concepts) some correspond to the proof of absence of run-time errors (e.g. 
absence of memory faults in the case of Schoor-Waite) and others correspond 
to advanced behavioral properties. In our case, VCs for the absence of 
run-time errors were discharged by the SMT solver Simplify, whereas the 
others were proved with Coq.

So, I would not say that SMT is definitely not what you want when working 
with Coq. I'd better say that SMT is sometimes good to solve some sub-goals 
that appear to be easy enough to be solved by SMT solvers, but not so easy 
with Coq (e.g. because of arithmetic or a lot of equality reasoning). It may 
allow you to concentrate your efforts to the "interesting" parts of a proof.

That's why I think that some better integration of SMT solvers in Coq could 
be very useful, in a similar fashion as the sledgehammer companion of 
Isabelle.

Let me add that there is something like this: the "why3" Coq tactic 
distributed with Why3:
http://why3.lri.fr/doc-0.86/manual010.html#sec101. But it should be used with 
caution, since it calls external SMT solvers and trust their answers, without 
building any proof term. In a case like program verification with Why3 or 
Dafny, where you are using external SMT solvers at the same time anyway, it 
is not an issue, but if you want to have the full high guarantee provided by 
Coq, then you should not use it (except may be for quick prototyping)

Hope this helps,

- Claude

Le 15/05/2015 17:40, Soegtrop, Michael a écrit :
> Dear Steve,
> 
>  
> 
> I support Adam Chlipala’s statement that SMT might not be what you 
> really want when working with Coq. Of cause the promise that it does 
> things automatically is nice, but SMT is much less expressive than 
> what Coq can handle in general. So you might spend a substantial 
> amount of work formulating something such that you can automatically 
> solve it with an SMT solver, which you can easily write down and solve 
> automatically in Coq.
> 
>  
> 
> I would recommend to look at the Shorr Waite algorithm proofs in Dafny 
> (SMT based proof language) and the same thing done in Coq. The things 
> you have to write down to formulate this such that the SMT solver can 
> solve it is really hard to understand, while the formulation of the 
> proof goals in Coq is fairly straightforward. Also interesting is, 
> that the Coq paper is 10 years older.
> 
>  
> 
> Another bad thing about SMT solvers is less abstraction. In Coq things 
> can be abstracted a lot and proofs be done in small steps. SMT proof 
> goals tend to be much less abstract and grow more with the complexity 
> of your project. So it might be easy to start with SMT, but get 
> increasingly unpleasant the further you go. Towards the end of a 
> project, you might spend most of your time thinking about how you can 
> reformulate your goal so that the SMT solver can solve it 
> automatically – something which can be just time consuming and tedious 
> trial and error. Coq work is much more pleasant ;-)
> 
>  
> 
> Best regards,
> 
>  
> 
> Michael
> 
>  
> 
> References:
> 
> Dafny: An Automatic Program Verifier for Functional Correctness K.
> Rustan M. Leino Microsoft Research
> 
> A case study of C source code verification: the Schorr-Waite algorithm.
> Thierry Hubert, Claude Marché
> 
>  
> 
> *From:*coq-club-request AT inria.fr
>  
> [mailto:coq-club-request AT inria.fr]
>  
> *On Behalf Of *stvienna wiener
> *Sent:* Friday, May 15, 2015 8:58 AM
> *To:* 
> coq-club AT inria.fr
> *Subject:* [Coq-Club] Pointers regarding the state of the art of 
> automation in Coq
> 
>  
> 
> Hi all,
> 
>  
> 
> Where can I start looking about the state of the art of automation in 
> Coq? I have read that there is ongoing work on SMT/SAT integration, as 
> well as automation support for resolution and rewriting proofs.
> 
>  
> 
> Are there any current papers I should look at?
> 
>  
> 
> By “Coq automation”, I mean automation regarding resolution, rewriting 
> and SAT/SMT solver integration. I am less interested in the basic 
> automation tools (auto, trivial or omega).
> 
>  
> 
> So far I have looked at the Coq workshop, ITP and the issues Journal 
> of Automated reasoning for the last six years. I am aware that my 
> question is rather broad and I still have some literature research to do.
> However, I would be glad if I get pointers into the right direction.
> 
>  
> 
> Best regards from Vienna,
> 
> Steve
> 
>  
> 
> PS: these are the papers I found so far:
> 
>  
> 
> [1] Armand, Michaël, et al. "A modular integration of SAT/SMT solvers 
> to Coq through proof witnesses." /Certified Programs and Proofs/. 
> Springer Berlin Heidelberg, 2011. 135-150.
> 
>  
> 
> [2] Blanqui, Frédéric, and Adam Koprowski. "CoLoR: a Coq library on 
> well-founded rewrite relations and its application to the automated 
> verification of termination certificates." /Mathematical Structures in 
> Computer Science/ 21.04 (2011): 827-859.
> 
>  
> 
> [3] Strub, Pierre-Yves. "Coq modulo theory." /Computer Science Logic/.
> Springer Berlin Heidelberg, 2010.
> 
>  
> 
> [4] Boldo, Sylvie, Jean-Christophe Filliâtre, and Guillaume Melquiond.
> "Combining Coq and Gappa for certifying floating-point programs."
> /Intelligent Computer Mathematics/. Springer Berlin Heidelberg, 2009. 59-74.
> 
>  
> 
> [5] Bezem, Marc, Dimitri Hendriks, and Hans De Nivelle. "Automated 
> proof construction in type theory using resolution." /Journal of 
> Automated Reasoning/ 29.3 (2002): 253-275.
> 

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