The Coq mailing list

[Daniel de Rauglaudre <daniel.de_rauglaudre AT inria.fr>]

On Thu, Sep 18, 2014 at 02:05:49PM +0200, Alan Schmitt wrote:

> > 5/ ∀ P : nat → Prop, { ∃ n, P n } + { ∀ n, ¬P n }.
> 
> Isn't it too strong? If I take "P k" to be "function F terminate when
> given input k", doesn't this mean you can decide termination?

Yes, it is too strong. Actually, I apply it only in file Puiseux.v line 235:
   destruct (exists_or_not_forall (multiplicity_decreases pol ns)) as ...

And 'multiplicity_decreases' is defined on this file, lines 47-54:
   Definition multiplicity_decreases pol ns n :=
     let c := ac_root (Φq pol ns) in
     let r := root_multiplicity acf c (Φq pol ns) in
     let poln := nth_pol n pol ns in
     let nsn := nth_ns n pol ns in
     let cn := nth_c n pol ns in
     let rn := root_multiplicity acf cn (Φq poln nsn) in
     (rn < r)%nat.

It says that some sequence of 'r' (of the pen-and-paper proof), which
is non-increasing, has a rank 'n' where it strictly decreases. This
property is true or false, and if it is false, it takes an infinite
amout of time to answer, so it is not programmable. Hence the axiom.

Well, I could change that in the source, this is easy.

-- 
Daniel de Rauglaudre
http://pauillac.inria.fr/~ddr/