fpow neg normal form

Stream: general

[Johan Commelin]

I've been playing with fpow in the perfectoid project. We have the following expressions:
x^(-n), (1/x)^n, 1/(x^n) and x¯¹ ^n.
Moving between these is pretty annoying atm. I think the library hasn't really decided on a "normal" form. It isn't really clear to me which one would be best.

[Kevin Buzzard]

Is n : nat here?

[Johan Commelin]

No n : int

[Reid Barton]

Of these x^(-n) "looks" the "most normal" to me, but that is not based on much

[Reid Barton]

I guess people would object if we started simplifying 1/2 to 2⁻¹, though

[Johan Commelin]

It would be 2^(-1) :wink:

[Johan Commelin]

But that doesn't need to happen, right?

[Johan Commelin]

Because 1/2 doesn't match one of the 4 forms that I gave above.

[Johan Commelin]

It's only 1/(2^1) that matches. So using priorities (!!) we can make sure that we still get the desired result.

[Reid Barton]

Ah, I was figuring the easiest way to deal with it would be to simplify 1/x to x^(-1), (x^a)^b to x^(a*b) and then have rules for multiplying negatives together

[Bryan Gin-ge Chen]

Is this the sort of thing where looking at what computer algebra systems do would be helpful?

[Johan Commelin]

#1522 is using 1/x in its statements. It think this discussion didn't really converge onto a normal form yet. Does anyone have some 2cts to contribute?

[Patrick Massot]

There is no simp lemma in this PR, so it doesn't claim anything about a normal form.

[Johan Commelin]

Well, I think other lemmas should still use the normal form as much as possible... because it will be easier to chain things.

[Floris van Doorn]

I think those lemmas are still useful to have even if they are not simp normal form.