Make pos and int unary

[Alizter]

I think it's time to make Pos and Int into the unary versions. By that I mean removing Pos completely and redefining Int as:

Inductive Int :=
| pos : nat -> Int
| negS : nat -> Int
.

This will remove a lot of the friction we have when working with the integers. To see how bad things are today, have a look at https://github.com/HoTT/Coq-HoTT/blob/master/theories/Algebra/Rings/Z.v

A lot of the problems actually come from Pos where the choice as a binary definition hasn't really been a good one. I think for proofs the unary definition is always better. If in the unlikely circumstance we end up needing to compute something big with unary nats and we want something more efficient, we can always convert across equivalences to an efficient one. (This scenario has yet to be conceived).

[Alizter]

Of course one disadvantage is that 123456 causes a stack overflow. I don't know if we have numbers this large that occur naturally and whether we need to unfold them.

[Alizter]

Here is a start with the number notations set up correctly:

Require Import Basics.Overture Basics.Nat.
Require Basics.Decimal.

Declare Scope int_scope.

Inductive Int : Type0 :=
| pos : nat -> Int
| negS : nat -> Int
.

Definition int_to_decimal_int (n : Int) : Decimal.int :=
  match n with
  | pos n => Decimal.Pos (Nat.to_uint n)
  | negS n => Decimal.Neg (Nat.to_uint (S n))
  end.

Definition int_to_number_int (n : Int) : Numeral.int :=
  Numeral.IntDec (int_to_decimal_int n).

Fixpoint int_of_decimal_uint (d : Decimal.uint) : Int :=
  match d with
  | Decimal.Nil => pos 0
  | Decimal.D0 d => int_of_decimal_uint d
  | Decimal.D1 d => pos (Nat.of_uint_acc d 1)
  | Decimal.D2 d => pos (Nat.of_uint_acc d 2)
  | Decimal.D3 d => pos (Nat.of_uint_acc d 3)
  | Decimal.D4 d => pos (Nat.of_uint_acc d 4)
  | Decimal.D5 d => pos (Nat.of_uint_acc d 5)
  | Decimal.D6 d => pos (Nat.of_uint_acc d 6)
  | Decimal.D7 d => pos (Nat.of_uint_acc d 7)
  | Decimal.D8 d => pos (Nat.of_uint_acc d 8)
  | Decimal.D9 d => pos (Nat.of_uint_acc d 9)
  end.

Definition int_of_decimal_int (d : Decimal.int) : Int :=
  match d with
  | Decimal.Pos d => int_of_decimal_uint d
  | Decimal.Neg u =>
      match int_of_decimal_uint u with
        | pos (S v) => negS v
        | _ => pos 0
      end
  end.

Definition int_of_number_int (d:Numeral.int) :=
  match d with
  | Numeral.IntDec d => Some (int_of_decimal_int d)
  | Numeral.IntHex _ => None
  end.

Number Notation Int int_of_number_int int_to_number_int : int_scope. 

Local Close Scope int_scope.
Delimit Scope int_scope with int.

Eval cbn in (-33 = 58)%int.

[mikeshulman]

Couldn't we keep the binary definition as "the" definition, but prove once that it's isomorphic to the unary one, and then transport all the proofs across that equivalence using univalence? The proofs wouldn't compute, but since the integers are a set it seems unlikely that we would need them to.

[Alizter]

That seems like a good idea at first, but it quickly runs into issues. Suppose we are proving that integer addition commutes. If we transport that statement from the binary to the unary one, suddenly we need to know that transporting our addition is the addition in the binary one. That is not a simple lemma to prove. Once you add in more and more things you can do with integers, you can quickly see how transporting is not as easy as it looks.

Also I should add that there are some "aesthetic" considerations. It seems somewhat ridiculous to me that proofs of arithmetic facts would require univalence.

[mikeshulman]

That's why I said "isomorphic" rather than "equivalent" -- we need to know the equivalence respects the operations. But only the operations: we don't need to know anything about the operations on binary integers except what's necessary to prove the isomorphism. I haven't tried, so maybe you're right that this isomorphism is nontrivial. But it does seem to me that there should be a limited number of operations on the integers and everything else should be definable in terms of those. What do you need beyond the ring structure?

