Zulip Chat Archive

Stream: general

Topic: fpow neg normal form


view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Sep 25 2019 at 19:08):

Is n : nat here?

view this post on Zulip Johan Commelin (Sep 25 2019 at 19:09):

No n : int

view this post on Zulip 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

view this post on Zulip Reid Barton (Sep 25 2019 at 19:28):

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

view this post on Zulip Johan Commelin (Sep 25 2019 at 19:29):

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

view this post on Zulip Johan Commelin (Sep 25 2019 at 19:30):

But that doesn't need to happen, right?

view this post on Zulip Johan Commelin (Sep 25 2019 at 19:30):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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