如何证明（forall x，P x / \ Q x） - ＆gt; （forall x，P x）[在Coq中]

Question

如何证明（forall x，P x / \ Q x） - ＆gt; （forall x，P x）在Coq？已经尝试了几个小时，无法弄清楚如何将先行者分解为Coq可以消化的东西。 （显然，我是个新手）。

Answer 1

你可以通过应用H来更快地完成它，但是这个脚本 应该更清楚。

Lemma foo : forall (A:Type) (P Q: A-> Prop), (forall x, P x /\ Q x) -> (forall x, P x).
intros.
destruct (H x). 
exact H0.
Qed.

Answer 2

尝试

elim (H x).

Answer 3

实际上，当我发现这个时，我想出了这个：

计算机科学家数学2

在第5课中，他解决了完全相同的问题，并使用“cut（P x / \ Q x）”。从“P x”重写目标到“P x / \ Q x - ＆gt; P x“。从那里你可以做一些操作，当目标只是“P x / \ Q x”时。你可以申请“forall x：P x / \ Q x”其余的很简单。

Answer 4

Assume ForAll x: P(x) /\ Q(x)
   var x; 
      P(x) //because you assumed it earlier
   ForAll x: P(x)
(ForAll x: P(x) /\ Q(x)) => (ForAll x: P(x))

直截了当地，如果对于所有x，P（x）和Q（x）成立，那么对于所有x，P（x）成立。