Use HB.lock(-like) sealing
hierarchy-builder offers a sealing mechanism that looks extremely syntactically lightweight, while doing module-based sealing under the hood (meaning it probably seals better than our seal
type, though I am not sure if that makes a difference in practice.
Quoting from https://github.com/math-comp/hierarchy-builder/wiki/Locking:
HB.lock Definition new_concept := 999999.
Lemma test x : new_concept ^ x ^ new_concept = x ^ new_concept ^ new_concept.
Proof.
Time Fail reflexivity. (* takes 0s *)
rewrite new_concept.unlock.
Time Fail reflexivity. (* takes 7s, the original body is restored *)
Abort.
This is exactly the kind of locking API I always wanted: just adding a keyword in front of the Definition
, done. This would make it a no-brainer to seal basically every iProp
that our reusable libraries export.
TODO:
- Check if this actually works in Iris
- Decide if we want to do this, and how -- are we okay with a dependency on hierarchy-builder?