[Agda] Solver usage

[Sergei Meshveliani]

On Wed, 2019-01-23 at 09:35 +0100, Nils Anders Danielsson wrote:
> 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 _≟_:


It is principal, that the goal to be proved for an arbitrary
CommutativeRing.

Maybe the prover could be adopted to the case of  
          CommutativeRing  + the axiom of  0# ≉ 1# ?

Also, it looks like it fails to prove  x - x ≈ 0#,
which can be derived from the Group instance for _+_.

Maybe, it can be all fixed by bringing-in polynomials over Integer,
as you write below (I guess this construct is basic in the standard
equality prover).

My current concrete goal is, probably, simpler.
The question is: 
how to prove with RingSolver the following three equalities in an 
arbitrary  CommutativeSemiring: 

 (I)
 (((n1 * d2 + n2 * d1) * d3) + n3 * d12) * (d1 * d23)	
 ≈
 (n1 * d23 + (n2 * d3 + n3 * d2) * d1) * (d12 * d3)

 (II)
 (n * n') * (d * d'') + (n * n'') * (d * d')  ≈
 d * (n * (n' * d'' + n'' * d'))

 (III)
 ((p'G * p'N) * g₂₃) * (g₁₂ * (pG * pD))  ≈
 ((g₁₂ * g₂₃) * (pG * p'G)) * (p'N * pD)
?

All the variables here are under  \forall (... : Carrier). 

I can set a proof by hand, but I thought that it is nicer to call some
prover.
I have two large modules of my home-made prover for
(Commutative)Semiring. And it proves these three.
But it is better to use some standard prover, because I have a small
application which needs to be as close to standard library as possible.

Can anybody, please, show how to use the standard solver to prove any
one of the above three equalities? 

Thanks,

------
Sergei



>    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.
>