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.

翻译：在证明助手中工作时，自动化是处理常规证明目标（如代数表达式间等式）的关键。同伦类型论允许用户使用高阶归纳类型（HITs）和单值性推理拓扑空间等高阶结构。立方Agda是Agda的扩展，为HITs和单值性提供计算支持。在立方Agda中工作的一大难点在于处理高阶结构的复杂组合学——这是等式推理的无限维推广。解决这些高维等式需要构造具有指定边界的立方体。我们开发了一种简化的立方语言，在其中隔离并研究两个自动化问题：扭曲求解（尝试使立方体"扭曲"以适配给定边界）和更一般的Kan求解（搜索涉及拼接多个立方体的解）。这两个问题在一般情况下都难以处理——Kan求解甚至不可判定——因此我们专注于在实践案例中表现良好的启发式方法。我们通过将扭曲问题重新表述为偏序集映射来提供求解器，同时使用约束满足编程解决Kan问题。我们在实验性的Haskell求解器中实现了算法，可用于自动求解立方Agda呈现的目标。我们通过案例分析（使用求解器证明Eckmann-Hilton定理）及多项基准测试展示了该方法的有效性，为立方类型论中证明自动化的进一步研究奠定基础。