integer group powers

[Alizter]

We generalise group powers to integers. The nat based powers become a special case.

@ThomatoTomato I've left two parts incomplete if you would like to finish them. Make sure to remove any axioms or Admitteds. You may push directly to this branch. If pushing doesn't work, then you can just create a new PR.

[jdchristensen]

Another approach to grp_pow is to develop something like Spaces/BinInt/Equiv.v for the newer integers, which let you define a function from the integers into a pointed type with a self-equivalence. Some of the properties are true in that generality. Not sure whether it would complicate things here to use that more general construction.

[Alizter]

This implementation doesn't compute particularly well to begin with. For instance grp_pow g n.+1 where n is a nat cannot be unfolded but n.+2 can. The reason is that we treat 0 differently in Int and we have to do a nat_ind starting from 1 giving us 3 cases.

I'm open to trying out the equivalence approach if @ThomatoTomato would like to have a go. I haven't thought much about it however.

[ThomatoTomato]

Okay! Thank you for making me some exercises 🥰 I will see what I will be able to do.

[ThomatoTomato]

(I need to learn how to make suggestions)

I've completed the two parts, but I've also changed a lot things along the way. I cannot tell if it is for the better or the worse.

I think Dan's idea about having a nat_iter for types with an auto-equivalence sounds nice, but can't we further generalize this to group actions? Do we have any theory of group actions atm?

[jdchristensen]

(I need to learn how to make suggestions)

What do you mean? Do you mean comments on the code? If so, then you can click on the "Files changed" tab, select some lines to comment on, and enter a comment.

I've completed the two parts, but I've also changed a lot things along the way. I cannot tell if it is for the better or the worse.

I think it all looks pretty good. And it seems like the unfolded definition of grp_pow simplified things a bit. However, if int_iter is added, I think it will produce something more like the previous definition, so you might have to undo some of your changes.

I think Dan's idea about having a nat_iter for types with an auto-equivalence sounds nice, but can't we further generalize this to group actions? Do we have any theory of group actions atm?

I don't think we have anything about group actions. But this is really something specific to the integers, since they are free on one generator, so I don't think a general theory of group actions would give as useful a tool as a specific int_iter. If you search the library, you'll find nat_iter and pos_iter, so you can model int_iter on them. But there are additional facts, like the naturality I mentioned earlier, that haven't been done for the existing iterators.

Maybe the best thing, though, is to first get this approach merged, and then start a new PR for int_iter. If you address the various comments above, then we can merge.

[ThomatoTomato]

I think I've adressed everything that has been commented on now. The change I made in Int.v probably has a shorter form, but I went with the easy solution 🥰 I managed to get rid of many of the rewrites, but I made a helper function that is very similar to grp_pow_int_add_1, called grp_pow_int_sub_1. I could prove it using the former, but then I had to use a lot of rewrites again. I think this is the cleanest way to do this, but idk.

[jdchristensen]

I think I've adressed everything that has been commented on now.

In addition to the new comments, there are still a couple of older ones that haven't been addressed. I marked the completed things as resolved. (A couple that aren't resolved are about int_iter, which we'll postpone to a future PR.)

[jdchristensen]

This LGTM. @ThomatoTomato is there anything else you want to do, or should I go ahead and merge?

[ThomatoTomato]

I'm ready to merge, so go ahead.