В чем разница между обозначениями и определениями с точки зрения автотактики? - PullRequest
Новая
       68

В чем разница между обозначениями и определениями с точки зрения автотактики?

0 голосов
/ 12 октября 2019

В главе 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].) *)

Что тут за мелочи? В чем разница между Notation и Definition с точки зрения тактики auto?

1 Ответ

2 голосов
/ 13 октября 2019

Обозначения предназначены только для ваших глаз, а определения понятны ядру 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, без раскрытия.

...