Avoid sequences of "_" by adjusting lemma statements
Some Iris lemmas are prone to needing plenty of _
almost every time they are used. I noticed this in particular for
- most big-op lemmas that access a single element, where the to-be-accessed element needs to be given explicitly, but often other arguments come first
- several allocation lemmas such as
inv_alloc
, where the to-be-allocated thing needs to be given explicitly, but other arguments come first - many of the update lemmas, where typically one works with
iMod
, so the new values (e.g. new lower bound for mono_nat, or new key and value for gmap) need to be given, but they are often the last arguments
There are two ways to fix this:
- reorder arguments, so that those that are likely to be determined by unification come first
- make likely-to-be-determined-by-unification arguments implicit, so that we do not have to write out their
_
I am in favor of the second approach because it has a better failure mode: if one of those arguments ends up not being determined by unification, we have use lemma (arg:=val)
to explicitly give the value for this agument. For lemmas with many arguments, this name-based approach is anyway much easier to read and write than the position-based approach (no need to remember the exact order of arguments).
However, while implicit arguments are widely used in Iris, we usually control them on a per-section basis, not a per-lemma basis. @robbertkrebbers has objected the used of implicit arguments for this reason. (That is my understanding, anyway.)