I have found it quite difficult to work with goals of the form
{forall _, _} + { not (forall _, _) }
Consider this for a minimal example:
Inductive X := a | b.
Proposition X_q_dec :
forall P : X -> Prop,
(forall x, { P x } + { not (P x) }) ->
{ forall x, P x } + { not (forall x, P x) }.
Proof.
intros.
pose proof H a as Ha.
pose proof H b as Hb.
destruct Ha, Hb.
left; destruct x; assumption.
all: right; intro C; auto.
Qed.
Since X has a finite number of elements, there is a finite number of decidable predicates on it. Thus in this proof I just look over all of them and prove the correct side of sumbool for each one.
However, in the more general case, I cannot move the goal at all:
Proposition nat_q_dec :
forall P : nat -> Prop,
(forall n, { P n } + { not (P n) }) ->
{ forall n, P n } + { not (forall n : nat, P n) }.
My gut feeling is that this should be undecidable: there is no algorithm with a finite upper boundary on operations required to determine whether or not P holds on all n : nat. The same, it seems, should apply to any other type with an infinite number of elements (i.e. not just nat). Unfortunately, my theoretical background falls short to provide a rigorous argument about this.
Is my feeling correct?
If so, why exactly?
If not, how should I go about proving such a goal in Coq?
Yes, you are right, and the argument is pretty much what you laid out. Suppose that P t n means that "the lambda term t can be normalized using at most n reduction steps". Then ~ P t n should be decidable for every n, but it is not the case that we can decide forall n, ~ P t n, since this would imply solving the halting problem.