The Coq mailing list

[Jonas Oberhauser <s9joober AT gmail.com>]

Am 14.11.2012 13:15, schrieb xavier:
> 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.
>
> The first direction is easy and the proof need not be told.
> Goal forall (P:nat->Prop), InfinitelyTrue P -> ~ FinitelyTrue P.
>
> But I'm stuck on the other direction:
> Goal forall (P:nat->Prop), (~ FinitelyTrue P) -> InfinitelyTrue P.

This is good. If you could prove this, we would have excluded middle.

Goal (forall (P:nat->Prop),  ~ FinitelyTrue P -> InfinitelyTrue P) -> 
(forall P, ~~P -> P).
intros impl P nnP.
assert (~ FinitelyTrue (fun _ => P)).
  intros [n allp]. apply nnP.
  apply allp with (S n) ; auto.
elim (impl (fun _ => P) H) with 0.
intros _ [_ p] ; auto. Qed.