Proof by duality is heavily employed in pen-and-paper proofs in lattice and order theory. Since the duality lemma is often heavily utilized in lattice theory, we developed a Coq tactic that can apply the duality lemma.

We also developed a reinforcement learning agent in Coq that, without the aid of neural networks or human training data, can prove basic lattice equalities and inequalities. Once the agent was equipped with our duality tactic, the agent could prove theorems in a single step if its dual statement has already been proven in the Coq context. We hope this work is a first step to bringing that proof tactic to formalized, automated, and artificially intelligent proofs.

Read the full paper here.