GitLab

This MR introduces a connective called ilocked that can be used to stop iNext and iFrame from unfolding definitions.

To demonstrate why this is useful, consider:

Definition foo : uPred M := (▷ something_big ∧ and_even_bigger)%I

Whenever we have a premise H : foo, the tactic iNext will unfold the definition of foo, which is not always desired. To avoid this behavior, we often seal-off the body of foo, which is quite a drastic measure, as we need to unseal whenever we want to do anything with a foo. This is especially cumbersome for auxiliary definitions where sealing doesn't also give a performance gain.

The ilocked connective in the MR proves a more lightweight solution. When a definition is flagged using ilocked, the tactics iNext and iFrame will not unfold it, but all other tactics, like iDestruct, iSplit and iLeft will.

Definition foo : uPred M := ilocked (▷ something_big ∧ and_even_bigger)%I

It works in a rather simple way, the connective ilocked is defined Typeclasses Opaque so that it will not be unfolded by type class search.

Definition ilocked {A} (x : A) : A := x.
Typeclasses Opaque ilocked.
Arguments ilocked {_} _ /.

To make sure that other tactics will unfold it, we define a bunch of instances like:

Instance into_pure_ilocked {M} (P : uPred M) φ :
  IntoPure P φ → IntoPure (ilocked P) φ := id.
Instance from_pure_ilocked {M} (P : uPred M) φ :
  FromPure P φ → FromPure (ilocked P) φ := id.
Instance from_and_ilocked {M} p (P Q1 Q2 : uPred M) :
  FromAnd p P Q1 Q2 → FromAnd p (ilocked P) Q1 Q2 | 100 := id.
Instance into_and_ilocked {M} p (P Q1 Q2 : uPred M) :
  IntoAnd p P Q1 Q2 → IntoAnd p (ilocked P) Q1 Q2 := id.
Instance from_or_ilocked {M} (P Q1 Q2 : uPred M) :
  FromOr P Q1 Q2 → FromOr (ilocked P) Q1 Q2 := id.

TODO

• Figure out where to put this stuff.
• What would be a better name for the connective?
• We currently do not have instances for PersistentP and TimelessP for ilocked. Should we add those? Are other instances missing?