The Coq mailing list

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

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                    |