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)).
In classical logic,
~(m>n /\ P m)
 <->
~(m > n) \/ ~ P m
<->
m > n -> ~ P m.

not (m >= n).
Kind regards, Jonas
> 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.
>
> I think that asserting that P is decidable may help, so I'm actually trying to
> prove:
> Goal forall (P:nat->Prop), decidable P -> ((~ FinitelyTrue P) ->
> InfinitelyTrue P).
>
> with decidable defined as follow:
> Definition decidable (P:nat->Prop) := forall n:nat, (P n) \/ ~ (P n).
>
> After a few trivial simple steps, I get the following goal:
>
> P : nat -> Prop
> dec : forall n : nat, P n \/ ~ P n
> n : nat
> nft : ~ (forall m : nat, m >= n -> ~ P m)
> ______________________________________(1/1)
> exists m : nat, m > n /\ P m
>
> This looks rather trivial to me. If it is not the case that all m greater than
> n do not have the property, then I can find one that has for which it holds.
> And yet I'm stuck.
>
> N.B. I don't feel very comfortable with respect to the inequalities (strict
> vs. not strict). I have to use le in the definition of FinitelyTrue so as to
> allow properties that are true 0 times. And I have to use lt in the definiton
> of InfinitelyTrue, or the definition won't match its meaning. And yet, nft
> will be true if P n and m=n and ~ P m for all m>n, so there's is something
> wrong here.