Theorem proving katas (and languages)

[flip111]

Would be nice if there were katas for theorem proving. I think it's best to use languages which are actually made for theorem proving such as coq, agda, idris and F*. Theorem proving is not easy to do so katas would really help out to build up knowledge gradually.

[Voileexperiments]

You can already do some theorem proving in Haskell (see: Odd+Odd=Even and A+B = B+A).

Adding those would require new language support though.

[kazk]

Coq has been requested before (codewars/codewars-runner-cli#425). If you want, you can provide more information like examples, how to test, what kind of output tests can produce, etc. It'll help to add support. (I did play with it as you can see in the comments, but I don't remember anymore.)

I think it'll be most helpful if you can provide example kata as a repository, showing where solution and tests should go and and how to run the test. I don't think we'll be able to add new languages anytime soon though because we've been working on a new system to replace the current one.

Also, isn't it difficult to write them without some interactivity? especially non-trivial ones?

[MarisaKirisame]

I can do a little bit of Coq and Haskell, but I dont know a thing about docker :( can anyone help? We can collaborate to get Coq and latest Haskell on.

[kazk]

For Haskell, the issue was backwards compatibility because we need to keep GHC 7.10 for existing contents. This is resolved by the new system that's work in progress. Also, I'm planning to simplify the implementation and use HUnit directly for new versions. I might ask for help/feedbacks when we're ready to add it.

For Coq, showing us a small example project resembling a kata will help. Don't worry about Docker and assume you're setting up from scratch on Linux machine.
So information we need are

• setup
  • how to install the tools needed?
• structure
  • where should solution file go?
  • where should test file go?
• command
  • how to run the test?
• test output
  • is it customizable?
  • if not, how does it look like?

[MarisaKirisame]

Well, there are two thing about Coq that I think I should mention up front.
0: Coq is interactive. AFAIK Nobody read Coq code/write Coq code by pen and paper. There need to be specialized software (namely Coq/CoqIDE/ProofGeneral on Coq) to visualize what else need to be done to prove the whole thing: in short, think of it as an environment.

1: Test is seldom done, and it sort of defeat the purpose. The point of Coq is usually to prove some property of your program, for all argument (even if they are infinite). Test may come to supplement proof (example, or making sure you are proofing the right thing), but proof is the main point.

Back to the topic

For setup:
use opam.
https://coq.inria.fr/opam/www/using.html

For structure:
use coqc to compile a .v file. It can go anywhere

For proof/test:
put the .v file you just compiled in same directory as a test.v file. Compile it. Done.
In Coq test can be expressed as proof, so no need to run it. Or one might say that the compilation process already run some of the code.

Also, we need to check if user include additional axiom or not. (Anything could be included as axiom, to circumvent any proving) This is a Coq command but I dont know how to do it externally. I had been using Coq for quite a while, but I never touched it's external API, I can look them up though, if you need more help.

Test output:
Throw all the type error back. Not really customizable AFAIK.

For non interactivity, it might be possible to throw interactive information back, essentially using codewars as a coq box.

One last thing: in Coq sometimes we write algorithm (read: bfs/dfs) that generate proof. I bought a i7 compilation server to compile my Coq stuff, so CW might have big trouble against advance Coq. Legend has it that there are project that need 12 hours to compile. I dont know what we should do about this, but for simple Coq it is not bad.

[kazk]

@MarisaKirisame Thanks!

there are two thing about Coq that I think I should mention up front.

Yeah, that's why I asked about the differences from general purpose languages when it was requested, including how to "test".

---

I need to comeback later because I can't spend much time on this right now. I'll reread your comment and ask any questions that I might have.
I'd definitely need your help when we're going to add it. I'll let you know when we can start looking into more details.

[MarisaKirisame]

@kazk
Yes, no problem, no need to hurry > <

[clayrat]

I can do some Idris.

[kazk]

Idris is coming soon. See codewars/codewars-runner-cli#711

[kazk]

Codewars now supports Idris and we already have some kata thanks to @ice1000 🎉

Agda is mostly ready (I think) and coming soon. It currently uses the release candidate of Agda 2.6.0 and will be updated when it's released. I might make it available before that to get some feedback.

I'm also looking into Coq which you can follow here.