[Agda] how to use monoid solver and how to derive a concept monoid if assume we do not know monoid

[Sergei Meshveliani]

On Mon, 2015-12-14 at 19:21 +0800, Mandy Martino wrote:

> Hi ,
> i find many places  define  identity, symmetric and  transitive,   how
> to  use  monoid  solve and  which  can  it  solve?
>
>
> i would like  to define a new  set  of  equivalence relations,  is  
> there  a  light  weight  version of  monoid?

See in Wikipedia what is a monoid.
Monoid  in Standard library is adequate, it cannot be any more
"light weight".

Monid has the axioms of
(1) associativity for _∙_,   (2) identity (ε).


> how to use  monoid  solve and  which  can  it  solve?

Earlier I tried  SemiringSolver  for  Nat.
And I guess that  MonoidSolver  uses a similar principle of reduction to
a normal form
(let people correct me, if I mistake).

For monoid:
having expressions        e1  and  e2,
a proof for the equality
                          e1 ≈ e2    (E)

can be searched by applying the  `solve'  function.
`solve' brings  e1  and  e2  to their certain normal forms  e1' and e2'.
This is done by moving parentheses (by using the associativity law),
and canceling  ε  by using the identity law.
Then, if  e1'  and  e2'  coincide
(are equal by  Equivalence.refl  contained in the setoid),
then the result of `solve'  is a proof for  (E).
Otherwise, some other proof may exist or not.

In various instances of Monoid there may exist many equations or
statements which can be proved but are not proved by  MonoidSolver.

Example of a proof:
I expect that `solve' will bring  e1 =  (x ∙ (e ∙ x)) ∙ (y ∙ e)
and                               e2 =  (e ∙ (x ∙ x)) ∙ y

by using the laws of  associativity and identity to the same expression

                             x ∙ (x ∙ y).
And this proves the equality

                (x ∙ (e ∙ x)) ∙ (y ∙ e)  ≈  (e ∙ (x ∙ x)) ∙ y

for any Monoid.

I do not know how precisely MonoidSolver is used.
But I have an example of using  SemiringSolver,  and I expect that
MonoidSolver has a similar usage.

For  Nat (n : Nat) :

  open import Data.Nat.Properties using (module SemiringSolver)

  open SemiringSolver using (solve; _:=_; con; _:+_; _:*_)

  e :  suc (suc (n + n)) ≡ 2 * suc n
  e =  solve 1 (\n →  con 1 :+ (con 1 :+ (n :+ n))  :=
                      (con 2) :* (con 1 :+ n)
               )
               PE.refl n

I guess that `solve' does the following. It has

  e1 =  1 + (1 + (n + n))
  e2 =  (1 + (1 + 0)) * (1 + n),

and it brings both terms to this normal form:
                                              1 + (1 + (n + n)).

It is done only by using the axioms of an arbitrary (commutative) ring.

I have arranged this by looking into the source of Standard library,
where it uses SemiringSolver, I just mimic the usage.

I guess that under this `solve',
`con' is a tag for a constant,  `:' is a tag for an operator,
all other items (in this case it is `n') are variables in a term.

I expect that  MonoidSolver  has a similar usage.


> assume we do not know monoid,  how to build  a concept such as  
> monoid  based  on  custom  equivalence  relations?

I do not know what is a  custom equivalence relation.
So I cannot tell.

Regards,

------
Sergei