[Agda] Commutativity problems in RingSolver

[Nils Anders Danielsson]

On 2010-08-17 19:11, Christoph HERRMANN wrote:
> In the attached file function *checkWorks* typechecks, which means
> that the application of function *foo* is reduced.

Your code:

   checkWorks : ((toNF (foo (con 1) vN)) ≡ (toNF ((con 1) :+ vN))) → Set
   checkWorks _ = ⊤

   checkFails : ((toNF ((con 0) :+ (con 1))) ≡ (toNF ((con 1) :+ (con 0)))) → Set
   checkFails _ = ⊤

Here checkFails fails because (toNF ((con 0) :+ (con 1))) and
(toNF ((con 1) :+ (con 0))) have different types
(Normal 2 (con 0 :+ con 1) and Normal 2 (con 1 :+ con 0)).

> Function checkFails delivers a type error which basically says that 0 unequal 1,
> so commutativity  of + is not exploited by the ring solver.

This is not the way the ring-solver is supposed to be used, as you later
found out. The RingSolver module states the following:

-- For examples of how solve and _:=_ can be used to
-- semi-automatically prove ring equalities, see, for instance,
-- Data.Digit or Data.Nat.DivMod.

There is also an example in README.Nat.

--
/NAD