証明方法（forall x、P x / \ Q x）-＆gt; （forall x、P x）[In 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では、まったく同じ問題を解決し、＆quot; cut（P x / \ Q x）＆quot;を使用します。 ＆quot; P x＆quot;から目標を書き換えます＆quot; P x / \ Q x-＆gt; P x＆quot;。そこからいくつかの操作を行うことができ、目標が単に「P x / \ Q x」である場合＆quot; forall x：P x / \ Q x＆quot;を適用できます。残りは簡単です。

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）AND Q（x）が成り立つ場合、すべてのxについてP（x）が成り立ちます。