Coq Fight 2018: June 27th

Affichage de 11 messages sur 1
Coq Fight 2018: June 27th Amos Robinson 28/05/18 18:08
Hello, provers.

Functional Programming Sydney will once again hold the world's most prestigious theorem-proving tournament, at its next meeting on 27 June 2018!

The annual FP-Syd Coq Fight is a tournament in which contestants race to prove simple theorems, using the Coq interactive theorem prover. Two contestants are simultaneously given the same lemma, and independently try to prove it, while projecting their Coq session to the audience. The first to discharge all goals wins the lemma. Each match usually consists of a few lemmas. The overall tournament might be round-robin or knock-out, depending on the number of participants.

Experience theorem proving like you've never seen it before: with pizza, heckling, expert commentary, and above all, fun.

I hereby invite challengers for the 2018 FP-Syd Coq Fight. Participation is open to everyone, and challengers need not be expert in Coq. I have attached a few self-qualifying lemmas (Qualifying.v). If you can prove each of those within a few minutes, I encourage you to participate. We aim to make competition lemmas fairly simple, since much of the challenge comes from the competition environment. If in doubt, have a go!

If you want to practice, I have attached an archive containing the lemmas from an earlier contest (2015, I believe). This is a good training set, but there are some harder ones here. Don't be discouraged if you can't finish them all.

We will need a supply of lemmas for the competition, so if you want to compete, you should contribute some lemmas to that supply. Start thinking up some lemmas now. Aim to provide about 5 competition lemmas. More if you can.

Competition lemmas should be a similar difficulty to the qualifying lemmas attached, with maybe a few that are just slightly more difficult. We want lemmas which can be solved by a contestant within a few minutes, bearing in mind that contestants are proving under pressure.

Lemmas about natural numbers and lists are great. Avoid requiring extensive knowledge of the standard library. It's ok to define structures or functions, but keep it simple. Slight variations on lemmas used in previous competitions are fine. You can also use the practice set for inspiration.

Each competition lemma should be self-contained in a single file, with all the necessary imports provided. It should be small enough that the lemma statement and any definitions fit on a projector screen.

Check to make sure the lemma cannot be solved immediately by eauto, congruence or omega. It should require at least a couple of steps.

We will use Coq version 8.8.

When you have some competition lemmas, please register a user account at Bantam, our Coq Fight tournament website helpfully provided by Charles O'Farrell:

Once you have a user account, you will be able to create lemmas there. Later, when we have enough competition lemmas, we will distribute them among competitors to classify them according to difficulty.

Now, let's get proving!

And many thanks to Matthew Brecknell for organising last year, and whose announcement I plagiarised heavily.

Amos