Arrow on relations

Stream: Is there code for X?

[Joachim Breitner]

I am playing around with program verification proofs in the refinement style. I believe I have seen a rather elegant way of expressing how abstract and concrete types and operations relate using an arrow on relations, something of type

Rel a a' -> Rel b b' -> Rel (a -> b) (a' -> b')

Do we have something like this? Possibly even with an API or even tactics to automate refinement proofs (possibly also known as transfer and lifting)?

[Kyle Miller]

Is it docs#Relator.LiftFun ?

[Joachim Breitner]

Yes it is! No API around it though. I'll play around with it once the weather is worse :-)