Определение в coq с использованием ключевого слова `exist` - PullRequest
Новая
       8

Определение в coq с использованием ключевого слова `exist`

0 голосов
/ 24 ноября 2018

Я пытаюсь определить сущность с именем 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 продолжает жаловаться на наличие синтаксической ошибки для определения.Сейчас я этого не понял.

Ответы [ 2 ]

0 голосов
/ 25 ноября 2018

Спасибо за помощь.После экспериментов немного.Ниже приведено решение, которое работает. 

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).
0 голосов
/ 24 ноября 2018

Здесь много проблем.

Сначала вы должны написать: 

exists A B : Point, …

без запятой между различными переменными.

Но затем вы такжеесть синтаксические ошибки на правой стороне.Во-первых, я не уверен, что эти операции 1 и -1 существуют.Во-вторых, вызовы функций будут записываться следующим образом: 

add_MP A B

Вы можете написать их так, как вы делаете: 

add_MP(A)(B)

Но в долгосрочной перспективе вы, вероятно, должны привыкнуть к синтаксисуиз вызовов функций просто пробел!Возможно, вам понадобится аксиоматизировать эту -1 операцию так же, как вы аксиоматизировали другие операции, если только они не являются обозначением, которое вы определили где-то, но не опубликовали здесь.

...