Как доказать существование в COQ? - PullRequest
Новая
       6

Как доказать существование в COQ?

0 голосов
/ 18 февраля 2019

Я совершенно новичок в 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".

Возможно ли это вообще?И если это так, кто-нибудь может мне помочь?

Заранее спасибо!

1 Ответ

0 голосов
/ 18 февраля 2019

Как правило, чтобы исключить exists N в coq, вам нужно создать его с помощью термина.Если бы вы написали это от руки, вы, вероятно, написали бы что-то вроде: «поскольку 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.
...