1

假设我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使这个工作也有效。

4

1 回答 1

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.
于 2014-09-10T12:56:02.133 回答