Use the ringsolver with variables in context

[mzeuner]

I often find myself in the situation where I want to use the ring solver for parts of a long argument like this:

...  ≡⟨ ... ⟩
s · r'₁ · s₁ · s₂ · s₂ + s · r₂ · s₁ · s'₁ · s₂  ≡⟨ ? ⟩
s · (r'₁ · s₂ + r₂ · s'₁) · (s₁ · s₂)  ≡⟨ ... ⟩ 
...

Here you would want to just write solve R' for ?, but since all the variables are in the context at this goal, what you have to do instead is to use the ring solver to get a path

eq2 : (r₁ s₁ r'₁ s'₁ s'₁ r₂ s₂ s : R)
    → s · r'₁ · s₁ · s₂ · s₂ + s · r₂ · s₁ · s'₁ · s₂ ≡ s · (r'₁ · s₂ + r₂ · s'₁) · (s₁ · s₂)
eq2 = solve R'

and then fill the goal with eq2 r₁ s₁ r'₁ s'₁ s'₁ r₂ s₂ s. This example can be found in the library at: https://github.com/agda/cubical/blob/master/Cubical/Algebra/CommRing/Localisation/Base.agda#L141

It would great if the ring solver could work with arguments from the context and it would save us quite a bit of boiler-plate code.

[felixwellen]

This is mostly solved by #585. More precisely, the feature as requested above works, if the variables for the ring solver are introduced after all other variables. The remaining problem requires more work with deBrujin indices and I won't work on it any time soon.