switch to Int in cring_Z

[Alizter]

This was a bit more work than I anticipated but I seem to have something workable. It could use some more cleanup as I think some of these proofs could be slicker.

In this PR we port the remaining uses of BinInt to Int and introduce int_iter with standard exponentiation results on equivalences and loops.

Feel free to push any commits.

@ThomatoTomato this should help you with #1992.

[ThomatoTomato]

I added a small lemma that I think can be useful in the future. This lemma also has an accompanying lemma that I do not think belong to this file, and it might already exist.

[Alizter]

@ThomatoTomato I simplified the proof of the lemma you gave.

[jdchristensen]

I think int_iter has worked well to simplify a lot of things. Thanks for tackling this, @Alizter !

The proofs about iterated powers of loops and the proof that the natural map from the integers to a ring respects addition all should be special cases about suitable functions of two variables. I started to write something down, but ran out of time. Maybe someone can figure out the right abstraction and use it in all of those places? (I started with acting on the left, but loopexp acts on the right, so one of the two should be flipped.) Here's what I had:

(** ** Iterating left-invertible binary operations. *)

Definition int_iter_op_l {A : Type} (f : A -> A -> A)
  (n : Int) (a b : A) `{IsEquiv _ _ (f a)}
  : A
  := int_iter (f a) n b.

Definition int_iter_op_l_succ_l {A : Type} (f : A -> A -> A)
  (n : Int) (a b : A) `{IsEquiv _ _ (f a)}
  : int_iter_op_l f n.+1 a b = f a (int_iter_op_l f n a b)
  := int_iter_succ_l (f a) n b.

Definition int_iter_op_l_succ_r {A : Type} (f : A -> A -> A)
  (n : Int) (a b : A) `{IsEquiv _ _ (f a)}
  : int_iter_op_l f n.+1 a b = int_iter_op_l f n a (f a b)
  := int_iter_succ_r (f a) n b.

(** When [f] is associative, this can be written a different way. *)
Definition int_iter_op_l_succ_r' {A : Type} (f : A -> A -> A)
  (n : Int) (a b : A) `{IsEquiv _ _ (f a)}
  {ass : forall x , f (f a x) b = f a (f x b)}
  : int_iter_op_l f n.+1 a b = f (int_iter_op_l f n a a) b.
Proof.
  lhs nrapply int_iter_op_l_succ_r.
  symmetry; exact (int_iter_commute_map (f a) (fun x => f x b) ass n a).
Defined.

(** When [f] is associative and [b] is a unit, we have another way. *)
Definition int_iter_op_l_succ_r'' {A : Type} (f : A -> A -> A)
  (n : Int) (a b : A) `{IsEquiv _ _ (f a)}
  {ass : forall x , f (f a x) b = f a (f x b)}
  {unit_l : forall x, f b x = x}
  {unit_r : forall x, f x b = x}
  : int_iter_op_l f n.+1 a b = f (int_iter_op_l f n a b) a.
  (* Instead of the unit laws for [b], it's probably enough to assume that [f a b = f b a]. *)
Proof.
  (* Probably have to do another induction here.  I couldn't see an abstract way to prove it. *)
Abort.

[jdchristensen]

I just pushed another commit that simplifies things by noticing that they are common instances of a general result.

I wonder how close our results on int_iter are to the Scoccola-Altenkirch induction principle? Once we have that, we can probably avoid doing induction on integers in many cases.

[Alizter]

@jdchristensen Isn't int_ter exactly the Scoccola-Altenkirch recursor? Just so that we are on the same page, we are talking about:

HIT sa_int :=
| succ : sa_int -> sa_int
| pred : sa_int -> sa_int
| succ_pred : forall x, succ (pred x) = x
| pred_succ : forall x, pred (succ x) = x
| coh ....

This is enough succ/pred an equivalence on sa_int. The recursion principle for this HIT then becomes int_iter (give or take) since we can package the data of the other constructors as an equivalence. The dependent case however becomes difficult to state.

[jdchristensen]

Now the name rng_int_mult makes sense. I generalized the results about it to not assume that the ring element is 1, except for preservation of multiplication. I also updated the comments. I removed the comment about opacity, since I didn't see anything opaque there.

[jdchristensen]

@Alizter My thoughts on these induction principles are a bit vague, but I get the sense that very similar manipulations are often being done when using our current induction principle. One idea I had would be to change the hypotheses to

  (HP : forall n : nat, P n -> P (n.+1%nat))
  (HN : forall n : nat, P (- n) -> P (-(n.+1%nat)))

instead of

  (HP : forall n : nat, P n -> P (int_succ n))
  (HN : forall n : nat, P (- n) -> P (int_pred (-n)))

(The proof is unchanged.) That might make some arguments go through more smoothly, but at least one becomes trickier, so it's not clear if this is a good idea. Maybe we should make both available?

Yes, I think int_iter is the Scoccola-Altenkirch recursor, but I was really thinking about the induction principle. Again, this is just a vague thought that might guide what we do.

[jdchristensen]

In the second-last commit, I've done some cleanups to grp_pow, ab_mul, abgroup_int_mult and rng_int_mult. Note that the last three are all special cases of grp_pow.

There are still some tasks to do.

• The grp_pow material in Group.v should be redone using int_iter. This is essentially what Ali did earlier in this PR, when defining rng_int_mult and proving properties about it. Those proofs were discarded in a recent commit, but should be brought back and used to replace the proofs of grp_pow in Group.v.

• abgroup_int_mult is just grp_pow, so I think we can just drop it.

• ab_mul is grp_pow, but regarded as a homomorphism A -> A for fixed n (needs A abelian), so this should be kept. And rng_int_mult again should be kept, since it gives a ring homomorphism.

• 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. This is optional, but the lemmas might be good tasks for @ThomatoTomato .

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. *)

[jdchristensen]

• The grp_pow material in Group.v should be redone using int_iter.

My second last commit does this. The last commit just does some cleanups to the naming and the order. So the second-last commit should be viewed on its own to better see the simplifications from using int_iter.

• abgroup_int_mult is just grp_pow, so I think we can just drop it.

I'll do this soon unless someone objects.

• 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. This is optional, but the lemmas might be good tasks for @ThomatoTomato .

If @Alizter or @ThomatoTomato plan to do this, write here first so nobody duplicates work.

[Alizter]

I'll leave it to @ThomatoTomato.

[jdchristensen]

I think we should merge this as is, and leave my suggestions about the proof of issemigrouppreserving_mult_rng_int_mult for a future PR.

[Alizter]

@jdchristensen Very well. Could you create an issue so we don't forget?