ltac中的表示法

Question

我注意到符号可以被不同的对待。例如，<只是普通定义的表示法，而unfold "<"确实工作，如下例所示：

Theorem a : 4 < 5.
Proof.
    unfold "<".

但是，<=是与类型le相关联的符号，由于某些原因，unfold "<="无法工作，如下面的示例所示：

Theorem a : 4 <= 5
Proof.
   unfold "<=".

这在Unable to interpret "<=" as a reference中失败了。

我可以使用ltac命令将4 <= 5转换为le 4 5吗？

Answer 1

添加到Anton的回答:如果您已经知道如何定义表示法，并且只想使它在目标中可见，您可以这样做

Definition make_visible {X} (f : X) := f.

Notation "` f" := (make_visible f) (at level 5, format "` f").

Tactic Notation "unfold" "notation" constr(f) :=
  change f with (`f).
Tactic Notation "fold" "notation" constr(f) :=
  unfold make_visible.

Theorem a : 4 <= 5.
Proof.
  unfold notation le.
  fold notation le.

(编辑:我的第一个解决方案是Definition make_visible {X} (f : X) := (fun _ => f) tt.，但是，正如Anton指出的，这更容易。)

Answer 2

之所以会发生这种情况，是因为<被解释为lt，这是一个定义(这里)：

Definition lt (n m:nat) := S n <= m.

您可以使用unfold lt实现同样的效果。

同样，<=的意思是le，但您不能展开le，因为它是一个类型构造函数。手册说，您只能展开定义的透明常量或本地定义。

这里的结果是，你不展开符号，而是展开那些符号所指的定义。