Лучший способ для выполнения универсального инстанцирования в Кок

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

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

3 2
coq

3 ответа:

pose proof (H x) as H'.

Скобки необязательны.

4

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

assert (H' := H x).

Если можно заменить существующую гипотезу 

specialize (H x).
3

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

1