predicate - Coq を使用した述語ロジックの証明 - 初級構文

Question

Coqで次のことを証明しようとしています:

目標 (forall x:X, P(x) /\ Q(x)) -> ((forall x:X, P (x)) /\ (forall x:X, Q (x)))。

誰か助けてくれませんか？分割するかどうか、仮定などを行うかどうかはわかりません。

完全な初心者で申し訳ありません

Answer 1

Goal forall (X : Type) (P Q : X->Prop), 
    (forall x : X, P x /\ Q x) -> (forall x : X, P x) /\ (forall x : X, Q x).
Proof.
  intros X P Q H; split; intro x; apply (H x).
Qed.

Answer 2

いくつかのヒント: イントロを使用して仮説に名前を付け、目的を分離するために分割し、証明用語 (proj1 または proj2 を含む場合があります) を提供するために正確を使用することをお勧めします。