grp_pow and related things

[jdchristensen]

Based on a comment I made in in #2000 (comment)_

I think issemigrouppreserving_mult_rng_int_mult can be proven by combining some pieces that will be useful on their own. See below for a sketch.

Group.v:

(** [grp_pow g n] commutes with [g].  Actually, for the inductive step below, we might need to know that if [g] commutes with [h], then [g] commutes with powers of [h]? *)
Definition grp_pow_commutes {G : Group} (n : Int) (g : G)
  : (grp_pow g n) * g = g * (grp_pow g n).

(** If [g] and [h] commute, then [grp_pow (g * h) n] = (grp_pow g n) * (grp_pow h n)]. *)
(* Note that part of the proof that [ab_mul] is a homomorphism will be covered by this. *)
Definition grp_pow_mul {G : Group} (n : Int) (g h : G)
  (c : g * h = h * g)
  : grp_pow (g * h) n] = (grp_pow g n) * (grp_pow h n).

(** [grp_pow] satisfies a multiplicative law of exponents. *)
Definition grp_pow_int_mul {G : Group} (m n : Int) (g : G)
  : grp_pow g (m * n)%int = grp_pow (grp_pow g m) n.
(* This will follow from the previous two. *)

Rings/Z.v:

Definition rng_int_mult_foo {R : Ring} (r : R) (n : Int)
  : rng_int_mult r n = (rng_int_mult 1 n) * r.

(* I think issemigrouppreserving_mult_rng_int_mult will follow from the previous item and grp_pow_int_mul. *)

cc: @ThomatoTomato

[ndcroos]

For Group.v I have this at the moment:

(** [grp_pow g n] commutes with [g].*)
Definition grp_pow_commutes'' {G : Group} (n : Int) (g : G)
  : (grp_pow g n) * g = g * (grp_pow g n).
Proof.
  symmetry.
  by apply grp_pow_commutes.
Defined.

(** If [g] and [h] commute, then [grp_pow (g * h) n] = (grp_pow g n) * (grp_pow h n)]. *)
Definition grp_pow_mul {G : Group} (n : Int) (g h : G)
  (c : g * h = h * g)
  : grp_pow (g * h) n = (grp_pow g n) * (grp_pow h n).
Proof.
  induction n.
  - simpl.
    rhs nrapply grp_unit_r; reflexivity.
  - rewrite 3 grp_pow_succ.
    rewrite IHn.
    repeat rewrite grp_assoc.
    apply grp_cancelR.
    repeat rewrite <- grp_assoc.
    apply grp_cancelL.
    apply grp_pow_commutes.
    symmetry.
    apply c; reflexivity.
  - simpl.
    rewrite 3 grp_pow_pred.
    rewrite IHn.
    repeat rewrite grp_assoc.
    apply grp_cancelR.
Defined.

The goal looks like this:

1 goal
G : Group
n : nat
g, h : G
c : g * h = h * g
IHn : grp_pow (g * h) (- n)%int =
      grp_pow g (- n)%int * grp_pow h (- n)%int
______________________________________(1/1)
- (g * h) * grp_pow g (- n)%int =
- g * grp_pow g (- n)%int * - h

@Alizter can you have a hint for this please?

For Ring/Z.v:

Definition rng_int_mult_foo {R : Ring} (r : R) (n : Int)
  : rng_int_mult r n = (rng_int_mult 1 n) * r.
Proof.
Defined.

I get the error:

In environment
R : Ring
r : R
n : Int
The term "r" has type "group_type R"
while it is expected to have type "Ring".

[Alizter]

@ndcroos I haven't been able to check the first, but for the second you will need to replace Int with cring_Z or else Coq doesn't pick up the ring structure.

[jdchristensen]

A few comments.

Definition grp_pow_commutes'' {G : Group} (n : Int) (g : G)
  : (grp_pow g n) * g = g * (grp_pow g n).

This isn't needed. You can just use grp_power_commutes', with symmetry before if needed.

    rhs nrapply grp_unit_r; reflexivity.

This produces the term (1 @ (grp_unit_r mon_unit)^, but the 1 @ part is redundant. Instead use symmetry; nrapply grp_unit_r. since grp_unit_r solves that goal. Only use lhs and rhs when the lemma you want to apply only gets you part way.

    apply c; reflexivity.

apply c doesn't produce any subgoals, so there is no need for ; reflexivity. And I would phrase it as exact c. to emphasize that it exactly solves the goal.

So here is how I would write the first part of your proof:

Definition grp_pow_mul {G : Group} (n : Int) (g h : G)
  (c : g * h = h * g)
  : grp_pow (g * h) n = (grp_pow g n) * (grp_pow h n).
Proof.
  induction n.
  - simpl.
    symmetry; nrapply grp_unit_r.
  - rewrite 3 grp_pow_succ.
    rewrite IHn.
    rewrite 2 grp_assoc.
    apply grp_cancelR.
    rewrite <- 2 grp_assoc.
    apply grp_cancelL.
    apply grp_pow_commutes.
    exact c^.
  - simpl.
    rewrite 3 grp_pow_pred.
    rewrite IHn.
    rewrite 2 grp_assoc.
    apply grp_cancelR.

As for the hint, you'll want to first commute g * h to h * g and then use that the inverse of a product is the product of the inverses in the other order, which is grp_inv_op.

[ndcroos]

At the moment I have this proof, where all the goals are completed.

(** If [g] and [h] commute, then [grp_pow (g * h) n] = (grp_pow g n) * (grp_pow h n)]. *)
Definition grp_pow_mul {G : Group} (n : Int) (g h : G)
  (c : g * h = h * g)
  : grp_pow (g * h) n = (grp_pow g n) * (grp_pow h n).
