Automating Boundary Filling in Cubical Agda
CoRR(2024)
摘要
When working in a proof assistant, automation is key to discharging routine
proof goals such as equations between algebraic expressions. Homotopy Type
Theory allows the user to reason about higher structures, such as topological
spaces, using higher inductive types (HITs) and univalence. Cubical Agda is an
extension of Agda with computational support for HITs and univalence. A
difficulty when working in Cubical Agda is dealing with the complex
combinatorics of higher structures, an infinite-dimensional generalisation of
equational reasoning. To solve these higher-dimensional equations consists in
constructing cubes with specified boundaries.
We develop a simplified cubical language in which we isolate and study two
automation problems: contortion solving, where we attempt to "contort" a cube
to fit a given boundary, and the more general Kan solving, where we search for
solutions that involve pasting multiple cubes together. Both problems are
difficult in the general case - Kan solving is even undecidable - so we focus
on heuristics that perform well on practical examples. We provide a solver for
the contortion problem using a reformulation of contortions in terms of poset
maps, while we solve Kan problems using constraint satisfaction programming. We
have implemented our algorithms in an experimental Haskell solver that can be
used to automatically solve goals presented by Cubical Agda. We illustrate this
with a case study establishing the Eckmann-Hilton theorem using our solver, as
well as various benchmarks - providing the ground for further study of proof
automation in cubical type theories.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要