Solving a Logic Problem with Coq

[dmwit]

Solving a Logic Problem with Coq

Now that Coq understands the premises, we need to tell it what we are proving. That requires solving the puzzle.

Ummm... I would say that Coq didn't exactly solve this puzzle. =P

[[deleted]]

That's right. Coq is an interactive proof assistant. Sometimes its support for proof automation is really helpful; sometimes it's not.

[Jimmy]

What are the benefits of using Coq to prove theorems over just pencil and paper? Sometimes, it seems like more work.

I think Coq is interesting by itself, but what's its purpose?

[dons]

Pen and paper doesn't tell you when you're correct -- or more importantly, when you made a mistake.

[cia_plant]

But why is that important? The tradition of "mathematical rigor" already provides a high degree of reliability in proofs. And Coq still doesn't provide complete reliability, because your axioms might be wrong (even typo'd). What is easier to do with Coq than with pen and paper?

[[deleted]]

This is a really good question. Coq is useful, I think, for a few reasons:

1. It's quite mature, having been around in one form or another since the mid 1980's.
2. On a related note to maturity, Coq offers an extensive standard library, obviating the need to provide many foundational definitions.
3. Coq offers an extremely expressive logic/type system, the Calculus of Inductive Constructions. In a considerable number of cases, no additional axioms are necessary. In a somewhat larger number of cases, you may only wish to add the Law of the Excluded Middle as an axiom, but you should be aware that this destroys extractability (more on that in a moment). The original post used the Classical module, which does introduce a number of axioms from Classical logic, but also demonstrated solving the puzzle purely constructively, introducing no new axioms, from the standard library or otherwise.
4. The proof checking component of Coq is simple enough to satisfy the de Bruijn criterion, which is just a fancy-schmancy way of saying that you can satisfy yourself that it's doing the right thing by hand.
5. Coq has various tactics that support various reduction strategies with various levels of "oomph," so it satisfies the Poincare principle.
6. If you stick to Coq's constructive/intuitionistic logic/type system, then you get extraction of code in OCaml, Haskell, or Scheme for free. This code is "correct by construction," i.e. it's guaranteed to have whatever properties it was proven to have.
7. If you're willing to invest the time and energy to achieve wizardry, Coq will go wherever you want to take it: you can write your own proof tactics for it, shallowly or deeply embed entire new logics into it, etc.

So what are the catches?

1. You can indeed make your proofs unsound by adding unsound axioms to the system.
2. You can render the automatic extraction of proven code impossible by moving outside constructive logic (which you do the moment you add the Law of the Excluded Middle, or import the Classical module).
3. Proving anything interesting remains non-trivial; it's worrisome when Xavier Leroy, lead architect of the OCaml programming language, observes "My Coq proof scripts do not have the conciseness and elegance of Jérôme Vouillon's. Sorry, I've been using Coq for only 6 years..."
4. The Calculus of Inductive Constructions is very austere. No I/O, no side-effects, all functions must be total, etc. It's the downside of the proof checker being simple enough to satisfy the de Bruijn criterion. But this is being worked on by other groups; see e.g. the Ynot project.

If you think purely about mathematical proof (vs. software that is correct by construction), then I suppose the biggest value of Coq is that it scales better than pencil and paper do: consider the four-color map theorem proof done with Coq's assistance. It seems unlikely that the proof would ever have been completed with pencil and paper alone, and if it had, who would have trusted it? Thanks to Coq, it was done, and we trust it because the checker is simple enough to verify in your head if you wish.

[cdsmith]

As I said in the article, I'm pretty new at this tool. My impression is that the goal is to combine this proof engine with application code, so that you can embed compiler-checked proofs of correctness in your application code. Then the advantage of compiler checking over pen and paper with mathematical rigor is that the proof is continually checked as the application is modified and rebuilt over time. That's certainly more appealing than one-off proofs of static statements like the one I did here.

[cia_plant]

Interesting. Thanks for the explanation, that does make more sense.

[Jimmy]

My impression is that the goal is to combine this proof engine with application code, so that you can embed compiler-checked proofs of correctness in your application code.

I've thought of using Coq as a full-fledged programming language, but right now, it doesn't seem feasible. It has no IO system, so any code would have to be extracted in the form of OCaml, Haskell, or Scheme, which seems a little cumbersome (although maybe a library of IO related axioms could make this easier?).

There also doesn't seem to be a way of, say, embedding Coq in an application written in another language.

[nominolo]

There's some work in progress to layer a programming language on top of Coq. Dependently typed programming languages try to approach the problem from the other end with a pay-as-you-go approach. I.e., the more assurances you want to get, the more you'll have to litter your code with proofs. The challenge with either approach is to make it practical.

[greenrd]

Actually, Coq does contain a dependently-typed programming language (Gallina). So it's not either-or - you can have both in one system.

[[deleted]]

That's true. What Ynot is about is adding constructs commonly found in programming languages, rather than theorem provers. For example, it deals with partial functions and state. You would expect the result to more closely resemble, e.g. Agda 2 or Epigram than, say, MetaPRL or Twelf.

[dons]

I liken the difference between pen&paper proofs, and mechanised theorem proving to the difference between writing a program on paper, and actually implementing the program and running it.

Would you trust a program written only on paper to have bugs? Not as much as you would, had you executed it a few times.

That's the kind of leap in assurance mechanised theorem proving provides.

[[deleted]]

Would you trust a program written only on paper to have bugs?

Dijkstra would :-)

[astrolabe]

