从自动策略的角度来看，符号和定义之间有什么区别?

Question

在编程语言基础的STLC章节中，我们发现以下内容：

(** [idB = x:Bool. x] *)
Notation idB :=
(abs x Bool (var x)).
(** [idBB = x:Bool->Bool. x] *)
Notation idBB :=
(abs x (Arrow Bool Bool) (var x)).
[...]
(** (We write these as [Notation]s rather than [Definition]s to make
things easier for [auto].) *)

这里的关键是什么？从auto战术的角度来看，Notation和Definition有什么区别？

Answer 1

符号只是为了你的眼睛，而定义是由coq内核理解的，使其成为第一个区别。 在对术语进行类型检查时，它应该不会产生太大影响，因为定义可以展开。

Definition foo : nat := 3 + 3.
(* [foo] is convertible to [3 + 3], its definition. *)
Check eq_refl : foo = 3 + 3.

然而，auto- 像所有策略一样 - 正在从语法上看待术语。 例如，如果您要编写以下愚蠢的策略：

Ltac bar :=
lazymatch goal with
| |- foo = 3 + 3 => reflexivity
end.

那么它仅适用于您的目标完全(即语法上(foo = 3 + 3.

Goal foo = foo.
Proof.
Fail bar.
unfold foo at 2. (* We need to unfold [foo] on the right to apply our tactic. *)
bar.
Qed.

现在，符号是不同的，正如我所说，只有你能看到它们，ltac没有。

Notation foofoo := (3 + 3).
Goal foofoo = 3 + 3.
Proof.
match goal with
| |- 3 + 3 = 3 + 3 => reflexivity
end.
Qed.

对于ltac，foofoo与3+3相同，无需进行任何展开。