Wie schreibe ich ∀x (P (x) und Q (x)) in Coq?

Question

Ich versuche Coq, aber ich bin mir nicht ganz sicher, was ich mache. Ist:

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

Entspricht:

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

Edit: Ich denke, sie sind.

Answer 1

Haben Sie Probleme mit der Syntax?

$ 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

Nun, Ihre Frage zu beantworten:

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.