2

我注意到符号可以被区别对待。例如<，它只是一个常规定义的符号，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

4

2 回答 2

1

发生这种情况是因为<被解释为lt哪个是定义（此处）：

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

您可以使用unfold lt.

以同样的方式<=表示le，但你不能展开le，因为它是一个类型构造函数。手册说您只能展开已定义的透明常量或局部定义。

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

于 2018-02-03T11:12:53.007 回答
1

添加到安东的答案：如果您已经知道符号是如何定义的并且只想使其在目标中可见，您可以执行类似的操作

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 指出的那样，这更容易。）

于 2018-02-07T10:09:10.893 回答