如何在Coq中将线的公理定义为两个点 [英] How to define axiom of a line as two points in Coq

问题描述

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

I am trying to find an example axiom in Coq of something like the line axiom in geometry: If given two points, there exist a line between those two points. I would like to see how this could be defined in Coq. Inherently choosing this simple line axiom to see how something very primitive is defined, because I'm having a hard time defining it outside natural language.

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

Specifically, I have seen these two axioms and would like to know how in Coq to define both:

1. 任何两个不同的点总是确定a线


2. 线的任何两个不同点唯一地确定该线

几乎可以将它们合并为一个定义，所以我想在语法和语义上看一下如何在Coq中编写此代码。

It almost seems like you can merge them into one definition, so I would like to see syntactically and semantically how to write this in Coq.

我不只是想看看他们是怎么写的，还不知道该怎么写。但是，如果我尝试这样做，就好像是这样：

I don't know how to write Coq really, just looking to see how they do it. But if I were to try it seems like this:

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

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

But that needs a Line and a Point object.

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

推荐答案

一个潜在可能。 存在！结语表示唯一的存在。

Here is a possibility. The exists! connective means unique existence.

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中将线的公理定义为两个点的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！