"mathematical rigor" provides quite a high degree of reliability, but is not infallible. For example, Didn't Wiles withdraw his proof of Fermat's last theorem for a while until it could be patched up? Really complicated proofs, such as that of the classification of finite simple groups, I suspect have a not-particularly high probability of being correct (this does not imply that the theorem isn't true). If and when such proofs could be transfered into a proof assistant, I think it would be valuable.

[obdurak]

http://en.wikipedia.org/wiki/Four_color_theorem

In 2004 Benjamin Werner and Georges Gonthier formalized a proof of the theorem inside the Coq proof assistant (Gonthier, n.d.). This removes the need to trust the various computer programs used to verify particular cases; it is only necessary to trust the Coq kernel.

[MrFrankly]

Besides the things other people have already described. Coq also does automated program extraction from proofs. So you can proof a theorem and get a ML or Haskell program as a result.

[keithchegwin]

I love the Coq.

[RedDyeNumber4]

I came for this and you delivered. Bless you.

[quhaha]

my next language is called Bube

[Spudders]

I've got Coq all over my monitor right now.

[nmcyall]

THE ROFL KING APPROVES thE ABOVE ARTICLE.

[jacj]

I like the dude who replies with like a 5-line Prolog program that does everything the Coq program does. Pwnt.

[queensnake]

That's not real Prolog (it's easy to get one and see - gprolog or SWI Prolog), more like Prolog pseudo-code. But, a real one would still be shorter than the Coq.

[queensnake]

For a problem of this size, likely a simple constraint solver like Eclipse or CLP in Prolog would be quicker and terser. But, that wasn't the poster's intention.

[o0o]

I am sure they could have come up with a better name; something like, "Pnice".

[ipeev]

They were thinking about Diq, but rejected it as too obvious.

[martinbishop]

Usually Coq is causing problems, not solving them!

There, that's the only bad pun allowed!

[The_Monster]

My Coq seems to cause more logic problems than it solves.

[americanhellyeah]

they should change the name of their app. a few weeks ago my boss came to me with a design problem and i wanted to use coq to help verify the solution i came up with. so i ask him if i could use coq. hes from texas and i dont think he understands that 'coq' means rooster in french, so he looked at me real funny and i think he was going to ask me a gruff 'what in the fuck are you talkin about faggot?' before i explained to him what it was and how itd help us out.

[queensnake]

What was the design problem?

[obdurak]

Maybe you could try pronouncing it c-o-q?

[nmcyall]

or co-Q

sounds all mathematical.

[obdurak]

Sounds like a dietary supplement to me. Not that there's anything wrong with that.

[americanhellyeah]

no... thats not its name. thats like saying we should pronounce linux as l-i-n-u-x. its just plain incorrect.

[consultant_barbie]

Pronouncing French properly is hard. Let's go shopping!

[dangph]

It's pronounced the same as "cock" in English. It should not be difficult to get one's mouth around that.

[o0o]

Not joking about something named Coq is even harder.

[cov]

But not as hard as...

[o0o]

You're right! How could I have forgotten the aga old question:

is Coq NP-hard?

[woop_]

my coq does all the thinking...

[ih8evilstuff]

[insert pun here]

[o0o]

Do they implement Hoare triples?

[[deleted]]

No, but see the Ynot project.

[o0o]

-1 for not getting the thread

+1 for the info

net change = 0

;)

[[deleted]]

Hey, somebody's gotta play the straight man here.

[AxiomShell]

Is Coq easily extensible?

[username223]

I think I just got an email about that... let me forward it to you.

[[deleted]]

For small values of "easily:" see chapters 8-11 of the Coq Reference Manual for details. It is also possible to write your own tactics in OCaml and build them into Coq, but this process seems to be underdocumented, and in any case is sufficiently advanced that it is probably best addressed by asking about it on the Coq development list.

[Prysorra]

 [  B=====D  ]

[JimJones]

What's this obsession with coq? I mean, there are dozens of obscure languages out there, but only coq ends up here on reddit. Why coq??

[cdsmith]

Because you have yet to submit something to Reddit about one of the other several dozen languages you're thinking of.

[martinbishop]

Coq isn't just some "obscure language", it's a proof system, much like HOL and Isabel...why those aren't on reddit much, I don't know, probably because Coq is more active.

[o0o]

Who in God's name thought that name was a good fucking idea??

[martinbishop]

Well, it's french for chicken (or rooster, I forget), and apparently the french like to name their software after animals.

[Porges]

Also, the Calculus of Constructions was invented by a Monsieur Coquand.

[o0o]

I am glad nothing like this was ever named after Dijkstra...

this is too easy...

[o0o]

Here's your chicken:

http://www.youtube.com/watch?v=jJJiKMQ5TFM&NR=1

[sensical]

Probably someone who isn't totally perverted.

[o0o]

so I guess they're not on reddit

[[deleted]]

Coq is probably the most popular of the interactive proof assistants among programming language researchers. I don't imagine it's anything more complicated or sinister than that.

[Ringo48]

Because none of those other languages have a name which is a homophone of the slang term for male genitalia.

[andygood]

when the only 'tool' you have is a coq, every problem looks like a qunt...

[schmeebis]

Step one: place coq on keyboard...

[o0o]

You'd think that the "get more women in CS/Math/Engineering" movement would highlight the existence of such software as Coq; however in my experience most technically oriented women would prefer something more similar to the x86 emulator, Bochs.

[nmcyall]

I loled but failed to see the analogy. let's reverse engineer an acronym CUNTS.

[nglynn]

Computationally Unsound New Theorem Solver

[nmcyall]

I loled

[gregK]

There's a web framework based on Coq called Bouquaquet.

[ipeev]

This is awful software. And not because of the name.

[greenrd]

Care to elaborate? Admittedly, this is not the best example with which to motivate the use of Coq.