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]

One pattern I noticed is that int_iter is defined directly from the definition of Int, and this doesn't mesh well with the custom induction principle we defined. That's why destruct n works quite well when the goal doesn't need an induction hypothesis. I wonder if we should also have the default induction principle available, and if it would help with some of these goals? Or if we should rephrase the custom induction principle so we don't need things like int_pred_succ so often?

[Alizter]

I'm not sure what you mean by default induction principle here. The only eliminator we have for Int is one by cases and it is non-recursive. This is essentially because we just have two copies of nat stuck together around a base point as a sum type.

Even when we destruct by cases we still have to case split on n in (negS n).+1 being 0 or .+1 given how we define successor. So it doesn't appear to gain us anything as we run into the same problems. I am however unsure if a Scoccola-Altenkirch induction prinicple would work, however it seems pretty complicated to write down. I guess in the hset case it would be simplified.

[jdchristensen]

(I should have put my top-level comment here. The idea is that maybe by using natural number successor instead of int_succ, we might not have to destruct n in as many places.)

[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?