ring solver

Stream: new members

[Thorsten Altenkirch]

@Kevin Buzzard said that it was easier to write a ring solve than a solver for semi-rings.
I would like to understand this. It seems to me that in both cases we simply exploit the fact that polynoms are the initial ring/semi-ring but in the latter case the coefficients are natural numbers and not integers.

[Kevin Buzzard]

Maybe I was worried about natural number subtraction?

[Kevin Buzzard]

Maybe I was wrong :-) Where did I say it?

[Bryan Gin-ge Chen]

I guess the precise quote is here:
Kevin Buzzard said:

We gave up trying to make the simplifier prove things about semirings and someone wrote a ring tactic instead.

[Reid Barton]

To clarify, the ring tactic also proves things about semirings--it just isn't based on the simplifier.

[Thorsten Altenkirch]

Yes, I guess what @Kevin Buzzard wanted to say was that it is just as easy to write a ring solver as it is to write a semi-ringsolver. Actually not exactly because for the ring you need that the integers are a ring while for the semi-ring you only need that the natural numbers are a semi-ring which is easier to prove. Actually how exactly are integers implemented in lean? Signed representation is good for computation but bad for reasoning, quotients are good for reasoning but bad for computation. In cubical you can have both...

[Kevin Buzzard]

Signed representation with a solid API is fine for reasoning. It's all about the API.

[Reid Barton]

You have jump-to-definition set up in emacs right? Type #check int and press M-.