如何在 Coq 中将直线公理定义为两点

Posted 2023-03-28

【中文标题】如何在 Coq 中将直线公理定义为两点

【英文标题】：How to define axiom of a line as two points in Coq

【发布时间】：2019-03-01 04:31:22

【问题描述】：

我试图在Coq 中找到一个示例 axiom，类似于几何中的直线公理：如果给定两点，则这两点之间存在一条线。我想看看如何在 Coq 中定义它。固有地选择这个简单的直线公理来查看非常原始的东西是如何定义的，因为我很难在自然语言之外定义它。

具体来说，我已经看到了这两个公理，想知道在 Coq 中如何定义这两个公理：

任何两个不同的点总是确定一条线 一条线的任意两个不同点唯一确定这条线

似乎您可以将它们合并到一个定义中，所以我想从语法和语义上了解如何在 Coq 中编写它。

我真的不知道如何编写 Coq，只是想看看他们是如何做到的。但如果我要尝试，它似乎是这样的：

Axiom line : forall ptA:Point ptB:Point, line ptA ptB.

但这需要一个 Line 和一个 Point 对象。

Axiom line : forall ptA ptB, line ptA ptB.
Definition Line ptA ptB -> (...) No idea.
Definition Point ...

【问题讨论】：

github.com/coq-contribs/euclidean-geometry 中有一个（也许是旧的）欧几里得几何公理化。它显示了 一种 方法，还有其他方法。它非常大，可能比您要求的要多。

【参考方案1】：

这是一种可能性。 exists! 连接词意味着独特的存在。

Axiom point : Type.
Axiom line  : Type.
Axiom lies_in : point -> line -> Prop.
Axiom ax : forall (p1 p2 : point), p1 <> p2 ->
           exists! l : line, lies_in p1 l /\ lies_in p2 l.

【讨论】：

想知道你是否可以自然语言化Axiom lies_in : point -> line -> Prop.，对我来说它说“如果一个点那么一条线就是一个命题”，但我真的不明白这意味着什么或我如何我会自己解决的。不过，我了解了其他公理的要点。

Prop 是命题的类型。 point -> line -> Prop 的元素是一个有两个参数的函数，它将 point 和 line 映射到一个命题。换句话说，它是点和线之间的关系。在这种情况下，预期的解读是 lies_in p l 断言点 p 位于 l 行中。

为了更好的可读性，我建议使用Parameter 来介绍point、line 和lies_in，并且仅在陈述命题时使用Axiom，这里是@ 987654336@.