这个主要是 graph theory，和题主要求的有点差别，不过好玩是挺好玩的。
Coq 也有自动档：https://coqhammer.github.io/
By 薛定宇, 陈阳泉
哟系，这玩样不错，我去研究下