Создайте новые экземпляры записи, когда тип записи имеет зависимые связующие в Coq - PullRequest
Новая
       10

Создайте новые экземпляры записи, когда тип записи имеет зависимые связующие в Coq

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

Я намеревался создать новый экземпляр вектора типа Vector в следующем коде.Однако изначально тип векторной записи имеет зависимые идентификаторы.Как и второй ident binder' or the second field -- 'proof' was dependent on the first идент-биндер '-' mpOf '.Когда я пытаюсь определить вычитание двух точек массы, я считаю невозможным пройти ядро ​​coq.

Require Export Coq.Reals.Reals.
Open Scope R_scope.

Definition Point:= Type.

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

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

Record Vector : Type := vecCons { mpOf : massPoint ; proof : isVector mpOf}.

Variable sub_MP: massPoint -> massPoint -> massPoint.


Definition point_sub (p1 p2: massPoint):Vector:=
vecCons (sub_MP p1 p2) proof (sub_MP p1 p2). (* errorsome definition*)

Кто-нибудь знает, как определить point_sub?

1 Ответ

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

У вас есть основные проблемы с инстанцированием в отношении того, что является доказательством.Посмотрите, например, этот код и попытайтесь понять, чего вам не хватает: 

Require Import Coq.Reals.Reals.
Open Scope R_scope.

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

Variable add_MP: massPoint -> massPoint -> massPoint.
Variable sub_MP: massPoint -> massPoint -> massPoint.

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

Record Vector : Type := vecCons { mpOf : massPoint; proof : isVector mpOf }.

Definition point_sub (p1 p2: massPoint) : Vector.
Proof.
refine (vecCons (sub_MP p1 p2) _).
repeat eexists.
...