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

发生这种情况是因为 < 被解释为 lt，这是一个定义 (here):

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

你可以用unfold lt达到同样的效果。

同理<=表示le，但是不能展开le，因为它是类型构造函数。手册说只能展开定义的透明常量或局部定义。

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

Answer 2

添加到 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.，但是，正如安东指出的那样，这更容易。）

ltac 中的展开符号

unfold notation in ltac

coq

ltac