The Coq mailing list

[Saulo Araujo <saulo2 AT gmail.com>]

Thanks a lot Amin!

Saulo

On Fri, Feb 13, 2015 at 11:41 AM, Amin Timany <amintimany AT gmail.com> wrote:

Hi,

Here is a proof for a very close theorem.

Require Import Coq.Logic.Classical.
Require Import Coq.omega.Omega.

Theorem convergence_t1 :
  forall (f : nat -> nat),
    (forall n n', n <= n' -> f n <= f n') -> (exists l, forall n, f n <= l) ->
    exists N L, forall n, n >= N -> f n = L.
Proof.
  intros f H1 H2.
  destruct H2 as [l H2].
  induction l.
  {
    exists 0; exists 0.
    intros n H3.
    assert (H2' := H2 n).
    destruct (f n); [trivial| inversion H2'].
  }
  {
    destruct (classic (exists n : nat, f n = S l)) as [H3|H3].
    {
      destruct H3 as [m H3].
      exists m; exists (S l).
      intros n H.
      apply H1 in H.
      assert (H2' := H2 n).
      abstract omega.
    }
    {
      apply IHl.
      intros n.
      assert (H2' := H2 n).
      assert (H4 : f n <> S l).
      {
        intros H4.
        apply H3; exists n; trivial.
      }
      abstract omega.
    }
  }
Qed.

Regards,
Amin

> On 13 Feb 2015, at 13:58, Saulo Araujo <saulo2 AT gmail.com> wrote:
>
> Hi,
>
> Does the Coq standard library or any public available library has the proof for the theorem below (or one similar)? It basically says that non decreasing natural number sequences are convergent.
>
> Theorem convergence_t1 :
>   forall (f : nat -> nat),
>     (forall n, f (S n) >= f n /\ exists l, forall n, f n <= l) ->
>     exists N L, forall n, n >= N -> f n = L.
>
> Thanks,
> Saulo