agda - 如何使用 Agda 标准库 monoid 求解器的示例

Question

我正在开发一个包含很多无聊列表连接等式的代码，所以我确实想使用一个幺半群求解器。我知道模块 Algebra.Monoid-solver 实现了一个幺半群求解器，但我没有找到任何关于如何使用它的示例。

有人可以提供一个使用 stdlib monoid 求解器的快速示例吗？

最好的，

Answer 1

这是一个简单的例子:

open import Relation.Binary.PropositionalEquality
open import Data.List
open import Data.List.Properties
open List-solver renaming (nil to :[]; _⊕_ to _:++_; _⊜_ to _:≡_)

assoc : {A : Set} (xs ys zs : List A) -> xs ++ (ys ++ zs) ≡ (xs ++ ys) ++ zs
assoc = solve 3 (λ xs ys zs -> xs :++ (ys :++ zs) :≡ (xs :++ ys) :++ zs) refl

Agda 可以部分推断类型签名:

assoc : {A : Set} (xs ys zs : List A) -> _
assoc = solve 3 (λ xs ys zs -> xs :++ (ys :++ zs) :≡ (xs :++ ys) :++ zs) refl

环形求解器还有至少两个前端: 1和 2 ，您可以以类似的方式为幺半群求解器编写前端。

您是否考虑过使用具有定义关联性的差异列表？

查看 this线程也。