## Stream: general

### Topic: fpow neg normal form

#### Johan Commelin (Sep 25 2019 at 18:33):

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.

Is n : nat here?

#### Johan Commelin (Sep 25 2019 at 19:09):

No n : int

#### Reid Barton (Sep 25 2019 at 19:17):

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

#### Reid Barton (Sep 25 2019 at 19:28):

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

#### Johan Commelin (Sep 25 2019 at 19:29):

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

#### Johan Commelin (Sep 25 2019 at 19:30):

But that doesn't need to happen, right?

#### Johan Commelin (Sep 25 2019 at 19:30):

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

#### Johan Commelin (Sep 25 2019 at 19:31):

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

#### Reid Barton (Sep 25 2019 at 20:43):

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 (Sep 25 2019 at 20:47):

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

#### Johan Commelin (Oct 08 2019 at 19:48):

#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 (Oct 08 2019 at 19:49):

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

#### Johan Commelin (Oct 08 2019 at 19:50):

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 (Oct 09 2019 at 01:05):

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

Last updated: May 08 2021 at 04:14 UTC