如何在 Coq 中将一条线的公理定义为两点

Question

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

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

Any two distinct points always determine a line

Any two distinct points of a line determine this line uniquely

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

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

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

但这需要一条线和一个点对象。

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

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.

如何在 Coq 中将一条线的公理定义为两点

How to define axiom of a line as two points in Coq

geometry

formal-methods

coq