status of `ring`

Stream: mathlib4

[Scott Morrison]

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]

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]

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

[Scott Morrison]

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]

Yes, that's what I meant

[Mario Carneiro]

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]

but of course the proof of those statements have dependencies etc

[Scott Morrison]

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]

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