从 auto 策略的角度来看，Notation 和 Definition 有什么区别？

Question

在STLC chapter of Programming Language Foundations中，我们找到以下内容：

(** [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——就像所有策略一样——不过是从句法上看术语。例如，如果您要编写以下 stupid 策略：

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 相同，无需进行任何展开。

从 auto 策略的角度来看，Notation 和 Definition 有什么区别？

What is the difference between Notation and Definition from the point of view of the auto tactic?

coq

coq-tactic