The Coq mailing list

["Carlos.SIMPSON" <Carlos.Simpson AT unice.fr>]

Dear Matthew,
  You would certainly need to know how to write a program to decide this, in your
favorite programming language. Then, that could also be done in Coq, basically using
inductive types to represent datatypes. The advantage of transforming your C++ program
into a Coq program is that you would then get a certified proof of the statement, rather
than just a positive answer from a program that you feel should find a correct proof.
The automation features in Coq will help to prove small lemmas along the way
(you need a lot of lemmas to say that your program does in fact find the correct proof), but can't
be considered as a substitute for coming up with your algorithm to find the proof.
---Carlos



On 02/28/2012 10:25 AM, Arnaud Spiwack wrote:

Well, you sound like you are trying to do logic programming. Coq has a small logical programming facility called 'eauto'. From Coq, what you will get is that the answer 'yes' will always be correct (hell, you'll have a definite proof of your result), but the answer 'no' will simply mean 'I couldn't find a proof'. Well, pretty much every logical programming system works like that: 'no' means failure rather than a definite 'no'. What Coq will help you do, is ensure your logical inferences are correct as you start by specifying what, say, positive definite matrices means, and then your inference rules are lemma; whereas in logic programming, the inferences act as the definition. On the other hand, Coq's eauto lacks the control abilities (like 'cut') that can be necessary to build reasonably effective logic programs.

On 27 February 2012 22:42, Matthew Rocklin <mrocklin AT cs.uchicago.edu> wrote:

Hello Coq community, 

I am interested in developing systems to answer questions about matrix expressions like the following:

Given that 

A and B are both matrices

A is symmetric and positive definite 

B is orthogonal

C = B.T * A * B

is C symmetric?

is C positive definite? 

This was also posted as a question on scicomp.stackexchange.com

http://scicomp.stackexchange.com/questions/74/symbolic-software-packages-for-matrix-expressions

A colleague recently suggested that I look at Coq. After a brief inspection and looking at some of the linear algebra codes already developed I have become quite interested. Before devoting significant time to this project I would like to ask the community's perspective. 

Some questions

1) Is Coq likely to be able to produce a black-box solver for questions like these? My solution must be fully automated. 

2) What types of questions are likely to be easy and what types are likely to be difficult?

3) Is there a simpler method to solve my problem? Perhaps Coq is overkill. Can anyone recommend a tool more appropriate for this problem?

I appreciate your time, 

-Matthew

--

Matthew Rocklin

University of Chicago - Computer Science PhD Student

http://people.cs.uchicago.edu/~mrocklin

-- 


------ ------ ------ ------ ------ ------ ------ ------ ------ ------ 

Carlos T. Simpson
C.N.R.S., Laboratoire J. A. Dieudonne, Universite de Nice-Sophia Antipolis

"Homotopy Theory of Higher Categories" now published!

Cambridge University Press, October 2011

http://www.cambridge.org/gb/knowledge/isbn/item6172978/

------ ------ ------ ------ ------ ------ ------ ------ ------ ------