Add Countable instances for byte

Thanks for the MR and sorry for the delayed response.

Two questions/remarks:

• Not sure if the strings file is the right place for this.
• What's the purpose of byte anyway?

bytes are an efficient representation of an 8-bit number. They're mainly used as part of the new String Notation feature, which allows customizing string literals to be parsed using an arbitrary Gallina function of type list Byte.byte -> option T and printed with an inverse function.

If you want compact bytes they're also good (and you probably don't want to write your own inductive with 256 constructors).

Originally I had them in a separate file but that seemed excessive, and they're sort of related to Coq strings (which are basically byte arrays).

Shouldn't we switch to strings based on byte in the proof mode? Since the terms of Ascii based strings are enormous, this would be much better.

Sure, that would certainly be cool!

Does such a string type readily exist in the Coq stdlib, or should we define a byte-based string type ourselves?

I don't see the construction in the standard library, but it's just a few lines of code:

From Coq Require Import Init.Byte.
Record bytes := bytes_from_list { bytes_to_list : list byte }.

Declare Scope bytestring_scope.
Open Scope bytestring_scope.
String Notation bytes bytes_from_list bytes_to_list : bytestring_scope.

Definition foo : bytes := "foo".

added 14 commits

• 535b3d81...befe38d4 - 13 commits from branch iris:master
• 5346dd70 - Add Countable instances for byte

Compare with previous version

Let's continue that discussion at iris#317

I think this MR can be merged. Thanks :)

mentioned in commit a2ac9e66

merged

This MR fails with Coq <= 8.9, so it seems like we need to revert this.

Oh of course, I didn't think about that; please do.

mentioned in commit e99804d9

mentioned in merge request !160 (merged)

So should we reopen the MR then to track re-landing this?

The latest released std++ and Iris already support Coq 8.9. So at least on the Iris side I would not hesitate much to drop support for it.

std++ has not dropped support for old Coq versions in a long time. @robbertkrebbers not sure what your policy on that is?

I don't have a policy on that. Maybe we should make a list of new Coq features that we can use. I don't think this MR alone justifies dropping support for old Coq versions, but I'm also now sure how many people actually rely on that support.

For Iris, let's do that in iris#318 (closed).

Okay seems like reopening is not possible... @tchajed could you open an MR or issue so we don't forger about byte?

mentioned in issue #62