在 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。

我的previous question 和这个非常相似。也许有一些方法可以使用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.