How do you use the Ring solver in Cubical Agda?

Question

I have started playing around with Cubical Agda. Last thing I tried doing was building the type of integers (assuming the type of naturals is already defined) in a way similar to how it is done in classical mathematics (see the construction of integers on wikipedia). This is

data dInt : Set where
    _⊝_ : ℕ → ℕ → dInt 
    canc : ∀ a b c d → a + d ≡ b + c → a ⊝ b ≡ c ⊝ d 
    trunc : isSet (dInt)

After doing that, I wanted to define addition

_++_ : dInt → dInt → dInt 
(x ⊝ z) ++ (u ⊝ v) = (x + u) ⊝ (z + v)
(x ⊝ z) ++ canc a b c d u i = canc (x + a) (z + b) (x + c) (z + d) {!   !} i
...

I am now stuck on the part between the two braces. A term of type x + a + (z + d) ≡ z + b + (x + c) is asked. Not wanting to prove this by hand, I wanted to use the ring solver made in Cubical Agda. But I could never manage to make it work, even trying to set it up for simple ring equalities like x + x + x ≡ 3 * x.

How can I make it work ? Is there a minimal example to make it work for naturals ? There is a file NatExamples.agda in the library, but it makes you have to rewrite your equalities in a convoluted way.

Answer 1

I've successfully used the ring solver for exactly the same problem: defining Int as a quotient of ℕ ⨯ ℕ. You can find the complete file here, the relevant parts are the following:

1. Non-cubical propositional equality to path equality:

open import Cubical.Core.Prelude renaming (_+_ to _+̂_)

open import Relation.Binary.PropositionalEquality renaming (refl to prefl; _≡_ to _=̂_) using ()
fromPropEq : ∀ {ℓ A} {x y : A} → _=̂_ {ℓ} {A} x y → x ≡ y
fromPropEq prefl = refl

2. An example of using the ring solver:

open import Function using (_$_)

import Data.Nat.Solver
open Data.Nat.Solver.+-*-Solver
  using (prove; solve; _:=_; con; var; _:+_; _:*_; :-_; _:-_)

reorder :  ∀ x y a b → (x +̂ a) +̂ (y +̂ b) ≡ (x +̂ y) +̂ (a +̂ b)
reorder x y a b = fromPropEq $ solve 4 (λ x y a b → (x :+ a) :+ (y :+ b) := (x :+ y) :+ (a :+ b)) prefl x y a b

So here, even though the ring solver gives us a proof of _=̂_, we can use _=̂_'s K and _≡_'s reflexivity to turn that into a path equality which can be used further downstream to e.g. prove that Int addition is representative-invariant.

Answer 2

You can see how the solver for natural numbers is supposed to be used in this file in the cubical library:

Cubical/Tactics/NatSolver/Examples.agda

Note that this solver is different from the solver for commutative rings, which is designed for proving equations in abstract rings and is explained here:

Cubical/Tactics/CommRingSolver/Examples.agda

However, if I read your problem correctly, the equality you want to prove requires the use of other propositional equalities in Nat. This is not supported by any solver in the cubical library (as far as I know, also the standard library doesn't support it). But of course, you can use the solver for all the steps that don't use other equalities.

Just in case you didn't spot this: here is a definition of the integers in math-style using the SetQuotients of the cubical library. SetQuotients help you to avoid the work related to your third constructor trunc. This means you basically just need to show some constructions are well defined as you would in 'normal' math.