Understanding and Porting O/RFunctors

Stream: iris-lean

[Oliver Soeser]

I'm making progress on porting excl.v to Lean, however I have encountered some difficulties with implementing the functors. I haven't been able to go off Agree.lean since its functors have not yet been ported. Furthermore I struggle to gain much of an intuition with regards to the O/RFunctors just by reading the definitions in OFE.lean and CMRA.lean. Does anyone know how these functors should be ported?

[Shreyas Srinivas]

I think Markus already worked on this

[Shreyas Srinivas]

I agree that agree.lean is not a great place to learn how to port cmras

[Shreyas Srinivas]

I instead have spent some spare time just reading the iris tutorial

[Markus de Medeiros]

Glad to hear you're making progress! The O/RFunctors are typeclasses on top of COFE.OFunctorPre, which should correspond to the oFunctor_car or rFunctor_car fields in Rocq. For excl You should be able to prove an instance of RFunctor and RFunctorContractive with your OFunctorPre as the parameter.

We do have one example of porting functors in UPred.lean to give you an idea of what it might look like.

[Markus de Medeiros]

If you're still stuck, feel free to make a PR and I can take a look at it :)

[Oliver Soeser]

Thanks! I think I've figured it out now, PR is up

[Markus de Medeiros]

Nice work! FYI I think the few remaining lemmas from excl.v (the discrete stuff, includedN...) should be pretty easy as well.

[Markus de Medeiros]

iris-lean#30 should also be pretty easy for you if you're looking for more work