Zulip Chat Archive

Stream: mathlib4

Topic: status of `ring`


Scott Morrison (Oct 14 2022 at 05:26):

I just reached the point debugging my port of linarith where it is failing because ring doesn't know about subtraction!

So --- @Mario Carneiro, are you planning on working on that? Or have advice/suggestions about what needs to be done?

Mario Carneiro (Oct 14 2022 at 05:28):

I'm planning on working on it. I need to finish norm_num first (make it so it understands rational arithmetic), so if you would like to help how about porting all the theorems used in the norm_num and ring files?

Scott Morrison (Oct 14 2022 at 05:34):

A busy non-lean weekend is coming up here, but I'll make a start!

Scott Morrison (Oct 14 2022 at 09:47):

I'm not entirely certain what you meant by

porting all the theorems used in the norm_num and ring files?

I'm for now interpreting this as:

  • find all the back-ticked identifiers in the norm_num and ring files in mathlib3
  • filter out just the lemmas
  • determine whats already in mathlib4
  • for the remainder, either
    • port the file it lives in if that is trivial to do
    • put a sorried statement of the lemma somewhere in mathlib4 (with a reference to where it eventually belongs)

Mario Carneiro (Oct 14 2022 at 10:01):

Yes, that's what I meant

Mario Carneiro (Oct 14 2022 at 10:03):

most of the lemmas are in the norm_num/ring files themselves, so you can just look for theorem/ lemma in those tactic files

Mario Carneiro (Oct 14 2022 at 10:03):

but of course the proof of those statements have dependencies etc

Scott Morrison (Oct 14 2022 at 10:32):

I've done the "external" dependencies, i.e. outside lemmas that are referenced directly from norm_num or ring, as mathlib4#471 and mathlib4#472. In internal dependencies (i.e. lemmas in the tactics files) I may not get to until after the weekend.

Scott Morrison (Oct 14 2022 at 10:32):

(and these have sorries, and two lemmas are noted but not even stated because we don't have Field.)


Last updated: Dec 20 2023 at 11:08 UTC