关于如何使用 Agda 标准库幺半群求解器的示例

Question

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

有人可以提供一个使用 stdlib 幺半群求解器的简单示例吗？

最佳，

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 and 2，你可以用类似的方式写一个幺半群求解器的前端。

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

同时检查 this 线程。

关于如何使用 Agda 标准库幺半群求解器的示例

An example on how to use Agda Standard Library monoid solver

agda