Coq：关于集合内容的命题

Coq: Proposition about the contents of a set

我刚开始使用 Coq。

如何定义命题 myProp，使得给定集合 H，myProp H 为真当且仅当 ?

特别是，我如何在命题中表达 H 是 nat 的子集这一事实？或者我如何简单地声明 让 H 成为 nat?

的子集

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

将某物描述为 nat 的子集只需将其描述为自然数上的命题即可。 nat -> Prop.

类型的东西

句子let H be a subset of 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.

的另一个有意义子集的所有子集的其他情况下，它可能会派上用场。