Лучший способ выполнить универсальную реализацию в Coq

Question

Предположим, у меня есть гипотеза H : forall ( x : X ), P x и переменная x : X в контексте. Я хочу выполнить универсальную реализацию и получить новую гипотезу H' : P x, Какой самый безболезненный способ сделать это? По-видимому apply H in x не работает. assert ( P x ) с последующим apply H делает, но это может стать очень грязным, если P это сложно.

Есть похожий вопрос, который кажется несколько связанным. Не уверен, что это можно применить здесь, хотя.

Answer 1

pose proof (H x) as H'.

Скобки не являются обязательными.

Answer 2

Если вам нужна новая гипотеза, вы можете использовать ответ @Ptival, или

assert (H' := H x).

Если это нормально, чтобы заменить существующую гипотезу

specialize (H x).

Answer 3

Вы можете использовать что-то вроде generalize (H x); intros Hx: generalize добавлю (H x) как новый смысл перед текущей целью, и intros поместит это в ваши гипотезы.