The Coq mailing list

[Nils Anders Danielsson <nad AT chalmers.se>]

On 2012-11-14 13:15, xavier wrote:
> Here are two basic definitions I have given to myself:
>
> Definition InfinitelyTrue (P:nat->Prop) := forall n:nat, exists m:nat, (m>n /\
> P(m)).
> Definition FinitelyTrue (P:nat->Prop) := exists n:nat, forall m:nat, (m>=n ->
> ~ P(m)).
>
> The first definition says that the predicate P is true for infinitely many
> integers. The way of specifying this is asserting that for any integers,
> there's a greater one that has the property.
>
> The second one says the opposite, namely that for some integer, all bigger
> ones do not have the property.
>
> I'm trying to prove that one is equivalent to the opposite of the other.

With similar definitions of InfinitelyTrue and FinitelyTrue we have

  ∀ P → ¬ (FinitelyTrue P) → ¬ ¬ (InfinitelyTrue P)

/iff/ we have the double-negation shift property

  ∀ P → DNS P,

where

  DNS P = (∀ i → ¬ ¬ P i) → ¬ ¬ (∀ i → P i).

I assume that this double-negation shift property cannot be proved in
Coq.

See NonConstructive.equivalent in the following code listing:

  http://www.cse.chalmers.se/~nad/listings/codata/InfinitelyOften.html

(The proof is due to Thierry Coquand and me.)

--
/NAD