The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Wed, 14 Nov 2012 13:15:17 +0100 (CET),
"xavier" 
<xavierdpt+coq AT gmail.com>
 a écrit :

I think Adam is right:

> 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

Take n=0,

then, you have:

> P : nat -> Prop
> dec : forall n : nat, P n \/ ~ P n
> nft : ~ (forall m : nat, ~ P m)
> ______________________________________(1/1)
> exists m : nat, m > 0 /\ P m

Here, you cannot do induction on anything.

Things would be different if you had Excluded Middle:

> P : nat -> Prop
> dec : forall n : nat, P n \/ ~ P n
> nft : exists m : nat, P m (*using excluded middle*)
> ______________________________________(1/1)
> exists m : nat, m > 0 /\ P m

Although even here, as you said, it is still not provable (change your
inequalities!)

Counter-example:
P:=λ m, match m with O => True | _ => False end
dec:=λ n, match n as n0 return P n0 ∨ ¬ P n0 with O => I | _ => λ x, x
          end
nft := λ H, (H O I)
---------------------
The goal is wrong.