Where to open a PR to upstream ENNReal normaliser tactic

Stream: mathlib4

[Willem vanhulle]

I am searching for a good place to upstream a tactic I wrote to normalize ENNReal (non-negative extended real) numbers. I refactored it a lot and I have been looking at several places in Mathlib to upstream it (such as Mathlib/Tactic/NormNum or ), but Mathlib is quite big and maybe its better if I just ask this group. Does anyone have a suggestion? I also have quite a lot of unit tests coming with this tactic.

This is the github project: ennreal-arith

[Kim Morrison]

Can you describe its spec?

[Willem vanhulle]

Kim Morrison said:

Can you describe its spec?

It’s a tactic that searches for atomic numbers and associated finiteness proofs and lifts the ENNReal to the reals. It solves it in the reals using ring and norm_num. Works with basic equations.

[Michael Rothgang]

What does the tactic do if the first step (lifting) works, but the second one (prove in R) fails?

[Michael Rothgang]

(Should these be two separate tactics? Or should the tactic do only the first, if it succeeds? The in-progress field tactic does the latter, so there is some precedent.)

[Kim Morrison]

"basic equations" seems pretty vague. I'd much prefer to see the lifting part as a standalone --- can this be done using lift?

[Willem vanhulle]

Michael Rothgang said:

(Should these be two separate tactics? Or should the tactic do only the first, if it succeeds? The in-progress field tactic does the latter, so there is some precedent.)

It emits an error saying the equality is not true.

[Willem vanhulle]

Kim Morrison said:

"basic equations" seems pretty vague. I'd much prefer to see the lifting part as a standalone --- can this be done using lift?

Maybe it could be done with the lift tactic, but I’m still fairly new to lean. I don’t know how to use it yet.

[Willem vanhulle]

Kim Morrison said:

"basic equations" seems pretty vague. I'd much prefer to see the lifting part as a standalone --- can this be done using lift?

I had a try to use the lift tactic and implemented the CanLift class but I couldn’t rewrite my tactic definition into using the lift tactic.

[Jireh Loreaux]

I think a better reference for this might be something like the enat_to_nat tactic, described here: docs#Mathlib.Tactic.ENatToNat.tacticEnat_to_nat. Having this for ennreal_to_real or ennreal_to_nnreal would be nice. Then your tactic would just become ennreal_to_real; norm_num.

[Jireh Loreaux]

Of course, if it's possible to unify these tactics somehow, that would be even better.

[Willem vanhulle]

Jireh Loreaux said:

I think a better reference for this might be something like the enat_to_nat tactic, described here: docs#Mathlib.Tactic.ENatToNat.tacticEnat_to_nat. Having this for ennreal_to_real or ennreal_to_nnreal would be nice. Then your tactic would just become ennreal_to_real; norm_num.

That looks like a really useful reference! Thanks! Maybe my tactic could as short as well :smile:.

[Kim Morrison]

Jireh Loreaux said:

Of course, if it's possible to unify these tactics somehow, that would be even better.

I assume you mean "unify enat_to_nat with ennreal_to_real". This is a good idea.

I hope you don't mean "unify ennreal_to_real with norm_num". This is a bad idea (there is a unification that would be useful, but it is not possible to reach that point starting with, or calling, norm_num).