The Numbers CMRA

Stream: iris-lean

[Shreyas Srinivas]

The iris numbers file defines the Numbers CMRA as nat with addition. I already defined an ordered commutative monoid that subsumes this, except the implicit positivity of nat

[Shreyas Srinivas]

Is this positivity strictly necessary or can ints qualify as numbers?

[Michael Sammler]

Iris defines cmras both for Z and nat, both for add and max so I guess all of them are useful (and none subsumes the others).

[Shreyas Srinivas]

Oh hey, nice to see one of the original iris authors here. Do you think describing Numbers as commutative monoids with a total order consistent with addition captures everything?

[Markus de Medeiros]

I think your ordered commutative monoid work is right on here

[Shreyas Srinivas]

iris-lean#67

The commit history mentions some commits in Frac, but we may rest assured that there is no intersection.

[Shreyas Srinivas]

Should I change the copyright header? The initial file came from Frac but since then most of it has changed

[Michael Sammler]

Shreyas Srinivas said:

Oh hey, nice to see one of the original iris authors here.

Just to clarify, I am not one of the original Iris authors, just someone who works with Iris quite a bit :) (Though actually more on the automation side, not too much with the different CMRA constructions.)

Shreyas Srinivas said:

Do you think describing Numbers as commutative monoids with a total order consistent with addition captures everything?

This is hard for me to says since I did not do muc fancy stuff my CMRAs myself. But I would recommend to look at uses of the CMRAs in e.g. Iris examples and see if your CMRA would work there. For example, here is an example using the max nat CMRA: https://gitlab.mpi-sws.org/iris/examples/-/blob/master/theories/lecture_notes/coq_intro_example_2.v#L413

In general, I think it would be nice if there is a mapping (e.g. in some document) from all CMRAs in Iris to CMRAs in Iris Lean such that it is easy to see that Iris lean can do everything that Iris can do.

[Shreyas Srinivas]

Michael Sammler said:

Shreyas Srinivas said:

Oh hey, nice to see one of the original iris authors here.

Just to clarify, I am not one of the original Iris authors, just someone who works with Iris quite a bit :) (Though actually more on the automation side, not too much with the different CMRA constructions.)

Shreyas Srinivas said:

Do you think describing Numbers as commutative monoids with a total order consistent with addition captures everything?

This is hard for me to says since I did not do muc fancy stuff my CMRAs myself. But I would recommend to look at uses of the CMRAs in e.g. Iris examples and see if your CMRA would work there. For example, here is an example using the max nat CMRA: https://gitlab.mpi-sws.org/iris/examples/-/blob/master/theories/lecture_notes/coq_intro_example_2.v#L413

In general, I think it would be nice if there is a mapping (e.g. in some document) from all CMRAs in Iris to CMRAs in Iris Lean such that it is easy to see that Iris lean can do everything that Iris can do.

In principle I like this idea. In practice, unless we at least add batteries (which has some moral equivalence with stdpp) as a dependency, achieving this will be difficult. For instance the current definition of Rational numbers is in Batteries. Currently our frac CMRA is a generalisation of the Coq version, but this takes the form of a typeclass. To derive an instance for $\mathbb{Q}$ we would currently have to create a downstream project that imports iris-lean and batteries.

Also I don’t know how much ordinals are required in the recent transfinite iris advances, but if they are needed, we only have them in mathlib, so that will also have to join the show. I am not opposed to that idea personally fwiw. My favourite thing to do is call import Mathlib at the beginning of a file and let #min_imports figure how to reduce this to essentials after I am done with the file.

[Kim Morrison]

I would discourage adding Mathlib as a dependency for something like iris-lean. We know there are many people out there who find some combination of Mathlib's size, speed of change, and lack of compatibility difficult to reconcile with their requirements.

Regarding Rat, we will probably need a Rat type for upcoming improvements to grind, but it remains unclear yet whether we would just make an internal-use-only version or make it part of the Lean Standard Library. Either way, it's helpful to know who would like access to it.

[Mario Carneiro]

we're likely to add a batteries import if it comes to it. Mathlib is not on the table

[Mario Carneiro]

anything needing mathlib + iris will be in a separate mathlib_iris repo

[Shreyas Srinivas]

Basically people who use Coq iris can, at a minimum, use everything in stdpp (adding more dependencies when required).

Stdpp includes all the basic number types and collection types (like sets, finsets, multi sets)

[Mario Carneiro]

stdpp is batteries

[Mario Carneiro]

it's literally the same naming convention

[Mario Carneiro]

std but more

[Shreyas Srinivas]

And the transfinite stuff?

[Shreyas Srinivas]

That’s the only thing for which I referred to mathlib

[Mario Carneiro]

depends on how it shakes out, but I'm willing to bet that it won't actually end up using ordinals, or it will use a bespoke type

[Mario Carneiro]

well founded types are in core

[Shreyas Srinivas]

Okay. Batteries should be fine though right ?

[Mario Carneiro]

yes

[Mario Carneiro]

it's not imported right now simply because there is no current need for it

[Shreyas Srinivas]

Except we don’t have Sets, Finsets, Multisets etc.

[Shreyas Srinivas]

Mario Carneiro said:

it's not imported right now simply because there is no current need for it

Ideally we should supply Frac instances for Rat. That’s how we get closer to a 1:1 mapping

[Mario Carneiro]

sets could get upstreamed to batteries

[Mario Carneiro]

for finsets et al we could probably use ExtTreeSet from core

[Shreyas Srinivas]

Is it convenient API wise?

[Mario Carneiro]

:shrug:

[Mario Carneiro]

maybe we'll be the first user

[Mario Carneiro]

generally "I'll cross that bridge when I come to it"

[Shreyas Srinivas]

It might be nice to have those code actions

[Shreyas Srinivas]

Are those in core now?

[Shreyas Srinivas]

Shreyas Srinivas said:

Mario Carneiro said:

it's not imported right now simply because there is no current need for it

Ideally we should supply Frac instances for Rat. That’s how we get closer to a 1:1 mapping

This is basically the only place we need batteries now. For feature parity with Coq iris.

[suhr]

There's long long way to feature parity. But right now the goal is to make something usable.

[Markus de Medeiros]

re. Transfinite Iris: It's still being upstreamed in Rocq, but they don't use a concrete ordinal type either. They have an interface.

[Markus de Medeiros]

I'm of the opinion that in general we should use interfaces whenever possible instead of concrete types :)

[Shreyas Srinivas]

I think I have an error in the Numbers CMRA. I am a bit tired to debug it now, and will look at this again tomorrow. If one of you finds the error, do please ping me and I might finish this CMRA earlier. See line 175. Link iris-lean#67

[Shreyas Srinivas]

Also I notice that there is a merge conflict because I added an @[ext] to the LeibnizO structure. I will fix that right away

[Shreyas Srinivas]

Concretely, I think I am missing some notion of positivity. I think I need to add 1 > 0. But it is possible the mistake lies elsewhere