[Agda] RingSolver, normalisation

[Christoph HERRMANN]

Hi,

I would like to use function *normalise* from the *RingSolver* module.
Therefore I removed the private declaration. However, when I
tried to use the function an error message occured which I do
not understand. Does anyone have an idea what the message
p != .p means?

Also, we need polynomials with natural coefficients and
variables; therefore I used the *Simple* interface. Is this correct? 

The import declarations, definitions and error message are
listed below. I'm using Agda 2.2.6 and the standard library
version 0.3.

Many thanks in advance
-----------------------------
-- import declarations

open import Data.Bool
open import Data.Unit
open import Data.Fin renaming ( zero to fzero ; suc to fsuc )
open import Data.Nat
open import Data.Nat.Properties
open import Data.Product
import Algebra.RingSolver.Simple as Solver
import Algebra.RingSolver.AlmostCommutativeRing as ACR
open Solver (ACR.fromCommutativeSemiring commutativeSemiring) 
-----------------------------
-- definitions

NF : Set
NF = {p : Polynomial 2} → Normal 2 p

foo : Polynomial 2 → NF 
foo p = normalise p
-----------------------------
-- error message

p != .p of type
.Algebra.RingSolver.Polynomial
(.Algebra.RingSolver.Simple._.rawRing
 (ACR.fromCommutativeSemiring commutativeSemiring))
(ACR.fromCommutativeSemiring commutativeSemiring)
(ACR.-raw-almostCommutative⟶
 (ACR.fromCommutativeSemiring commutativeSemiring))
2
when checking that the expression normalise p has type
.Algebra.RingSolver.Normal
(record
   {Carrier = ℕ; _+_ = λ x x' → Data.Nat._+_ x x';
    _*_ = λ x x' → x * x'; -_ = .Data.Function.id; 0# = 0; 1# = 1})
(record
   {Carrier = ℕ; _≈_ = λ x x' → .Relation.Binary.Core.Dummy._≡_ x x';
    _+_ = λ x x' → Data.Nat._+_ x x'; _*_ = λ x x' → x * x';
    -_ = .Data.Function.id; 0# = 0; 1# = 1;
    isAlmostCommutativeRing =
      record
        {isCommutativeSemiring =
           record
             {isSemiring =
                record
                  {isSemiringWithoutAnnihilatingZero =
                     record
                       {+-isCommutativeMonoid =
                          record
                            {isMonoid =
                               record
                                 {isSemigroup =
                                    record
                                      {isEquivalence =
                                         record
                                           {refl = λ {.x} → .Relation.Binary.Core.Dummy.refl;
                                            sym =
                                              λ {.i} {.j} →
                                                .Relation.Binary.PropositionalEquality.Core.sym;
                                            trans =
                                              λ {.i} {.j} {.k} →
                                                .Relation.Binary.PropositionalEquality.Core.trans};
                                       assoc = .Data.Nat.Properties.+-assoc;
                                       ∙-cong =
                                         λ {.x} {.y} {.u} {.v} →
                                           .Relation.Binary.PropositionalEquality.cong₂
                                           Data.Nat._+_};
                                  identity =
                                    (λ _ → .Relation.Binary.Core.Dummy.refl) ,
                                    .Data.Nat.Properties._.n+0≡n};
                             comm = .Data.Nat.Properties.+-comm};
                        *-isMonoid =
                          record
                            {isSemigroup =
                               record
                                 {isEquivalence =
                                    record
                                      {refl = λ {.x} → .Relation.Binary.Core.Dummy.refl;
                                       sym =
                                         λ {.i} {.j} →
                                           .Relation.Binary.PropositionalEquality.Core.sym;
                                       trans =
                                         λ {.i} {.j} {.k} →
                                           .Relation.Binary.PropositionalEquality.Core.trans};
                                  assoc = .Data.Nat.Properties.*-assoc;
                                  ∙-cong =
                                    λ {.x} {.y} {.u} {.v} →
                                      .Relation.Binary.PropositionalEquality.cong₂ _*_};
                             identity =
                               .Data.Nat.Properties._.n+0≡n , .Data.Nat.Properties._.n*1≡n};
                        distrib =
                          .Data.Nat.Properties._.distˡ , .Data.Nat.Properties._.distʳ};
                   zero =
                     (λ _ → .Relation.Binary.Core.Dummy.refl) ,
                     .Data.Nat.Properties._.n*0≡0};
              *-comm = .Data.Nat.Properties.*-comm};
         -‿cong = λ {.i} {.j} → .Data.Function.id;
         -‿*-distribˡ = λ _ _ → .Relation.Binary.Core.Dummy.refl;
         -‿+-comm = λ _ _ → .Relation.Binary.Core.Dummy.refl}})
(record
   {⟦_⟧ = .Data.Function.id;
    +-homo = λ _ _ → .Relation.Binary.Core.Dummy.refl;
    *-homo = λ _ _ → .Relation.Binary.Core.Dummy.refl;
    -‿homo = λ _ → .Relation.Binary.Core.Dummy.refl;
    0-homo = .Relation.Binary.Core.Dummy.refl;
    1-homo = .Relation.Binary.Core.Dummy.refl})
2 .p
-----------------------------
Many thanks
--
 Dr. Christoph Herrmann
 University of St Andrews, Scotland/UK
 phone: office: +44 1334 461629, home: +44 1334 478648 
 email: ch at cs.st-andrews.ac.uk,  c.herrmann at virgin.net
 URL:   http://www.cs.st-andrews.ac.uk/~ch
 
 The University of St Andrews is a charity registered in Scotland: No SC013532