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

Question

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

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

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

似乎您可以将它们合并到一个定义中，所以我想从语法和语义上了解如何在 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 ...

标签： geometrycoqformal-methods

Answer 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.