Stream: Coq users

Topic: Coercion of subspaces

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.?

view this post on Zulip 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.

view this post on Zulip Stéphane Desarzens (Jun 25 2022 at 07:43):

Oh, nice! Thanks for mentioning that @Guillaume Melquiond. It really works now.

Last updated: Jun 25 2024 at 14:01 UTC