Понимание специализированной тактики

Question

Пытаясь понять ответ @keep_learning, я пошагово прошел этот код:

Inductive nostutter {X:Type} : list X -> Prop :=
| ns_nil : nostutter []
| ns_one : forall (x : X), nostutter [x]
| ns_cons: forall (x : X) (h : X) (t : list X), nostutter (h::t) -> x <> h -> nostutter (x::h::t).

Example test_nostutter_4: not (nostutter [3;1;1;4]).
Proof.
  intro.
  inversion_clear H.
  inversion_clear H0.
  unfold not in H2.
  (* We are here *)
  specialize (H2 eq_refl).
  apply H2.
Qed.

Вот то, что мы имеем перед исключением, специализируемся

H1 : 3 <> 1
H : nostutter [1; 4]
H2 : 1 = 1 -> False
============================
False

Вот eq Prop, конструктор которого eq_refl используется в specialize:

Inductive eq (A:Type) (x:A) : A -> Prop :=
    eq_refl : x = x :>A

where "x = y :> A" := (@eq A x y) : type_scope.

Я не могу объяснить, как работает эта команда:

specialize (H2 eq_refl).

Я читал про специализацию в справочном руководстве, но объяснение там слишком широкое. Насколько я понимаю, он видит, что выражение "1 = 1" в H2 удовлетворяет конструктору eq_refl и, следовательно, утверждение eq верно. Тогда это упрощает выражение:

True -> False => False

И мы получаем

H1 : 3 <> 1
H : nostutter [1; 4]
H2 : False
============================
False

Может ли кто-нибудь дать мне минимальный пример с объяснением того, что делает specialize, чтобы я мог свободно его использовать?

Обновление

Пытаясь имитировать, как работает specialize, используя apply, я сделал следующее:

Example specialize {A B: Type} (H: A -> B) (a: A): B.
Proof.
  apply H in a.

Это дает:

A : Type
B : Type
H : A -> B
a : B
============================
B

Почти так же, как specialize, только другое название гипотезы.

В теореме test_nostutter_4 я попробовал это, и это сработало:

remember (@eq_refl nat 1) as Heq.
apply H2 in Heq as H3.

Это дает нам:

H1 : 3 <> 1
H : nostutter [1; 4]
H2 : 1 = 1 -> False
Heq : 1 = 1
H3 : False
HeqHeq : Heq = eq_refl
============================
False

Этот был более сложным, нам пришлось ввести новую гипотезу Heq. Но мы получили то, что нам нужно - H3 в конце.

Использует ли внутренняя специализация что-то вроде "помни"? Или это можно решить с помощью apply, но не помните?

Answer 1

specialize в простейшем виде просто заменяет данную гипотезу той гипотезой, которая применяется к какому-либо другому термину.

В этом доказательстве

Example specialize {A B: Type} (H: A -> B) (a: A): B.
Proof.
  specialize (H a).
  exact H.
Qed.

у нас изначально есть гипотезаH: A -> B.Когда мы вызываем specialize (H a), мы применяем H к a (применяется как в приложении функции).Это дает нам что-то типа B.specialize затем избавляется от старого H для нас и заменяет его результатом приложения.Это дает новой гипотезе то же имя: H.

В вашем случае у нас есть H2: 1 = 1 -> False, которая является функцией от типа 1 = 1 до типа False.Это означает, что H2, примененный к eq_refl, имеет тип False, то есть H2 eq_refl: False.Когда мы используем тактику specialize (H2 eq_refl)., старый H2 очищается и заменяется новым термином (H2 eq_refl), тип которого False.Тем не менее, оно сохраняет старое имя H2.

specialize полезно, если вы уверены, что собираетесь использовать гипотезу только один раз, поскольку она автоматически избавляется от старой гипотезы.Одним из недостатков является то, что старое имя может не соответствовать смыслу новой гипотезы.Однако в вашем случае и в моем примере H - это достаточно общее имя, которое работает в любом случае.

---

К вашему обновлению ...

specialize - этоОсновная тактика определяется непосредственно в плагине ltac.Он не использует никакую другую тактику для внутреннего использования, поскольку он является его внутренностями.

Если вы хотите сохранить гипотезу, вы можете использовать модификатор as, который работает для обоих specialize и apply.В доказательстве

Example specialize {A B: Type} (H: A -> B) (a: A): B.
Proof.

, если вы сделаете specialize (H a) as H0. вместо очистки H, будет введена новая гипотеза H0: B.apply H in a as H0. имеет тот же эффект.