[Agda] Solver usage

[Nils Anders Danielsson]

On 30/12/2018 23.01, Sergei Meshveliani wrote:
> And it does not work.
> Please, how to fix?

First, give the arguments in the right order:

   solve 2 (λ x y →  ((x :* y) :- (y :* x)) := (con 0#))
         ? a b

Giving reflexivity in the hole still does not work. I looked at the
normalised goal type, and it contains subexpressions like

   CommutativeRing.1# R ≟ 0#.

This expression is stuck, which is not so surprising, given that you
have not used a concrete ring or a concrete implementation of _≟_:

   module _ {α α=} (R : CommutativeRing α α=)
                   (open CommutativeRing R using (_≈_))
                   (_≟_ : Decidable _≈_)

We can take things a little further by instantiating the ring solver in
a different way:

   open import Algebra
   open import Algebra.Solver.Ring.AlmostCommutativeRing
   open import Data.Maybe

   module _ {α α=} (R : CommutativeRing α α=) where

     open CommutativeRing R

     open import Algebra.Solver.Ring
       (AlmostCommutativeRing.rawRing (fromCommutativeRing R))
       (fromCommutativeRing R)
       (-raw-almostCommutative⟶ (fromCommutativeRing R))
       (λ _ _ → nothing)

     lemma : (a b : Carrier) → ((a * b) - (b * a)) ≈ 0#
     lemma a b =
       solve 2 (λ x y →  ((x :* y) :- (y :* x)) := (con 0#))
             {!!} a b

Here, as a first try, I have instantiated the "weak decision procedure"
with λ _ _ → nothing. Now the normalised goal type is readable:

   {x : Carrier} {x = x₁ : Carrier} →
   (0# * x + ((0# * x₁ + (1# * 1# + - 1# * 1# * (1# * 1#))) * x₁ +
              (1# * 0# + - 1# * 1# * (0# * 1#)))) * x + 0# ≈
   0# * x + (0# * x₁ + 0#)

You can see that there are a number of "obvious" simplifications that
have not been performed. I think that a good way to proceed would be to
instantiate the coefficient ring with the usual commutative ring over
the integers. The standard library already contains such an
instantiation for commutative *semirings* (using the natural numbers
instead of the integers), but I did not find one for the integers.

See Section 4 of "Proving Equalities in a Commutative Ring Done Right in
Coq" by Grégoire and Mahboubi (https://doi.org/10.1007/11541868_7) for
more information.

-- 
/NAD