如何在Cubical Agda中使用Ring solver完成环等式证明？

最小自然数场景示例 #

以下是完整可直接编译的代码，可证明x + x + x ≡ 3 * x这类自然数半环等式：

{-# OPTIONS --cubical #-}
open import Cubical.Foundations.Prelude
open import Cubical.Data.Nat
open import Cubical.Data.Nat.Properties
open import Cubical.Algebra.CommSemiring
open import Cubical.Algebra.SemiringSolver

-- 导入自然数预定义的交换半环实例
ℕ-csr = ℕ-CommSemiring 0
open CommSemiringSolver ℕ-csr

-- 示例证明：3个x相加等于3乘x
3x-identity : ∀ x → x + x + x ≡ 3 * x
3x-identity = solve 1 (λ x → x :+ x :+ x := con 3 :* x) refl

调用solver的核心规则 #

• 第一个参数是等式中变量的数量，和后续lambda的参数个数严格匹配
• 等式左右两边必须使用solver提供的算子：:+对应加法，:*对应乘法，con包裹常量值，:=分隔等式左右
• 最后一个参数固定传refl即可

dInt加法定义的洞填充方案 #

目标等式基于前提a + d ≡ b + c，可以结合solver自动处理交换律结合律，再代入前提即可：

add-canc-case : ∀ x z a b c d → a + d ≡ b + c → x + a + (z + d) ≡ z + b + (x + c)
add-canc-case x z a b c d eq =
  -- 用solver把左边整理为 x + z + (a + d)
  solve 4 (λ x z a d → x :+ a :+ (z :+ d) := x :+ z :+ (a :+ d)) refl x z a d
  -- 代入前提 a + d ≡ b + c
  ∙ cong (λ k → x + z + k) eq
  -- 用solver把x + z + (b + c)整理为目标右边形式
  ∙ solve 4 (λ x z b c → x :+ z :+ (b :+ c) := z :+ b :+ (x :+ c)) refl x z b c
  where open CommSemiringSolver ℕ-csr

直接把上述add-canc-case x z a b c d u填入代码的大括号位置即可通过类型检查。

内容的提问来源于stack exchange，提问作者Junkyards