Unary integers

[Alizter]

We define the unary integers as discussed in #1913. We show that we have addition and multiplication and that these operations are associative.

This should be enough for the ring structure on Int. We can think about replacing BinInt after this PR.

The proofs here might need some cleanup, but they work.

The (initial) design is based on mathcomps integers but the proofs are only similar. These appear to be more pleasant to work with than the binary integers so far.

Edit: We now define the integer operations by integer induction, essentially 6.10.12 in the HoTT book.

[jdchristensen]

Some of the proofs are still pretty tricky with this approach. Here is how I would consider structuring these results:

• Define the successor and predecessor right away.
• State the induction principle Int_ind using them.
• Use the induction principle instead of the original definition to define addition, multiplication, etc. To define n + m, you only need to do induction on n, which means that formulas like 0 + n = n and (int_succ n) + m = int_succ (n + m) are definitionally true.
• Use the induction principle to define negation, and show that y + (- y) = 0.
• Then I think associativity follows from a short argument using induction on just the left-most variable, with no lemmas needed.
• It follows that (x + y) - y = x, so you have cancellation: if x + y = z + y, then x = z.
• Then formulas like -(x + y) = - y - x follow immediately, since they are equal when you add x + y to both sides.
  I didn't look at all of the results, e.g. commutativity, but the fact that you can get these ones fairly easily suggests to me that this approach will be much cleaner.

[Alizter]

I've only rebased and removed the unintentional changes.

[Alizter]

• Use the induction principle to define negation, and show that y + (- y) = 0.

This wasn't possible because negation is part of the induction principle. I can't just stick to nat either because I am missing the P 0 -> P (-1) step. I've therefore left negation as it was. It may be possible to define negation and integer induction mutually inductively but I didn't try since it looks complicated/convoluted and also would mean negation takes a useless universe parameter due to how universes are shared in mutual fixpoints.

• Then I think associativity follows from a short argument using induction on just the left-most variable, with no lemmas needed.

I still needed to introduce lemmas. I don't see a way to make them hold by definition due to the way we had to define induction and its interaction with negation. The basic problem is that x.+1 + y = (x + y).+1 by definition when x : nat and y : Int, but not generally for x : Int.

[Alizter]

Also I did some archaeology and here is the definition of the integers we had before I introduced the binary ones: https://github.com/Alizter/HoTT/blob/02fe3325deb76bb8b4bd5aa0079c9b32b51a7325/theories/Spaces/Int.v. This current one appears to be a slight improvement on that by reducing the number of constructors from 3 to 2.

[jdchristensen]

Ok, I see that my proposed plan was too optimistic. I was thinking of a slightly incorrect induction principle. Your latest commit actually added slightly more lines than it removed, so it's not clear if it is better this way. But what I realized is that the Int_ind induction principle is exactly the induction principle for the old version of the integers that you linked to in the previous comment. So if we went back to that definition, then Int_ind would be there for free, and would compute definitionally. That old version is also more symmetrical, which should make things cleaner. It's true that it has three constructors instead of two, but so does Int_ind, which is what seems to be used most of the time. (And even in cases where the two constructor induction principle is used, like in int_succ and int_pred, one case is treated separately, still giving three cases.)

There's also the approach of The Integers as a Higher Inductive Type, Thorsten Altenkirch, Luis Scoccola, https://arxiv.org/abs/2007.00167, Definition 1.3. They show that to prove a family of propositions (such as identities between integers) with their definition, you just need to prove them for 0, successors, and predecessors, so I think it would end up working out more like i described in my plan. It would be a big change from what is in this PR, but it could have some advantages.

What do you think about either using the old definition with three constructors or the Altenkirch-Scoccola definition? In the latter case, there's an implementation in cubical Agda that could be roughly followed.

[Alizter]

Ok, I see that my proposed plan was too optimistic. I was thinking of a slightly incorrect induction principle. Your latest commit actually added slightly more lines than it removed, so it's not clear if it is better this way.

