Dependencies of abel

Stream: mathlib4

[Yaël Dillies]

I just came to realising something really quite bad about our import tree, and I do not immediately know how to solve it.

[Yaël Dillies]

abel depends on norm_num to normalise numerals, and norm_num depends on Field to handle fractions (in fact it even depends on LinearOrderedField to handle nonnegative fractions through NNRat, but I'm pretty sure I know how to fix this).

[Yaël Dillies]

This means that eg the definition of docs#Module can't be made without importing LinearOrderedField. Of course, one could just move to a later file or eliminate the uses of abel, but that's solving the symptom, not the disease.

[Yaël Dillies]

Can we make it so that abel, a tactic about commutative groups, does not need to know about linearly ordered fields?

[Johan Commelin]

Shouldn't the plug-in system of norm_num mean that you can use a barebones norm_num in abel in low-level files, and norm_num (and hence abel) become more powerful once you import higher-level files?

[Yaël Dillies]

I would hope so, but currently Tactic.Abel imports Tactic.NormNum

[Johan Commelin]

I mean, I understand that is not how it currently works... but it seems that it would be good to make it work like that.

[Yaël Dillies]

Actually, what even is the point of fractions in abel? It's only dealing with Int and Nat, right?

[Yaël Dillies]

Even if we scrap the support for fractions, we still have the issue that those Int and Nat equalities are backed by Ring. That's definitely better than LinearOrderedField, but still not great

[Mario Carneiro]

I think this is not worth it. abel uses norm_num and norm_num uses rational numbers in the framework code (not the add-ons). I would instead suggest pulling out a minimal version of fields which Tactic.NormNum.Core can import, and use that whenever you need abel; or don't use abel and prove it by hand / by group

[Yaël Dillies]

I know that, Mario, but plenty of properties of Rat are proved without using Field, so I'm not convinced norm_num really must depend on Field

[Eric Wieser]

Is the issue here the way that norm_num caches algebraic instances in it's result type?

[Mario Carneiro]

yes

[Mario Carneiro]

and also when it has to compute with them

[Mario Carneiro]

Yaël Dillies said:

I know that, Mario, but plenty of properties of Rat are proved without using Field, so I'm not convinced norm_num really must depend on Field

It's not storing Rat, it's storing rational expressions in a Field

[Mario Carneiro]

all math is performed over appropriate algebraic classes

[Mario Carneiro]

on the "programming side" that means working with Rat but the generated proofs make no reference to Rat and only use field axioms

[Mario Carneiro]

IMO all the lemmas etc are already being applied as late as they reasonably can be. Feel free to try to separate out the minimum requirements, but I don't think it is worth trying to cleave norm_num into two tactics, which is what you would need to do to make it not know about/handle rational numerals

[Yaël Dillies]

I think your idea of a custom Field typeclass could make sense

[Eric Wieser]

Removing abel from the file that defines Module seems like a more reasonable thing to aim for

[Eric Wieser]

Tactics are hard enough to write without making more rules about what they aren't allowed to import

[Yaël Dillies]

Okay but that doesn't solve the fact that abel is a tactic about commutative groups

[Mario Carneiro]

no, it's more like a tactic about Z-modules

[Eric Wieser]

I suppose there could be an abel_core tactic for early files which does not normalize numerals? (And so doesn't need norm_num)

[Mario Carneiro]

I think that's simp [add_assoc, add_left_comm, add_comm]

[Mario Carneiro]

There is no need to use abel at all in early files

[Eric Wieser]

I've seen a lot of places where abel can be replaced with rw [add_add_add_comm]

[Yaël Dillies]

#13274

[Eric Wieser]

I'd be happy to merge the de-abel bit, but don't have time to review the scope creep moves right now

[Kim Morrison]

Yes, this PR should be split according to paragraphs in the description, no need to do it all at once?

[Yaël Dillies]

I mean the first part is tiny? It's three lines of diff. The main part is the second one

[Eric Wieser]

Well, we can't tell that by looking at the PR; how many of the transitive import changes were caused by the abel/rw swap? If they were separate PRs then the answer would be obvious

[Yaël Dillies]

I've opened a separate PR #13305 and removed its diff from #13274

[Kim Morrison]

Imports aren't quite right yet, but LGTM.

[Yaël Dillies]

#13305 passes CI. #13274 will pass CI soon.