Stream: Coq users

Topic: if, match, lambda and scopes

Paolo Giarrusso (Aug 27 2021 at 13:56):

To fix bugs due to missing Bind Scope foo_scope with foo., I've been slowly trying to remove all %foo specifiers from some of my projects, but that fails with if, match and lambda. I can see lambdas are harder, but if and match seems fixable.

For instance, since Iris overloads ∀ over its embedded logics, I might write

Definition foo : iProp Σ :=
  ∀ x : nat, x ≡ x.

where the return type ensures that ∀ is interpreted in the scope for the embedded logic, not Coq's logic. Additionally, this will fail if the scopes for ∀ are wrong, so that I can fix those.

However, if I use if or match, the scope does not propagate to the return arguments. Example:

Definition foo : iProp Σ :=
  (if true then
    ∀ x : nat, x ≡ x
  else
    ∀ x : nat, x ≡ x)%I.

Is there a way to get the right behavior, or do I need a bug report to Coq to patch scope propagation? I'm not looking for first-class scope-polymorphic constants, but doing this for keywords seems reasonable.

Last updated: Oct 01 2023 at 19:01 UTC