Abstract
We present Aesop, a proof search tactic for the Lean 4 interactive
theorem prover. Aesop performs a tree-based search over a user-specified
set of proof rules. It supports safe and unsafe rules and uses a best-first
search strategy with customisable prioritisation. Aesop also allows users
to register custom normalisation rules and integrates Lean's simplifier to
support equational reasoning. Many details of Aesop's search procedure are
designed to make it a white-box proof automation tactic, meaning that users
should be able to easily predict how their rules will be applied, and thus how
powerful and fast their Aesop invocations will be. Since we use a best-first search strategy, it is not obvious how to handle
metavariables which appear in multiple goals. The most common strategy for
dealing with metavariables relies on backtracking and is therefore not
suitable for best-first search. We give an algorithm which addresses this
issue. The algorithm works with any search strategy, is independent of the
underlying logic and makes few assumptions about how rules interact with
metavariables. We conjecture that with a fair search strategy, the algorithm
is as complete as the given set of rules allows.
Original language | English |
---|---|
Title of host publication | Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs |
Publisher | Association for Computing Machinery |
Publication date | 2023 |
Pages | 253-266 |
ISBN (Print) | 979-8-4007-0026-2/23/01 |
DOIs | |
Publication status | Published - 2023 |
Event | 12th ACM SIGPLAN International Conference on Certified Programs and Proofs - Boston Park Plaza, Boston, United States Duration: 16 Jan 2023 → 17 Jan 2023 https://popl23.sigplan.org/ |
Conference
Conference | 12th ACM SIGPLAN International Conference on Certified Programs and Proofs |
---|---|
Location | Boston Park Plaza |
Country/Territory | United States |
City | Boston |
Period | 16/01/2023 → 17/01/2023 |
Internet address |