[Agda] Re: about RingSolver

[Sergei Meshveliani]

On Thu, 2016-01-28 at 14:19 +0100, Nils Anders Danielsson wrote:
> On 2016-01-28 12:56, Sergei Meshveliani wrote:
> > 1. RingSolver of Standard library is not for solving algebraic
> >     equations.
> > It is for forming proofs for universal algebraic equalities.
> > For example,
> >      "find a proof for that the equality
> >                             (x + 1) * (x - 1) ≈ x * x - 1
> >       holds for all  x  in any ring.
> >      "
> > is done by calling `solve' with appropriate arguments.
> 
> This is not quite true. Here is an example taken from "Proving
> Equalities in a Commutative Ring Done Right in Coq" by Grégoire and
> Mahboubi (http://doi.org/10.1007/11541868_7):
> 
>    example : (b : Bool) → b xor b ≡ false
>    example = solve 1 (λ b → b :+ b := con false) refl
>      where open XorRingSolver
> 
> We don't have x + x ≡ 0 for arbitrary x in an arbitrary ring.
> 


Indeed, my explanation needs correction. 

Probably, the term   b + b  is normalized here according to the
equations of the domain (universal algebra ?) of  XorRingSolver.  
And it is normalized to `false', and this makes it a proof.
Right?

What equations (rules) are contained in  XorRingSolver ?

I expect that its equation (law) set E has 
associativity, commutativity, distributivity of several kinds.
I also expect that it also has the law  
                                   X + X ≡ false  ( ≡ 0),
where  _+_ stands for _xor_.
Right?
I expect that this makes it "Arbitrary Boolean ring E".

Respectively, the above `solve' call proves 
                                \forall X (X + X ≡ false)  
for all Boolean rings. 

Probably, `solve' RingSolver searches for a proof "in variety", -- by a
certain normalization only, -- in a specified category (variety)  D  of
domains (universal algebras).
What this D can be?
In can be CommutativeRing.
Probably it also can be an extension (by adding some operations) of
CommutativeRing 
(?)
For example, a Boolean ring 
(I do not recall now: is a Boolean ring really a ring?).

Still I doubt, how to describe plainly: what `solve' of RingSolver
can prove.

Regards,

------
Sergei