Coq：关于一组内容的命题

Question

我刚开始使用Coq。

我该如何定义命题myProp这样给定一个集合H,myProp H是真的iff ？

特别是，我该如何表达一个事实：H是nat的子集？或者我怎么能简单地说让H是nat的一个子集？

Answer 1

你是在类型理论中，所以子集的概念并不完全以集合论的方式存在于 中。

将某些事物描述为nat的子集只是通过将其描述为自然数的命题来完成的。某种类型的nat -> Prop。

句子让H是NAT一个子集写的是：

Variable H : nat -> Prop. 

现在对自然数谓语只能应用于自然数。

如果你想有一致性和谈论自然数的全部子集，它是由（随机选择的名称）

Definition all_nat n := True. 

将注意力转向你的myProp谓语表示的，它只会被应用关于自然数的谓词，所以你可以删除有关作为nat子集的部分，这将始终得到满足。

Definition myProp (H : nat -> Prop) := forall x, H (2 * x) -> H x. 

如果我真的想有以下的初步建议的说明，我会写

Definition myProp' (H : nat -> Prop) := 
    (forall x, H x -> all_nat x) /\ 
    (forall x, H (2 * x) -> H x). 

但相合的第一部分是在all_nat的情况下，真没用。在其他情况下，您可能想要考虑另一个有意义的nat子集的所有子集。