solver - 您如何在 Cubical Agda 中使用环求解器？

Question

我已经开始玩 Cubical Agda。我尝试做的最后一件事是构建整数类型（假设已经定义了自然数的类型），其方式类似于经典数学中的完成方式（参见wikipedia 上的整数构造）。这是

data dInt : Set where
    _⊝_ : ℕ → ℕ → dInt 
    canc : ∀ a b c d → a + d ≡ b + c → a ⊝ b ≡ c ⊝ d 
    trunc : isSet (dInt)

之后，我想定义加法

_++_ : dInt → dInt → dInt 
(x ⊝ z) ++ (u ⊝ v) = (x + u) ⊝ (z + v)
(x ⊝ z) ++ canc a b c d u i = canc (x + a) (z + b) (x + c) (z + d) {!   !} i
...

我现在卡在两个牙套之间的部分。x + a + (z + d) ≡ z + b + (x + c)询问类型术语。不想手动证明这一点，我想使用Cubical Agda 制造的环求解器。但我永远无法让它工作，甚至尝试将它设置为简单的环等式，如x + x + x ≡ 3 * x.

我怎样才能使它工作？有没有一个最小的例子使它适用于自然？库中有一个文件 NatExamples.agda，但它使您必须以复杂的方式重写您的等式。

Answer 1

您可以在cubical库的这个文件中看到应该如何使用自然数求解器：

立方/代数/NatSolver/Examples.agda

请注意，此求解器与交换环求解器不同，交换环求解器是为证明抽象环中的方程而设计的，并在此处进行了说明（不仅在 PR 中）：

立方/代数/RingSolver/Examples.agda

但是，如果我正确地阅读了您的问题，那么您要证明的等式需要在 Nat 中使用其他命题等式。立方体库中的任何求解器都不支持这一点（据我所知，标准库也不支持它）。但是，当然，您可以将求解器用于不使用其他等式的所有步骤。

以防万一您没有发现这一点：这SetQuotient是使用立方体库的 s 以数学风格定义整数。SetQuotients 帮助您避免与您的第三个构造函数相关的工作trunc。这意味着您基本上只需要像在“正常”数学中那样显示一些结构是明确定义的。

Answer 2