在範圍內展開記號

Question

This answer提供了一個簡單有用的技巧：unfold ">="與unfold ge相同，但不要求您知道>=是ge的記號。

你可以對範圍內的符號做同樣的事嗎？

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。