Coq - 假设中的通用量词

Question

我想证明以下定理

Goal (forall x, P x \/ Q x) -> (forall x, P x) \/ (forall x, Q x).

有上下文

1 subgoal
P : nat -> Prop
Q : nat -> Prop
R : nat -> nat -> Prop
H : forall x : nat, P x \/ Q x
______________________________________(1/1)
(forall x : nat, P x) \/ (forall x : nat, Q x)

该陈述在谓词逻辑中似乎是正确的，但我不知道如何证明它。问题本质上是我不能一次消除所有的forall，但我不能在破坏hypotesis H之前既不左也不右应用。

有没有一种简单的方法可以做到这一点？

Answer 1

以P 为偶数，Q 为奇数，你应该看到你的定理有缺陷。