This is somewhat subjective, as I could be far more compact with the rewrites. The previous attempt had far more complex proofs since I had to reason about inequalities often.

But what I realized is that the Int_ind induction principle is exactly the induction principle for the old version of the integers that you linked to in the previous comment. So if we went back to that definition, then Int_ind would be there for free, and would compute definitionally. That old version is also more symmetrical, which should make things cleaner.

That's a good point. I'll try and see if it works out.

There's also the approach of The Integers as a Higher Inductive Type, Thorsten Altenkirch, Luis Scoccola, arxiv.org/abs/2007.00167, Definition 1.3. They show that to prove a family of propositions (such as identities between integers) with their definition, you just need to prove them for 0, successors, and predecessors, so I think it would end up working out more like i described in my plan. It would be a big change from what is in this PR, but it could have some advantages.

I've also thought about this before, however I am a little worried that introducing a HIT for the integers might be a little heavy. We could also define the integers the usual classical way with a pair of natural numbers. (IIRC this comes from medieval Italian accountants tacking credit and debit). I'm not sure how well these compute intentionally. We actually already have these with natpair_int in the mathclasses library.

What do you think about either using the old definition with three constructors or the Altenkirch-Scoccola definition? In the latter case, there's an implementation in cubical Agda that could be roughly followed.

I think switching to the AS definition of the integers would be too radical at this point. It's not entirely clear to me if it will work out in a practical way. The main aim of this PR was to get the integers into a workable and practical state so that we can start to develop some more algebra on top of them. I'm of course open to some experimentation with the AS definition, but I wouldn't recommend we make it the main definition.

I will therefore experiment with the 3 constructor integers, bringing us full-circle, which is ironic since we are talking about integers. However this time at least we have a lot more experience and lemmas about them.

[jdchristensen]

This is somewhat subjective, as I could be far more compact with the rewrites. The previous attempt had far more complex proofs since I had to reason about inequalities often.

It sounds like you think the current approach is better which is great. Length is of course not the most important factor, but I didn't do a careful comparison, which is why I mentioned the length. If you think it was cleaner, then I agree with continuing this way. And switching to the three-constructor version of the integers will trim a bit of the code, probably making the length comparable or even shorter than the previous version.

[Alizter]

I had a go at:

Inductive Int : Type0 :=
| negS : nat -> Int
| zero :Int
| posS : nat -> Int
.

however it quickly becomes apparent that this definition is inferior. I'll list all the problems here:

• Converting from a nat to an Int has to be done by cases:

Definition int_of_nat (n : nat) :=
  match n with
  | O => zero
  | S n => posS n
  end.

• int_succ and int_pred end up having more cases:

Definition int_succ (n : Int) : Int :=
  match n with
  | posS n => posS (S n)
  | 0 => 1
  | -1 => 0
  | negS (S n) => negS n
  end.

Definition int_pred (n : Int) : Int :=
  match n with
  | posS (S n) => posS n
  | 1 => 0 
  | 0 => -1
  | negS n => negS (S n)
  end.

• Int_ind ends up having 5 cases rather than 4:

Definition Int_ind@{i} (P : Int -> Type@{i})
  (H0 : P 0)
  (HP : forall n : nat, P n -> P (int_succ n))
  (HN : forall n : nat, P (- n) -> P (int_pred (-n)))
  : forall x, P x.
Proof.
  intros[x | | x].
  - induction x as [|x IHx] using Core.nat_ind.
    + apply (HN 0%nat), H0.
    + apply (HN x.+1%nat), IHx.
  - exact H0.
  - induction x as [|x IHx] using Core.nat_ind.
    * apply (HP 0%nat), H0.
    * apply (HP x.+1%nat), IHx.
Defined.

This means I often have to split induction into 5 cases rather than 3 (maybe 4) from before

For example:

