在 coq 中使用关键字 `exists` 定义答案

【问题标题】：Definition in coq using keyword `exists`在 coq 中使用关键字 `exists` 定义
【发布时间】：2018-11-24 20:36:10
【问题描述】：

我正在尝试使用以下语法定义一个名为 isVector 的实体

Require Export Setoid.
Require Export Coq.Reals.Reals.
Require Export ArithRing.


Definition Point := Type.

Record MassPoint:Type:= cons{number : R ; point: Point}.

Variable add_MP : MassPoint -> MassPoint -> MassPoint . 

Variable mult_MP : R -> MassPoint -> MassPoint .

Variable orthogonalProjection : Point -> Point -> Point -> Point.

Definition isVector (v:MassPoint):= exists A, B :Point , v= add_MP((−1)A)(1B).

Coq IDE 一直抱怨定义存在语法错误。目前，我还没有弄明白。

【问题讨论】：

标签： coq exists definition

【解决方案1】：

这里有很多问题。

首先，你会写：

exists A B : Point, …

不同变量之间没有逗号。

但是，右侧还有语法错误。首先，我不确定那些 1 和 -1 操作是否存在。其次，函数调用会这样写：

add_MP A B

您可以按照自己的方式编写它们：

add_MP(A)(B)

但从长远来看，您可能应该习惯函数调用的语法只是一个空格！您可能需要以公理化其他操作的方式公理化此 -1 操作，除非它们是您在某处定义但未在此处发布的符号。

【讨论】：

【解决方案2】：

感谢您的帮助。稍作试验后。以下是可行的解决方案。

Definition Point:= Type.

Record massPoint: Type := cons{number: R; point: Point}.

Variable add_MP: massPoint -> massPoint -> massPoint.
Variable mult_MP: R        -> massPoint -> massPoint.


Definition tp (p:Point) := cons (-1) p.

Definition isVector(v:massPoint):= exists A B : Point, v = add_MP(cons (-1) A)(cons 1 B).

【讨论】：

很高兴你知道了！