[mikeshulman]

But it's true that in this library, where we are explicitly tracking uses of univalence with a typeclass, that it would be ugly and annoying to have facts about the integers depend on it. (Although in principle, I tend to view univalence as a fundamental aspect of mathematics and not something one should object to depending on.)

[mikeshulman]

It does seem like there ought to be a way to define the integers that isn't asymptotically inefficient but is also practical for proofs. A couple of years ago I started a conversation on the HoTT mailing list about an "infinite two's complement" or "eventually-constant 2-adic" representation of binary integers that wouldn't need an explicit "sign bit". I started with a HIT version but eventually realized there is a version without HITs.

The definition is Z = Unit + Bwd(2), where Bwd denotes backwards lists that cons (or "snoc") on the right. Here the point of Unit represents zero (2-adically ...0000), the empty list represents -1 (2-adically ...1111), and a nonempty list represents a 2-adic integer with an implicit tail left that is the opposite of its leftmost explicit digit (thus 1101 represents ...0001101 = 13 while 0110 represents ...1110110 = -10). Then doubling is "snoc(-,0)" on lists and fixes the point of Unit; while doubling-plus-one is "snoc(-,1)" on nonempty lists, fixes the empty list, and sends the point of Unit to the singleton list "1". Addition is simple binary addition with carrying, munged at the end appropriately, and multiplication should be definable in terms of doubling and doubling-plus-one. There are still some case splits necessary, of course, but they seem mainly to involve dealing explicitly with small numbers like 0 and -1, so I would hope they wouldn't be too bad.

[Alizter]

That's why I said "isomorphic" rather than "equivalent" -- we need to know the equivalence respects the operations. But only the operations: we don't need to know anything about the operations on binary integers except what's necessary to prove the isomorphism. I haven't tried, so maybe you're right that this isomorphism is nontrivial. But it does seem to me that there should be a limited number of operations on the integers and everything else should be definable in terms of those. What do you need beyond the ring structure?

Actually I think maybe we have this backwards. I would say that defining them as unary and proving facts about them should be first-class. It should then be the job of the person wanting to actually compute things to translate that via an isomorphism to a statement about binary ints. Similar to how we can quote/unquote things in effective algebra.

But it's true that in this library, where we are explicitly tracking uses of univalence with a typeclass, that it would be ugly and annoying to have facts about the integers depend on it. (Although in principle, I tend to view univalence as a fundamental aspect of mathematics and not something one should object to depending on.)

In the grand scheme of things, yes, univalence is fundamental. However I don't think that is an excuse to use it everywhere. An apple-to-oranges comparison might be something like AC or specifically Zorn's lemma. Older literature on ring theory used Zorn's lemma at every turn, which made some proofs quick but quickly leads to problems when trying to give explicit descriptions of ideals. In many cases it can be avoided. I think so far we've done something similar for univalence. I am not aware anybody in HoTT is interested in HoTT-like models without univalence, so I would assume that our main driver is that it is an axiom.

Cubical agda has univalence "built-in" which is why they've (cubical agda and 1lab) been able to use it all over the place. The fact that we have to explicitly ask for univalence is annoying but perhaps not our biggest gripe. The largest issue is that of "blocking computation". You can use all sorts of transports over univalence when proving things, but as soon as you need to reason about that proof, you find yourself in the role of the computer. This is again one of the reasons HITs are not used at every turn.

Of course, this kinds of things can be fixed with richer type theories, and there as you know the main blocker is the lack of understanding for the general models.

It does seem like there ought to be a way to define the integers that isn't asymptotically inefficient but is also practical for proofs. A couple of years ago I started a conversation on the HoTT mailing list about an "infinite two's complement" or "eventually-constant 2-adic" representation of binary integers that wouldn't need an explicit "sign bit". I started with a HIT version but eventually realized there is a version without HITs.

