Skip to content

Generalizing the Proofmode

I am sure I have this request this issue with almost everyone already but let me summarize it here again: In our iGPS work, we work with monotone (Iris) predicates over a type called views - though the actual type doesn't matter much. We call these predicates vPreds. In spirit, all proofs are done with respect to a "current" view which changes when taking a step – not unlike step indices, I think. However, we currently have to manually upgrade the view of our assumptions to the new view after taking a step to achieve coherence between the goal and the assumptions.

Since I am about to start another development with the same setup I wanted to gather information on how to hide the views from the potential users of our logic. I talked to @jjourdan about this and he suggested a bunch of hacky steps that could potentially make the views disappear. The approach uses a typeclasse to represent the current view of the proof. However, I think we will still suffer from some inherent drawbacks: we have to redefine connectives, the proof mode syntax, and probably many more things. If possible I would prefer a more principled solution.

Here's an incomplete list of pain points with our current setup:

  1. Views show up in the proof context.
  2. Views show up in the proof script. (We can mostly hide them behind custom tactics and underscores, though.)
  3. We define what amounts to an incomplete copy of the uPred scope to get all the logical connectives on vPreds.
  4. Because we do not want to redefine every last bit (especially lemmas) of uPred, we sometimes unfold away all the vPred stuff. This results in scope chaos, with annotations %I and %VP everywhere.
  5. Once we unfold, refolding is almost impossible.
  6. The typeclasses for the proofmode are not always smart enough to see through our definitions and recognize the underlying uPreds. (I think this is largely fixed but I don't quite remember what the exact issue were. They might pop up again in different circumstances)

I think that these issues could be fixed by making the proofmode more general. Maybe it would be parametrized by a BI with the more intricate parts (viewshift stuff?) parametrized by additional assumptions on the BI. Maybe different parts of it would have different parameters. I haven't thought a lot about the specifics. What I think this doesn't immediately fix is the interaction between two different logics like vPred and uPred: How does one make the proofmode aware of the two different levels? Can we get rid of the need to switch between the two logics entirely or should we try to make it possible to switch between them inside proofs?

I would love to hear your feedback on this. Maybe there are other ways of going about this? @robbertkrebbers, I know you thought about this as well. What is the best approach in your view?

/cc @haidang