如何在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.