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