Çoqoban!

Did you know you can play Sokoban, the classic Japanese logic puzzle game, right in Coq? With Coqoban, you can!

From Coqoban Require Import Coqoban_engine Coqoban_levels.

Each puzzle is formulated via a proposition that can be used as a goal. Tactics move the warehouse keeper, and the goal is discharged as soon as all the boxes are in place.

Tactic Notation "→" := e. Tactic Notation "←" := w. Tactic Notation "↑" := n. Tactic Notation "↓" := s. Goal solvable microban_1. unfold microban_1.

With the magic that is Web programming, it becomes even more fun. Click the board shown in the goal pane to the right, and press some arrow keys on your keyboard. Press Backspace to undo one move.

The default goal microban_1 is not an actual level, it just demonstrates the concept; for a true challenge, replace it with Level_n, where n is a level number, 1..355.

Go to level:

(Disclaimer: It might be a bit slow on the larger levels... it's still two interpreters stacked one on top of the other, after all.)

Good luck! 🇯🇵🤺