存在下重写

Question

说我有以下关系：

Inductive my_relation: nat -> Prop :=
constr n: my_relation n.

我想证明以下几点：

Lemma example:
  (forall n, my_relation n -> my_relation (S n)) -> (exists n, my_relation n) -> exists n, my_relation (S n).
Proof.
  intros.

介绍之后，我具有以下环境：

1 subgoal
H : forall n : nat, my_relation n -> my_relation (S n)
H0 : exists n : nat, my_relation n
______________________________________(1/1)
exists n : nat, my_relation (S n)

我的问题是：是否有可能在存在量词下重写H？如果不是，是否有解决此类问题的策略（该特定问题并非真正相关，但是存在的问题是您必须证明exists使用另一种问题exists，并且在非正式情况下可以“推论”一种方法来重写该问题）exists。假设进入exists目标）？

例如，如果尝试尝试rewrite H in H0.，将出现错误（Error: Cannot find a relation to rewrite.）。

Answer 1

操作假设中存在量化的标准方法是使用inversion或更好和更简单地使用来获得属性的见证destruct。

您可以使用以下语法之一为变量命名：

destruct H0 as (n, H0).
destruct H0 as [n H0].
destruct H0 as (n & H0).

请注意，您还可以使用介绍模式来破坏假设。

intros H (n & H0).

您甚至可以直接H在中申请H0。

intros H (n & H0%H). exists n. assumption.

软件基金会对此进行了清晰的解释。