Как написать Coq определения с «подтипов»

Question

У меня есть следующее определение 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)}. 

Answer 1

Параметр 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.