Как определить аксиому линии как две точки в 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 ...

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.