The definition is Z = Unit + Bwd(2), where Bwd denotes backwards lists that cons (or "snoc") on the right. Here the point of Unit represents zero (2-adically ...0000), the empty list represents -1 (2-adically ...1111), and a nonempty list represents a 2-adic integer with an implicit tail left that is the opposite of its leftmost explicit digit (thus 1101 represents ...0001101 = 13 while 0110 represents ...1110110 = -10). Then doubling is "snoc(-,0)" on lists and fixes the point of Unit; while doubling-plus-one is "snoc(-,1)" on nonempty lists, fixes the empty list, and sends the point of Unit to the singleton list "1". Addition is simple binary addition with carrying, munged at the end appropriately, and multiplication should be definable in terms of doubling and doubling-plus-one. There are still some case splits necessary, of course, but they seem mainly to involve dealing explicitly with small numbers like 0 and -1, so I would hope they wouldn't be too bad.

That's an interesting suggestion that I haven't seen before. I'm sure it would work out but I think it runs into the same issues as our current binary implementation. When working in proofs you want to have a definitionally computing slick induction principle. As soon as case analysis goes above 2 cases for each number, the number of cases you have to consider blows up making proofs difficult. It also doesn't help that it's hard to reuse lemmas about nat and arithmetic in nat in this case.

I should maybe point out that the "computation issues" that I hinted at above are not coming from Coq's kernel but rather from the printing mechanism. In practice you can reason about much large unary numbers as long as you aren't forced to print the term.

[JasonGross]

When working in proofs you want to have a definitionally computing slick induction principle. As soon as case analysis goes above 2 cases for each number, the number of cases you have to consider blows up making proofs difficult.

Possible alternative viewpoint: the computational behavior of the induction principle for int should never be relied on judgmentally. Furthermore, the recursor should only show up directly when defining operations or characterizing them, and otherwise proofs should go through characterizing equations of the basic operations.
(How painful would it be to mark all direct definitions on int as simpl never and have an autorewrite db for the simplifying equations?)

[JasonGross]

(And transports across proofs about int should not hurt us, except maybe performance-wise; we can have a tactic that automatically generalizes over equations being transported across in hSets and another that eliminates hProp equalities in the context)

[JasonGross]

What do you need beyond the ring structure?

I think the general theory also wants sign / abs, and log2 / nbits (for, e.g., recursion fuel in Euclidian division). I guess we can derive the order structure (in terms of sign / abs), div & mod, and bitwise operations.

[Alizter]

Possible alternative viewpoint: the computational behavior of the induction principle for int should never be relied on judgmentally. Furthermore, the recursor should only show up directly when defining operations or characterizing them, and otherwise proofs should go through characterizing equations of the basic operations. (How painful would it be to mark all direct definitions on int as simpl never and have an autorewrite db for the simplifying equations?)

The issue with rewrites is that they make the proof terms much larger. There are ways around this using Setoid rewrite however this is difficult and time consuming to setup correctly, and has various issues last I checked, mostly to do with universe polymorphism. Presumably this would be fine if for proofs of equality that can even be opaque, however in HoTT we have various situations where we need to reason about arithmetic for a transparent proof term that needs to be used in a computational way. An example of this is the theory of graded abelian groups where we need to rewrite the indexing of the grading according to some arithemtic laws so having huge proof terms around can be painful and opaque terms are out of the question.

I think the general theory also wants sign / abs, and log2 / nbits (for, e.g., recursion fuel in Euclidian division). I guess we can derive the order structure (in terms of sign / abs), div & mod, and bitwise operations.

In practice for us, Mike might be correct. We rarely have to do much more than ring manipulations in our proofs as we aren't typically interested in these operations. Perhaps div and mod would fall into this category if we ever need to develop a theory of PIDs or UFDs.

[mikeshulman]

Yes, Jason said what I had in mind. Does it really cause problems in graded abelian groups if the proofs of arithmetic properties are opaque? Those equalities all belong to propositions, so they are all propositionally unique anyway, and e.g. if we end up comparing transports of some proof-relevant object across two opaque equalities they must be typally equal anyway.