The Coq mailing list

[Amin Timany <amintimany AT gmail.com>]

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