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

Question

我已经开始玩 Cubical Agda。我尝试做的最后一件事是以类似于经典数学中的方式（参见the construction of integers on 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) 的术语。不想手动证明这一点，我想使用ring solver made in Cubical Agda。但我永远无法让它工作，甚至尝试将其设置为简单的环等式，例如x + x + x ≡ 3 * x。

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

Answer 1

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

立方/代数/NatSolver/Examples.agda

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

立方/代数/RingSolver/Examples.agda

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

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

Answer 2

我已经成功地将环求解器用于完全相同的问题：将Int 定义为ℕ ⨯ ℕ 的商。你可以找到完整的文件here，相关部分如下：

1. 非立方命题等式到路径等式：

open import Cubical.Core.Prelude renaming (_+_ to _+̂_)

open import Relation.Binary.PropositionalEquality renaming (refl to prefl; _≡_ to _=̂_) using ()
fromPropEq : ∀ {ℓ A} {x y : A} → _=̂_ {ℓ} {A} x y → x ≡ y
fromPropEq prefl = refl

1. 使用环求解器的示例：

open import Function using (_$_)

import Data.Nat.Solver
open Data.Nat.Solver.+-*-Solver
  using (prove; solve; _:=_; con; var; _:+_; _:*_; :-_; _:-_)

reorder :  ∀ x y a b → (x +̂ a) +̂ (y +̂ b) ≡ (x +̂ y) +̂ (a +̂ b)
reorder x y a b = fromPropEq $ solve 4 (λ x y a b → (x :+ a) :+ (y :+ b) := (x :+ y) :+ (a :+ b)) prefl x y a b

所以在这里，即使环求解器为我们提供了 _=̂_ 的证明，我们也可以使用 _=̂_ 的 K 和 _≡_ 的自反性将其转化为路径相等，可以在下游进一步使用例如证明Int加法是代表不变的。