More documentation.

iris/proofmode/ltac_tactics.v

@@ -418,6 +418,7 @@ Ltac iFrameAnyIntuitionistic :=
     match Hs with [] => idtac | ?H :: ?Hs => repeat iFrameHyp H; go Hs end in
   match goal with
   | |- envs_entails ?Δ _ =>
+     (* [lazy] because [Δ] involves user terms *)
      let Hs := eval lazy in (env_dom (env_intuitionistic Δ)) in go Hs
   end.
 
@@ -427,6 +428,7 @@ Ltac iFrameAnySpatial :=
     match Hs with [] => idtac | ?H :: ?Hs => try iFrameHyp H; go Hs end in
   match goal with
   | |- envs_entails ?Δ _ =>
+     (* [lazy] because [Δ] involves user terms *)
      let Hs := eval lazy in (env_dom (env_spatial Δ)) in go Hs
   end.
 
@@ -1021,6 +1023,7 @@ Tactic Notation "iSpecializeCore" open_constr(H)
        (* Check if we should use [tac_specialize_intuitionistic_helper]. Notice
        that [pm_eval] does not unfold [use_tac_specialize_intuitionistic_helper],
        so we should do that first. *)
+       (* [lazy] because [Δ] involves user terms *)
        let b := eval lazy [use_tac_specialize_intuitionistic_helper] in
          (if p then use_tac_specialize_intuitionistic_helper Δ pat else false) in
        lazymatch eval pm_eval in b with
@@ -1030,6 +1033,7 @@ Tactic Notation "iSpecializeCore" open_constr(H)
           lazymatch iTypeOf H with
           | Some (?q, _) =>
              let PROP := iBiOfGoal in
+             (* [lazy] because [PROP] involves user terms *)
              lazymatch eval lazy in (q || tc_to_bool (BiAffine PROP)) with
              | true =>
                 notypeclasses refine (tac_specialize_intuitionistic_helper _ H _ _ _ _ _ _ _ _ _ _);

iris/proofmode/reduction.v

@@ -12,12 +12,31 @@ proofmode:
 - 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. *)
+  and to lookup items in the proof mode environment.
 
-(** The reduction [pm_eval] avoids reducing anything user-visible to make sure
+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. *)
+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). *)
 Declare Reduction pm_eval := cbv [
   (* base *)
   base.negb base.beq