Лучший способ создания экземпляра вложенного экзистенциального оператора в Coq

Question

Предположим, у меня есть вложенное экзистенциальное утверждение H : exists ( a : A ) ( b : B ) ( c : C ) ... ( z : Z ), P a b c ... z в контексте. Как лучше всего создать экземпляр H и получить новую гипотезу H' : P a b c ... z? Делая это путем повторного inversion занимает много времени и оставляет все нежелательные промежуточные шаги, такие как H0 : exists ( b : B ) ( c : C ) ... ( z : Z ), P a b c ... z,

Мой предыдущий вопрос очень похож на этот. Может быть, есть какой-то способ использовать pose proof или же generalize чтобы заставить это работать.

Answer 1

То, что вы хотите сделать, не называется "создание экземпляров". Вы можете создать универсально выраженную гипотезу и создать экзистенциально количественное заключение, но не наоборот. Я думаю, что правильное имя "введение". Вы можете ввести экзистенциальное количественное определение в гипотезу, и вы можете ввести универсальное количественное определение в заключение. Если вам кажется, что вы "исключаете" вместо этого, это потому, что, когда вы что-то доказываете, вы начинаете с нижней части последовательного вывода исчисления и продвигаетесь назад к вершине.

Во всяком случае, использовать тактику firstorder, Также используйте команду Set Firstorder Depth 0 отключить пробный поиск, если вы хотите упростить свою цель.

Если ваша цель имеет элементы более высокого порядка, вы, вероятно, получите сообщение об ошибке. В этом случае вы можете использовать что-то вроде simplify,

Ltac simplify := repeat
  match goal with
  | h1 : False |- _ => destruct h1
  | |- True => constructor
  | h1 : True |- _ => clear h1
  | |- ~ _ => intro
  | h1 : ~ ?p1, h2 : ?p1 |- _ => destruct (h1 h2)
  | h1 : _ \/ _ |- _ => destruct h1
  | |- _ /\ _ => constructor
  | h1 : _ /\ _ |- _ => destruct h1
  | h1 : exists _, _ |- _ => destruct h1
  | |- forall _, _ => intro
  | _ : ?x1 = ?x2 |- _ => subst x2 || subst x1
  end.