Пример о том, как использовать стандартные библиотеки Агды решатель моноидом

Я разрабатываю код с большим количеством скучных равенств конкатенации списков, поэтому я хочу использовать моноидный решатель. Я знаю эту модульную алгебру.Моноид-решатель реализует моноидный решатель, но я не нахожу ни одного примера, как его использовать.

Может ли кто-нибудь привести быстрый пример использования моноидного решателя stdlib ?

Лучший,

1 4
agda

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, аналогичным образом можно написать интерфейс для моноидного решателя.

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

Проверьте такжеЭТУ нить.

4