(** Integer addition with zero on the right is the identity. *)
Definition int_add_0_r@{} (x : Int) : x + 0 = x.
Proof.
  induction x as [|[|x] IHx|[|x] IHx].
  - reflexivity.
  - reflexivity.
  - change ((x.+1%nat + 0).+1 = x.+1%nat.+1).
    by rewrite IHx.
  - reflexivity.
  - change (?x.-1 + ?y) with (x + y).-1.
    by rewrite IHx.
Defined. 

Therefore it looks like the current approach is the best.

[mikeshulman]

When I did some formalization work on the integers in a different proof assistant, I felt that the conceptual clarity of the three-constructor version outweighed the disadvantages of a few more cases. With the two-constructor version I kept being confused about whether or not to add or subtract one from my natural numbers to get the definitions correct. Not saying you have to do it that way, just contributing my experience.

[jdchristensen]

I'm not completely convinced by those examples. While there are more cases, they look pretty trivial and follow an easy to see pattern. And I would guess that there are situations where things simplified as well. I guess I'd be more convinced by a more difficult thing blowing up with one approach vs the other.

I also wonder if there's an induction principle that will reduce the number of cases when you are proving a proposition. E.g. having hypotheses P 0, forall z : Int, P z -> P (int_succ z) and forall z : Int, P z -> P (int_pred z). But this would probably only be helpful if addition could be defined in a similar way, which gets us to the Altenkirch-Scoccola approach. I think I now see why their approach reduces the number of cases to consider. Can we mimick their approach by showing that our Int satisfies a similar induction principle?

(That all said, I think it's fine however you choose to do this.)

[mikeshulman]

Also a side note, in case anyone is interested or has suggestions. One of the features I've considered for Narya is "nominal subtyping that requires structural compatibility". Specifically, that means that if A and B are inductive types, and for every constructor of A, B has a constructor of the same name, and the inputs of the constructor of A are subtypes of those of the constructor of B (assuming recursively that A is a subtype of B), then we can declare A to be a subtype of B. This is like an implicit coercion except that no actual coercion function needs to be inserted even internally, since a term of type A can literally be used like a term of type B in computations. With this sort of subtyping, if we define Nat and Int by

def Nat : Type := data [
| zero.
| suc. (_ : Nat)
]

def Int : Type := data [
| zero.
| suc. (_ : Nat)
| negsuc. (_ : Nat)
]

then we can declare Nat to be a subtype of Int. In other words, int_of_nat can be the identity function, because it just renames constructors, but now the constructors of Nat are also themselves constructors of Int and no renaming is necessary.

Of course, this doesn't reduce the number of cases for defining operations on Int, nor is it relevant at all to Coq. But I think it's an interesting argument for the three-constructor version in a language with this sort of subtyping. You could also make it work with the Altenkirch-Scoccola definition.

[jdchristensen]

@Alizter That last commit looks pretty good to me. It's a small diff, and it did in fact reduce the number of lines of code, while also simplifying a few things.

[jdchristensen]

Let me know if you think this is ready for another review.

[Alizter]

I want to do another pass over trying to simplify a few proofs and there are things that need some comments.

[Alizter]

@jdchristensen I've added some more comments. It was a bit tricky putting lemmas like int_mul_succ_l into prose, but I think I managed it. This is ready as far as I am concerned.

[jdchristensen]

I made two comments, and I'm about to push a few minor clean-ups.

[jdchristensen]

Just before this point, we have proved everything that shows that Int is an abelian group. So int_neg_add follows from general facts about abelian groups (e.g. negate_sg_op and Int_add_comm). Is there a way to restructure to do it this way? (It can also be locally proved without induction on x, using algebraic rules we also have.) But it's also fine this way.

[Alizter]

I don't see a way to do this without having to pull in mathclasses which I would prefer not to do at this point. I would like to keep the group theory restricted to Z.v so that this file can be used without pulling in too much.

[jdchristensen]

That makes sense. So this PR LGTM.