Пример использования монолитного решателя библиотеки Agda Standard Library

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 

Агда может частично определить тип подписи:

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

Есть также по крайней мере две передние концы для кольца решатель: 1 и 2, вы можете написать интерфейс для моноидного решателя аналогичным образом.

Считаете ли вы использование списков различий, имеющих ассоциативность определения?

Проверить this нить тоже.