Как написать определения coq с подтипами

У меня есть следующее определение для closed_subspace_equiv

Record Closed_Subspace (V:Normed_Space) := {
closed_subspace  :> V -> Prop;
addition_closure : forall (x y:V),(closed_subspace x) -> (closed_subspace y) -> (closed_subspace (add V x y));
smul_closure     : forall (x:V) (a:R),(closed_subspace x) -> (closed_subspace (scalar_mul V a x));
subspace_closure : forall (x:V), closure (closed_subspace) x <-> closed_subspace x}.

Definition closed_subspace_equiv {V : Normed_Space} (U:Closed_Subspace V) (x y:V) (p:U x)(q:U y) := exists z:V,(add V x z = y) /\ (U z).

Я хотел бы что-то вроде

Definition closed_subspace_equiv {V : Normed_Space} (U:Closed_Subspace V) (x y:U) := exists z:U,(add V x z = y).

Как бы я это сделал?

Для контекста, вот Normed_Space.

Record Normed_Space : Type := mknormspace
{Vspace     :> Type;
 add        : Vspace -> Vspace -> Vspace;
 neg        : Vspace -> Vspace;
 scalar_mul : R -> Vspace -> Vspace;
 zero       : Vspace;
 norm       : Vspace -> R;
 add_assoc  : forall x y z:Vspace, add x (add y z) = add (add x y) z;
 add_comm   : forall x y:Vspace, add x y = add y x;
 add_inv    : forall x:Vspace, add x (neg x) = zero;
 add_id     : forall x:Vspace, add x zero = x;
 mul_assoc  : forall (x:Vspace) (a b:R), scalar_mul a (scalar_mul b x) = scalar_mul (a*b) x;
 mul_id     : forall x:Vspace, scalar_mul 1 x = x;
 mul_dist1  : forall (x:Vspace) (a b:R), scalar_mul (a+b) x = add (scalar_mul a x) (scalar_mul b x);
 mul_dist2  : forall (x y:Vspace) (a:R), scalar_mul a (add x y) = add (scalar_mul a x) (scalar_mul a y);
 norm_pos   : forall x:Vspace, (x=zero) \/ (norm x > 0);
 norm_multi : forall (x:Vspace) (a:R), norm (scalar_mul a x) = (Rabs a)*(norm x)}.

dependent-type coq
person davik    schedule 21.12.2016    source источник
comment
Код не скомпилируется — отсутствует определение closure.   -  person Anton Trunov    schedule 22.12.2016

Ответы (1)


arrow_upward
2
arrow_downward

Параметр V можно переместить в тело записи, используя синтаксис :> для автоматического создания приведения.

Record Closed_Subspace := {
  normed_space :> Normed_Space;
  closed_subspace  :> normed_space -> Prop;
  addition_closure : forall x y:normed_space, closed_subspace x -> closed_subspace y -> closed_subspace (add normed_space x y);
  smul_closure     : forall (x:normed_space) (a:R), closed_subspace x -> closed_subspace (scalar_mul normed_space a x);
  subspace_closure : forall x:normed_space, closure (closed_subspace) x <-> closed_subspace x
}.

Теперь ваше второе определение работает:

Definition closed_subspace_equiv (U:Closed_Subspace) (x y:U) :=
  exists z:U, add _ x z = y.

Другой способ сохранить параметр V состоит в том, чтобы определить Closed_Subspace следующим образом:

Record Closed_Subspace (V:Normed_Space) : Type := {
  normed_space := V;
  closed_subspace  :> V -> Prop;
  addition_closure : forall x y:V, closed_subspace x -> closed_subspace y -> closed_subspace (add V x y);
  smul_closure     : forall (x:V) (a:R), closed_subspace x -> closed_subspace (scalar_mul V a x);
  subspace_closure : forall (x:V), closure (closed_subspace) x <-> closed_subspace x
}.

И добавляем необходимое приведение вручную:

Coercion normed_space : Closed_Subspace >-> Normed_Space.
person Anton Trunov    schedule 22.12.2016
comment
Возможно ли иметь V выше (в качестве параметра), т.е. иметь Closed_Subspace V быть типом и по-прежнему иметь возможность делать (U:Closed_Subspace V) (a:U)? - person davik; 22.12.2016
comment
@davik Ты знаешь, что V это не тип, это запись, верно? Чтобы увидеть, что происходит под капотом, вы можете Set Printing Coercions. и посмотреть определение closed_subspace_equiv с помощью Print closed_subspace_equiv. - person Anton Trunov; 22.12.2016
comment
Но разве Vspace :› Type не превращает его в тип? Я сделал печатную вещь, и я не уверен, что я должен заметить. Я новичок в coq, так что терпите меня. - person davik; 22.12.2016
comment
Будет ли что-то подобное работать для вас? Record Closed_Subspace (V:Normed_Space) : Type := { normed_space := V; ...}., после этого добавить Coercion normed_space : Closed_Subspace >-> Normed_Space. - person Anton Trunov; 23.12.2016
comment
Я думаю, это работает, да. Спасибо! Если вы добавите это к своему ответу, я приму его. - person davik; 23.12.2016
comment
На самом деле извините, я только что нашел проблему, я хотел бы, чтобы x:U был s.t. x:V с доказательством closed_subspace x, в противном случае я думаю, что все в V делается элементом V, но мне нужно быть более строгим. - person davik; 23.12.2016