How to proof existence in COQ?

Question

I am quite new to Coq and I am trying to proof the following lemma (with the Reals library):

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

Now, I get stuck when I try to find a suitable N such that for all n >= N the sequence converges. I know how to do it by hand, but I do not know how to program this into Coq.

This is my proof so far:

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.

And I am left with:

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

And the problem is that I do not know how to get rid of the "exists N".

Is this even possible? And if it is, can anyone help me?

Thanks in advance!

user4614475 user4614475 · Accepted Answer · 2019-02-18T20:52:05

Generally, to eliminate exists N in coq, you need to instantiate it with a term. If you were to write this out by hand, you would probably write something like, "since An converges, there is some N such that ..." and then you would use that N in your proof.

To do this in Coq, you will need to use the destruct tactic on A_cv. Once you have this N, you can use it to instantiate and continue like you'd expect.

Full proof for reference:

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.

How to proof existence in COQ?

1 Answers