在范围内展开方程式

Question

This answer 提供了一个简单有用的技巧：unfold ">=" 与 unfold ge 相同，但不需要您知道 >= 是 [=15 的表示法=].

你能对范围内的符号做同样的事情吗？

Require Import NArith.
Goal forall x, (x >= x)%N.
unfold ">=".

这里 unfold ">=" 不做任何事情，因为它试图展开 ge，而不是 N.ge。

我找到了以下解决方案：

Open Scope N.
unfold ">=".

但是有没有一种语法允许在不首先打开范围的情况下展开这个符号？

Answer 1

是的，您可以按如下方式使用模板unfold string % scope：

Require Import NArith.
Goal forall x, (x >= x)%N.
  unfold ">=" % N.

这给了我们目标 forall x : N, (x ?= x)%N <> Lt 展开 >=。

Unfold a notation within a scope