Мне было довольно сложно работать с целями вида
{forall _, _} + { not (forall _, _) }
Рассмотрим это для минимального примера:
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.
С X имеет конечное количество элементов, на нем есть конечное число разрешимых предикатов. Таким образом, в этом доказательстве я просто просматриваю их все и доказываю правильную сторону сумбула для каждого.
Однако в более общем случае я вообще не могу сдвинуть цель :
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) }.
Мне кажется, что это должно быть неразрешимым: не существует алгоритма с конечной верхней границей для операций, необходимых для определения того, выполняется ли P для всех n : nat. Похоже, то же самое следует применять к любому другому типу с бесконечным числом элементов (т.е. не только nat). К сожалению, мои теоретические знания не дают точных аргументов по этому поводу.
Правильно ли мое чувство?
Если да, то почему именно?
Если нет, то как мне это сделать? пойти доказать такую цель в Coq?