在Coq中是否有一种类似“有效”的策略可以实现“存在”目标？ [英] is there a `eapply`-like tactic that works on `exists` goals in Coq?

问题描述

在证明中，目标是存在的，目标属性是其中的假设之一。

I have the following during a proof where the goal is an existential, and the target property is one of the assumptions.

H : x ==> y
...
______________________________________(1/2)
exists t : tm, x ==> t

我知道我可以做到存在。运用H。来证明当前的目标，但是我想知道是否有更聪明的策略可以直接使用假设来证明存在的目标，例如 eapply H ？

I know I can do exists y. apply H. to prove the current goal, but I am wondering if there is a more intelligent tactic that can use the assumption directly to prove the existential goal here, like eapply H?

由于这是一个统一的标准，所以不必写 X 中的c>部分存在X。。

Since this is one unification away, it would be nice not having to write the X part in exists X..

如果不存在这种策略，我该怎么写？

If such a tactic does not exist, how do I write one?

推荐答案

存在这样的策略，称为 exists 。
它确实符合您的期望。

There exists such a tactic and it is called eexists. It does exactly what you seem to expect.

https://coq.inria.fr/distrib/current/refman/Reference-Manual010.html#hevea_tactic23

示例用法：

Variable T : Type.
Variable R : T -> T -> Prop.

Theorem test : forall x y, R x y -> exists t, R x t.
Proof.
  intros. eexists. apply H.
Qed.

这篇关于在Coq中是否有一种类似“有效”的策略可以实现“存在”目标？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！