如何证明(对于所有x,p x/\q x)->(对于所有x,p x)【在coq中】

只需应用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.

尝试

elim (H x).

事实上,当我发现这个的时候我发现了这个:

Mathematics for Computer Scientists 2

在第5课中,他解决了完全相同的问题,并使用“cut(p x/\q x)”,将目标从“p x”重新写入“p x/\q x->p x”。从那里你可以做一些操作,当目标仅仅是“p x/\q x”时,你可以应用“for all x:p x/\q x”,剩下的就很简单了。

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)保持不变。