How to write coq definitions with "subtypes"

Question

I have the following definition for 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).

What I would like is something like

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

How would I do this?

For context, here is 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)}.

Answer 1

The V parameter can be moved into the body of the record, using the :> syntax to automatically create coercions.

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
}.

Now your second definition works:

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

Another way, preserving parameter V, would be to define Closed_Subspace as follows:

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
}.

And add the necessary coercion manually:

Coercion normed_space : Closed_Subspace >-> Normed_Space.