Logic

Coq 中的逻辑系统。

We have seen many examples of factual claims (propositions) and ways of presenting evidence of their truth (proofs). In particular, we have worked extensively with equality propositions ([e1 = e2]), implications ([P -> Q]) and quantified propositions ([ forall x, P]). In this chapter, we will see how Coq can be used to carry out other familiar forms of logical reasoning.

Typed language: every sensible expression in Coq's world has an associated type.

Proposition: All syntactically well-formed propositions have type [Prop] in Coq, regardless of whether they are true.

First-class entities: propositions can be manipulated in all the same ways as any of the other things in Coq's world.

还有参数化命题，接受一个参数返回一个命题。如：

Definition is_three (n : nat) : Prop :=
  n = 3.
Check is_three : nat -> Prop.

Logical Connectives

Conjunction and ...

Coq vs. Set Theory

见单独文章 Coq vs. Set Theory