Comment écrire des définitions avec « coq sous-types »

Question

je la définition suivante pour 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). 

Ce que je voudrais est quelque chose comme

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

Comment puis-je faire cela?

Pour le contexte, voici 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

Le paramètre V peut être déplacé dans le corps de la fiche, en utilisant la syntaxe :> pour créer automatiquement 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 
}. 

Maintenant votre deuxième marche définition:

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

Une autre façon, paramètre préserver V, serait de définir Closed_Subspace comme suit:

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

Et ajouter la contrainte nécessaire manuellement:

Coercion normed_space : Closed_Subspace >-> Normed_Space.