Stéphane Desarzens (Jun 25 2022 at 07:13): Stéphane Desarzens (Jun 25 2022 at 07:13):I'd like to declare a coercion, but don't know how to formulate it to coq. My situation is this:
Definition Ensemble (X : Type) := X -> Prop.
Definition In {X : Type} (U : Ensemble X) (x : X) := U x.
Record TopologicalSpace := {
point_set :> Type;
}.
Definition SubspaceTopology {X : TopologicalSpace} (U : Ensemble X) :=
{| point_set := { x : X | In U x }; |}.
Axiom connected : TopologicalSpace -> Prop.
Now I'd like to write the following:
Coercion SubspaceTopology : Ensemble >-> TopologicalSpace.
Section S.
Variable X : TopologicalSpace.
Variable U : Ensemble X.
Fail Variable V : Ensemble U.
Fail Variable p : U. (* should be interpreted as [p : { x : point_set X | In U x }] *)
Fail Variable f : U -> X.
Fail Goal connected U. (* should be interpreted as [connected (SubspaceTopology U)] *)
End Section S.
Is there some way to make this work?
Guillaume Melquiond (Jun 25 2022 at 07:31):Your coercion does not respect the uniform inheritance. For some obscure reason, Coq is extremely crippled in that case, and meaningful examples like yours fail. This restriction was removed in Coq 8.16 and most of (all?) your examples should go through. But with 8.15 or earlier, I cannot think of a good way to make it succeed.
Michael Soegtrop (Jun 25 2022 at 07:33):Maybe it helps you to know that coercions don't do any unification - the involved types must match literally without any reduction.
Your intuition around U and V is not clear to me. Did you mean Definition U := Ensemble X.?
Stéphane Desarzens (Jun 25 2022 at 07:34):I wanted U to be a subset of X and simultaneously consider it as a space endowed with the subspace topology.
Stéphane Desarzens (Jun 25 2022 at 07:43):Oh, nice! Thanks for mentioning that @Guillaume Melquiond. It really works now.
Last updated: Sep 30 2023 at 05:01 UTC