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

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 策略，它找到一个术语的出现并将它们抽象为一个应用于参数的函数。所以 pattern a 将 H 的类型从 FooProp a b 转换为 (fun x => FooProp x b) a。之后，你应用ex_intro时，Coq 就能理解你的意思了。

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

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

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

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

How do I change a concrete variable to an existentially quantified var in a hypothesis?

coq