How to quantify quantifiers: an Ltac puzzle
- April 5, 2018
In some occasions, using the Coq proof assistant stops resembling a normal software development activity, and becomes more similar to puzzle solving.
Similarly to the excellent video games of the Zachtronics studio (TIS-100, SpaceChem, …), the system provides you with puzzles where obstacles have to be side-stepped using a fair amount of tricks and ingenuity, and finally solving the problem has often no other utility than the satisfaction of having completed it.
In this blog-post, I would like to present what I think is one such situation. What the puzzle is, how we solved it, and why you shouldn’t probably do that if you like spending your time in a useful manner.
