증명하는 방법 (forall x, P x /\ Q x) -> (forall x, P x) [Coq에서]

Question

Coq에서 (forall x, P x /\ Q x) -> (forall x, P x)를 어떻게 증명합니까?몇 시간 동안 노력했지만 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 레슨에서 그는 똑같은 문제를 해결하고 "p x"에서 "p x / q x-> p x"로 목표를 다시 작성하는 "컷 (p x / q x)을 사용합니다. 거기에서 당신은 약간의 조작을 할 수 있으며 목표가 "p x / q x"일 때 "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)가 유지됩니다.