証明方法（forall x、P x） - （forall x、P x）

Question

どのようにして証明するか（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

を試してみて、私はこの見つかったとき、私はこの1つを考え出し：レッスン5では

Mathematics for Computer Scientists 2

が、彼は正確に解決を同じ問題があり、 "P x"から "P x/\ Q x - > P x"にゴールを書き換える "cut（P x/\ Q 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)) 

Intuitivlyに、すべてのxに対して、P（x）とQ（x）を保持している場合、すべてのxに対して、P（x）が成立します。