Stream: Coq users

Topic: Coercion to Type


view this post on Zulip Jordan Mitchell Barrett (Apr 02 2021 at 06:33):

Why does Coq reject the following?

Inductive metricspace :=
| met (X:Type)(d: X -> X -> R)`{is_metric d}.

Definition MStoT (M:metricspace) :=
  match M with
  | met X d => X
  end.
Coercion MStoT : metricspace >-> Type.
Syntax error: [class_rawexpr] expected after '>->' (in [gallina_ext]).

view this post on Zulip Guillaume Melquiond (Apr 02 2021 at 06:40):

As the message says, Type is not a class. Try with, e.g., Sortclass instead.

view this post on Zulip Jordan Mitchell Barrett (Apr 02 2021 at 06:43):

What is Sortclass and how is it different to Type?

view this post on Zulip Guillaume Melquiond (Apr 02 2021 at 06:43):

Sortclass is a class and Type is a type.

view this post on Zulip Cyril Cohen (Apr 02 2021 at 07:34):

@Jordan Mitchell Barrett here is the relevant section of the coq documentation https://coq.inria.fr/refman/addendum/implicit-coercions.html#classes

view this post on Zulip Jordan Mitchell Barrett (Apr 02 2021 at 09:56):

Thanks @Guillaume Melquiond and @Cyril Cohen. Speaking of coercions, is it possible to make proj1_sig a coercion for any A : Type, P : A -> Prop? I tried

Coercion sig1co {A : Type}{P : A -> Prop}(y:{x : A | P x}) := proj1_sig y.

but Coq didn't like it.

view this post on Zulip Matthieu Sozeau (Apr 02 2021 at 10:31):

The coercion system does not accept such "generic" coercions, but if you use Program it implements this coercion (and the converse, generating a proof obligation when you implicitely inject in a subset type). Be sure to Unset Program Cases so that your matches and lets don't get interpreted by program unless you really want to https://coq.inria.fr/refman/addendum/program.html?highlight=program#coq:flag.Program-Cases


Last updated: Mar 28 2024 at 14:01 UTC