Library iris.proofmode.reduction

The following tactics should be used when performing computation in the proofmode:

• Use cbv/vm_compute (depending on expected size of computation) if the expected result is a simple term (say, a boolean, number, list of strings), and the input term does *not* involve user terms (such as bodies of hypotheses in the proof mode environment).
• Use lazy if the expected result is a simple term and the input term *does* involve user terms.
• Use pm_eval otherwise, particularly to compute new proof mode environments and to lookup items in the proof mode environment.

The reduction pm_eval avoids reducing anything user-visible to make sure we do not reduce e.g., before unification happens in iApply. This needs to contain all definitions used in the user-visible statements in coq_tactics, and their dependencies. Examples:

• envs_lookup i Δ, where Δ is a proof mode environment. This should be computed using pm_eval because Δ involves user terms and the result is also a user term (a hypothesis).
• dom Δ, where Δ is a proof mode environment. This should be computed with lazy because Δ involves user terms and the result is a list of strings. This should *never* be computed using cbv/vm_compute as that would eagerly unfold all hypotheses in Δ. Note that in this specific case one could also use pm_eval because all definitions in dom are whitelisted by pm_eval. However, lazy is more useful when considering f (dom Δ) where f is not whitelisted, as pm_eval would simply get stuck.
• tc_to_bool (BiAffine PROP). This should be computed using lazy as PROP involves user terms (a BI canonical structure instance) and the result is a mere Boolean. This term trivially normalizes with lazy to a Boolean (which is present as implicit parameter derived by TC search), while cbv would eagerly normalize the whole of PROP (i.e., all BI operations contained in the record).

Called by many tactics for redexes that are created by instantiation. This cannot create any envs redexes so we just do the cbn part.