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

Question

In the STLC chapter of Programming Language Foundations, we find the following:

(** [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].) *)

What's the nitty gritty here? What is the difference between Notation and Definition from the point of view of the auto tactic?

Answer 1

Notations are just for your eyes, while definitions are understood by the coq kernel, making it a first difference. When typechecking a term, it shouldn't have much impact since definitions can be unfolded.

Definition foo : nat := 3 + 3.

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

auto—like all tactics—is looking at terms syntactically however. If you were for instance to write the following stupid tactic:

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

Then it would only apply when your goal is exactly (ie syntactically) 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.

Now, things are different with a notation, as I said, only you can see them, ltac doesn't.

Notation foofoo := (3 + 3).

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

For ltac, foofoo is the same as 3+3 without any unfolding to be done.