Provide a convenient way to define non-recursive ghost state
It is somewhat annoying, in particular from a teaching perspective, that we have to use incantations like the following each time we want to use some ghost state:
Class lockG Σ := LockG { lock_tokG :> inG Σ (exclR unitC) }.
Definition lockΣ : gFunctors := #[GFunctor (exclR unitC)].
Instance subG_lockΣ {Σ} : subG lockΣ Σ → lockG Σ.
Proof. solve_inG. Qed.
To make things worse, if you forget the lockΣ
, your proof will still work. You might just have assumed false, accidentally.
Can we do better than that, at least for the simple and common case of non-recursive ghost state?