Coqに∀x（P（x）とQ（x））を書くにはどうすればいいですか？

Question

私はCoqを試していますが、私は何をしているのか完全にはわかりません。です：

Theorem new_theorem : forall x, P:Prop /\ Q:Prop 

相当

：

∀x (P(x) and Q(x)) 

編集：私は、彼らがいると思います。

Answer 1

構文に問題がありますか？

$ coqtop 
Welcome to Coq 8.1pl3 (Dec. 2007) 

Coq < Section Test. 

Coq < Variable X:Set. 
X is assumed 

Coq < Variables P Q:X -> Prop. 
P is assumed 
Q is assumed 

Coq < Theorem forall_test: forall x:X, P(x) /\ Q(x). 
1 subgoal 

    X : Set 
    P : X -> Prop 
    Q : X -> Prop 
    ============================ 
    forall x : X, P x /\ Q x 

forall_test < 

Answer 2

さて、あなたの質問に答えるために：

Section test. 

    Variable A : Type.   (* assume some universe A *) 
    Variable P Q : A -> Prop. (* and two predicates over A, P and Q *) 

    Goal forall x, P x /\ Q x. (* Ax, (P(x) and Q(x)) *) 

End test.