Proof.
  induction n.
  - simpl.
    symmetry; nrapply grp_unit_r.
  - rewrite 3 grp_pow_succ.
    rewrite IHn.
    rewrite 2 grp_assoc.
    apply grp_cancelR.
    rewrite <- 2 grp_assoc.
    apply grp_cancelL.
    apply grp_pow_commutes.
    exact c^.
  - simpl.
    rewrite 3 grp_pow_pred.
    rewrite IHn.
    rewrite 2 grp_assoc.
    apply grp_cancelR.
    rewrite c.
    rewrite grp_inv_op.
    rewrite 2 grp_pow_commutes.
    1: rewrite grp_assoc; reflexivity.
    1: rewrite grp_commutes_inv; reflexivity.
    rewrite <- grp_inv_op.
    rewrite grp_commutes_inv.
    1: reflexivity.
    rewrite <- c.
    rewrite c.
    rewrite grp_commutes_op.
    1: reflexivity.
    1: exact c.
    reflexivity.
Defined.

grp_pow_int_mul is still incomplete. I did not use grp_pow_mul or grp_pow_commutes yet. The proofs for the positive and negative case of n are similar here, using int_mul_succ_r and int_mul_pred_r. It works for the positive case, but not (yet) for the negative case.

(** [grp_pow] satisfies a multiplicative law of exponents. *)
Definition grp_pow_int_mul {G : Group} (m n : Int) (g : G)
  : grp_pow g (m * n)%int = grp_pow (grp_pow g m) n.
(* This will follow from the previous two. *)
Proof.
  induction n.
  - simpl.
    rewrite int_mul_0_r.
    simpl; reflexivity.
  - simpl.
    rewrite int_mul_succ_r.
    rewrite grp_pow_add.
    rewrite grp_pow_succ.
    apply grp_cancelL.
    exact IHn.
  - simpl.
    rewrite int_mul_pred_r.
    rewrite grp_pow_add.
    rewrite grp_pow_pred.
    rewrite grp_pow_neg.
    rewrite IHn.
    apply grp_cancelR.
    rewrite <- grp_pow_neg.

Defined.

The remaining goal is here:

1 goal
G : Group
m : Int
n : nat
g : G
IHn : grp_pow g (m * - n)%int =
      grp_pow (grp_pow g m) (- n)%int
______________________________________(1/1)
grp_pow g (- m)%int = - grp_pow g m

At this point, I tried several things: again looking at grp_pow_mul and grp_pow_commutes, unfolding grp_pow, looking at grp_homo_inv and grp_pow_natural.

(Group element inversion is a group homomorphism if and only if the underlying group G is abelian, so using grp_pow_natural would not work here.)
The group n'th power operation f is a group homomorphism:

• identity is mapped to identity
• f(g*h) = (g*h)^n = g^n * h^n for all g, h in G. Note that this is grp_pow_mul, and grp_pow_mul assumes that that g and h are commutative.

So I think maybe grp_homo_inv could be used here. grp_pow is not yet defined as a group homomorphism.

Since I did not use grp_pow_mul or grp_pow_commutes (yet), maybe there is another approach to proving this. Could I get a hint for how to continue?

[jdchristensen]

The last goal of grp_pow_mul has a slightly shorter proof:

  - simpl.
    rewrite 3 grp_pow_pred.
    rewrite IHn.
    rewrite 2 grp_assoc.
    apply grp_cancelR.
    rewrite c.
    rewrite grp_inv_op.
    rewrite <- 2 grp_assoc.
    apply grp_cancelL.
    apply grp_pow_commutes.
    symmetry; apply grp_commutes_inv, c.

About grp_pow_int_mul: The goal you have is one that we'd like to know anyways as a separate lemma. To show that foo = -bar, it's enough to show that foo * bar = mon_unit, and that follows in this case from grp_pow_add.

Alternatively, the proof I had in mind uses induction on m instead of n. Then it requires grp_pow_mul and grp_pow_commutes, but doesn't require the goal you are left with. Either way is fine, since we'd like to know that fact about inverses anyways.

Sorry to be slow to respond. I'm travelling until Sept 1, and will be pretty busy in the fall.

[ndcroos]

Thanks, the proofs for group.v are now complete.

For Z.v I have still the same error.

Definition rng_int_mult_foo {R : Ring} (r : R) (n : cring_Z)
  : rng_int_mult r n = (rng_int_mult 1 n) * r.
Proof.
Defined.

In environment
R : Ring
r : R
n : cring_Z
The term "r" has type "group_type R" while it is expected to have type
 "Ring".

[Alizter]

@ndcroos The arguments of rng_int_mult are perhaps not what you expected. If you have a look, the ring that it takes is explicit meaning you should pass rng_int_mul R r n instead. The reason this is done is so that the next lemma after the definition can be stated nicely, but perhaps this reason is not good enough. You can make R explicit in rng_int_mult and replace rng_int_mult in issemigrouppreserving_mult_rng_int_mult with @rng_int_mult (which makes all the args explicit).

[ndcroos]

Is it meant that the proof for issemigrouppreserving_mult_rng_int_mult that is already in Z.v should be replaced by a proof using grp_pow_int_mul and rng_int_mult_foo?

[jdchristensen]

Is it meant that the proof for issemigrouppreserving_mult_rng_int_mult that is already in Z.v should be replaced by a proof using grp_pow_int_mul and rng_int_mult_foo?

Yes, that is what I was proposing. I haven't checked all of the details, though. (BTW, foo is just a placeholder for choosing an appropriate name.)