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

问题描述

说我有一个这样的假设：

Say I have a hypothesis like this:

FooProp a b

我想将假设更改为以下形式：

I want to change the hypothesis to this form:

exists a, FooProp a b

我该怎么做？

我知道我可以通过eauto进行 assert（存在，FooProp ab），但是我正在尝试寻找一种不需要我明确声明的解决方案写下整个假设；这对于自动化是不利的，并且在假设不重要的情况下通常只是令人头疼。理想情况下，我想在H1中指定 intro_exists a ；

I know I can do assert (exists a, FooProp a b) by eauto but I'm trying to find a solution that doesn't require me to explicitly write down the entire hypothesis; this is bad for automation and is just generally a headache when the hypothesis are nontrivial. Ideally I'd like to specify intro_exists a in H1 or something; it really should be that simple.

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

EDIT: Why? Because I have a lemma like this:

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

我正在尝试像这样重写：

And I'm trying to rewrite like this:

rewrite <- find_instr_in in H1

哪个失败，错误为未找到匹配存在z，...的子项... 。但是，如果我通过eauto声明（存在z，find_instr zc =一些i）。首先，重写有效。

Which fails with the error Found no subterm matching "exists z, ..." .... But if I assert (exists z, find_instr z c = Some i) by eauto. first the rewrite works.

推荐答案

类似这样的东西：

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.

关键是模式策略，它查找术语的出现并将其抽象为应用于自变量的函数。因此，模式a 会从 FooProp ab 转换 H 的类型。到（fun x => FooProp xb）a 。之后，Coq可以弄清楚您申请 ex_intro 的意思。

The key to this is the pattern tactic, which finds occurrences of a term and abstracts them into a function applied to an argument. So pattern a converts the type of H from FooProp a b to (fun x => FooProp x b) a. After that, Coq can figure out what you mean when you apply ex_intro.

编辑：
在您的具体情况下，我会说实际建议使用另一种方法，即不要这样陈述引理。取而代之的是将它分成两个引理，每个方向一个引理是方便的。向前的方向是相同的，但向后的方向应重新设置如下

All that being said, in your concrete case I would actually recommend a different approach, which is to not state your lemma like that. Instead it is convenient to split it into two lemmas, one for each direction. The forwards direction is just the same, but the backwards direction should be restated as follows

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

如果执行此操作，则重写将成功而无需引入存在性。

If you do this, then the rewrite will succeed without needing to introduce the existential.

这篇关于如何在假设中将具体变量更改为存在量化的var？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！