Zulip Chat Archive

Stream: new members

Topic: ring solver

Thorsten Altenkirch (Sep 05 2020 at 15:10):

@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 (Sep 05 2020 at 15:21):

Maybe I was worried about natural number subtraction?

Kevin Buzzard (Sep 05 2020 at 15:22):

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

Bryan Gin-ge Chen (Sep 05 2020 at 15:39):

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 (Sep 05 2020 at 15:49):

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

Thorsten Altenkirch (Sep 05 2020 at 15:56):

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 (Sep 05 2020 at 16:01):

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

Reid Barton (Sep 05 2020 at 16:01):

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

Last updated: Dec 20 2023 at 11:08 UTC