如何在COQ中证明存在？

Question

我对 Coq 还很陌生，我正在尝试证明以下引理（使用 Reals 库）：

forall (An : nat -> R) (a : R),  Un_cv An a -> Un_cv (fun i : nat => An i - a) 0.

现在，当我试图找到一个合适的 N 使得对于所有 n >= N 序列收敛时，我陷入了困境。我知道如何手工完成，但我不知道如何将其编程到 Coq 中。

这是我迄今为止的证明：

Proof.
  intros An a A_cv.
  unfold Un_cv. unfold Un_cv in A_cv.
  intros eps eps_pos.
  unfold R_dist. unfold R_dist in A_cv.

我只剩下：

1 subgoal
An : nat -> R
a : R
A_cv : forall eps : R,
       eps > 0 -> exists N : nat, forall n : nat, (n >= N)%nat -> Rabs (An n - a) < eps
eps : R
eps_pos : eps > 0
______________________________________(1/1)
exists N : nat, forall n : nat, (n >= N)%nat -> Rabs (An n - a - 0) < eps

问题是我不知道如何摆脱“存在N”。

这可能吗？如果是的话，有人可以帮助我吗？

提前致谢！

Answer 1

一般来说，要消除coq中的

exists N

，需要用一个term来实例化它。如果你要用手写出来，你可能会写出类似这样的内容，“因为

An

收敛，所以有一些

N

这样......”，然后你会在证明中使用该

N

。

要在 Coq 中执行此操作，您需要对

destruct

使用

A_cv

策略。 一旦你有了这个

N

，你就可以用它来实例化并像你期望的那样继续。

完整证明供参考：

Lemma some_lemma : forall (An : nat -> R) (a : R),  Un_cv An a -> Un_cv (fun i : nat => An i - a) 0.
Proof.
  intros An a A_cv.
  unfold Un_cv. unfold Un_cv in A_cv.
  intros eps eps_pos.
  unfold R_dist. unfold R_dist in A_cv.
  destruct (A_cv eps eps_pos) as [N HN].
  exists N; intro.
  rewrite Rminus_0_r.
  apply HN.
Qed.