Coq:关于集合内容的命题

Question

我刚开始使用 Coq。

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

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

Answer 1

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

将某物描述为 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 的另一个有意义子集的所有子集的其他情况下，它可能会派上用场。