module CheckSolver where

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
open import Relation.Binary.PropositionalEquality

import Algebra.RingSolver.Simple as Solver
import Algebra.RingSolver.AlmostCommutativeRing as ACR
open Solver (ACR.fromCommutativeSemiring commutativeSemiring) 

Ex : Set
Ex = Polynomial 2 

vM : Ex
vM = var fzero

vN : Ex
vN = var (fsuc fzero)

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

toNF : (p : Polynomial 2) → NF {p}
toNF p = normalise p

foo : Ex → Ex → Ex
foo m n = m :+ n 

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 _ = ⊤