coq - 如何在假设中将具体变量更改为存在量化的变量？

Question

假设我有一个这样的假设:

FooProp a b

我想将假设更改为这种形式:

exists a, FooProp a b

我怎样才能做到这一点？

我知道我可以做 assert (exists a, FooProp a b) by eauto但我试图找到一个不需要我明确写下整个假设的解决方案；这对自动化不利，并且在假设不重要时通常会令人头疼。理想情况下，我想指定 intro_exists a in H1或者其他的东西;真的应该这么简单。

编辑 : 为什么？因为我有一个这样的引理:

Lemma find_instr_in: 
  forall c i,
   In i c <-> (exists z : Z, find_instr z c = Some i).

还有一个这样的假设:

H1: find_instr z c = Some i

我正在尝试像这样重写:

rewrite <- find_instr_in in H1

失败并出现错误 Found no subterm matching "exists z, ..." ... .但如果我 assert (exists z, find_instr z c = Some i) by eauto.首先重写工作。

Answer 1

这样的事情怎么样:

Ltac intro_exists' a H :=
  pattern a in H; apply ex_intro in H.

Tactic Notation "intro_exists" ident(a) "in" ident(H) := intro_exists' a H.

Section daryl.
  Variable A B : Type.
  Variable FooProp : A -> B -> Prop.

  Goal forall a b, FooProp a b -> False.
    intros.
    intro_exists a in H.
  Admitted.
End daryl.

关键是 pattern tactic，它找到一个术语的出现并将它们抽象成一个应用于参数的函数。所以 pattern a转换 H 的类型来自 FooProp a b至 (fun x => FooProp x b) a .之后，Coq 就能弄清楚你申请时的意思 ex_intro .

编辑:
话虽如此，在您的具体情况下，我实际上会推荐一种不同的方法，即不要那样陈述您的引理。相反，将它分成两个引理很方便，每个方向一个。向前的方向是一样的，但向后的方向应该重新表述如下

forall c i z, 
  find_instr z c = Some i -> In i c.

如果你这样做，那么重写将成功而无需引入存在。