Skip to content

Add duplicable type class

Simon Friis Vindum requested to merge simonfv/iris:duplicable-type-class into master

I took a stab at adding a type class for duplicable resources. I've been using the duplicable resource ∃ q, l ↦{q} v quite a lot in a project, and I think it would be nice if the proof mode had better support for duplicable resources. This MR is intended to be a step in that direction.

This MR adds a type class Duplicable for duplicable resources. Where applicable it changes existing lemmas such that they are either instances of the Duplicable type class or otherwise makes use of Duplicable. I found those places by looking for occurrences of dup in the code. I might have missed some places, especially if they do not use the string dup.

I wasn't sure if the type class should use a bi entailment (P ⊣⊢ P ∗ P) or a normal entailment (P ⊢ P ∗ P). As several of the existing duplicable lemmas used the bi entailment I did so as well. In an affine setting those should be equivalent, and I guess that even in a non-affine setting a duplicable proposition will support both directions. If that is not the case, the type class should probably be defined using only a normal entailment.

I wanted to add an IntoSep instance for duplicable resources as follows:

Global Instance from_sep_duplicable P : Duplicable P → FromSep P P P.

This would make it easy to make copies of duplicable resources. However, this instance turned out to be problematic. Take for instance the proposition R : A ∧ B where both A and B are persistent. Then, since R is persistent it is duplicable which leads to a FromSep instance. Additionally, there is a FromSep instance for conjunction. Hence iDestrut "R" as "[N M]". becomes ambiguous, and, after I added the above instance, Coq ended up picking the FromSep instance from Duplicable which is definitely not what one would want in that case.

I'm not sure what the best solution to that problem is. Maybe the FromSep instance could be given lower priority so Coq would pick it last? But I'm not sure if that is more trouble than it is worth and it sounds quite brittle to me. Alternatively, the FromSep instance is useful for duplicating resources, but if the proof mode allowed one to use duplicable resources without them getting consumed, then that need would go away at least to some extend. I.e., other features along those lines may obliterate the need for a FromSep instance.

This is a breaking change, so an addition to the changelog should be added if we decide to merge this.

Merge request reports