Work on issue #2015: grp_pow and related things

[ndcroos]

Fixes #2015

[jdchristensen]

Suggested change

(* This will follow from the previous two. *)

[jdchristensen]

Suggested change

	: IsSemiGroupPreserving (A:=cring_Z) (Aop:=(.*.)) (Bop:=(.*.)) (@rng_int_mult R 1).
	: IsSemiGroupPreserving (A:=cring_Z) (Aop:=(.*.)) (Bop:=(.*.)) (rng_int_mult R 1).

[ndcroos]

I forgot this change in this commit. I will do this tomorrow.

[jdchristensen]

It's probably also worth stating a third variant of grp_pow_neg, namely that grp_pow (- g) n = - grp_pow g n. This can be proved by combining grp_pow_neg and grp_pow_neg_inv, or maybe it's just as easy to prove it directlly.

Then ab_mul will follow from grp_pow_unit, grp_pow_mul and this new result, so ab_mul_helper won't be needed.

[Alizter]

The indentation here seems off. Everything after a - should be two spaces indented so that you can easily see the parts of the proof.

- foo.
  bar.
- foo.
  bar.

[Alizter]

Suggested change

[Alizter]

easy is a bit weird, I would prefer if you instead used by or better yet, just explicitly use a tactic.

[ndcroos]

I haven't found a proof for issemigrouppreserving_mult_rng_int_mult that uses the suggested results (#2015 (comment)). (I did some attempts.)
I have a proof that for ab_mul that uses grp_pow_neg_inv' (another variant), but it does't usage of that result isn't crucially in the proof.
I also have an issue with grp_pow_neg_inv' that isn't found in the environment of AbelianGroup.v

[jdchristensen]

@ndcroos There are a few problems with this PR:

• The "Apply suggested changes" commit does more than just suggested changes, and the library doesn't build after that commit. You shouldn't push something that doesn't build unless you specifically are stuck on something and want help. You also shouldn't mix suggested changes with other work.
• rng_int_mult_dist was simultaneously moved and changed, which means we can't see the changes in the diff. And the changes seem to make the proof harder to follow. I would move it back to where it was and undo the changes to the proof.
• I think you should go back to before that commit, and make changes again, one at a time, checking that the library builds after each one. When you find the change that causes problems with universe variables, we can help fix it. But as it is now, too much is changed to make that easy to do.
• The proof of ab_mul was replaced with a longer proof, so this is a step backwards. We'll need to discuss, but for now, I would revert to the previous proof.
• The comment describing ab_mul was deleted and should be reinstated.

After things are in a good state again, it'll be easier to work on issemigrouppreserving_mult_rng_int_mult.

[ndcroos]

Thanks for the feedback. Could I get some hints for issemigrouppreserving_mult_rng_int_mult and ab_mul?

[jdchristensen]

The proof of issemigrouppreserving_mult_rng_int_mult is just the composite of the distributivity result and the power result. With the distributive law that I stated, you'd also need to use the commutativity of multiplication in Z, but if you also prove the reverse distributivity, it's just the composite of the two results. Since it's only two lines, I pushed it. And I gave a short proof of the distributivity laws. I'm out of time now, but will think about ab_mul later.

[jdchristensen]

And ab_mul is just a special case of grp_pow_mul. So I pushed that.

[jdchristensen]

I tightened up a few proofs and think this is ready to merge. @Alizter , do you want to give it a quick check?

Before merging, I think we should squash most of the commits, since there was a lot of churn and some intermediate commits don't build. I'll do this after both @Alizter and @ndcroos respond (so @ndcroos can see the last few commits I made).

[jdchristensen]

@ndcroos A few general comments about how this ended up working out:

• About ab_mul being a homomorphism, this is the statement that n (a + b) = n a + n b. In multiplicative notation, n a is a^n, so this goal translates to (a * b)^n = a^n * b^n, which is grp_pow_mul.
• In general, instead of proving things about a specific situation (e.g. rng_int_mult or ab_mul) we tried to find a more basic result about grp_pow or int_iter that covered it.
• We tried to avoid induction over n if we could instead apply a general principle, such as commuting with a group homomorphism.

[Alizter]

Looks good to me.

[ndcroos]

Looks also good to me.

[jdchristensen]

Thanks, @ndcroos!