Stream: Coq users

Topic: Chaining a type-level and a term-level coercion


view this post on Zulip Jarl G. Taxerås Flaten (May 10 2021 at 20:00):

I have a pointed type X whose elements are themselves types, giving a function f : pointed_type X -> Type from the underlying type of X. If I make this a coercion, Coq complains about UIC (because pointed_type is not a class?). Now pointed_type is itself already a coercion, so I can write x0 x1 : X. Now I would like to write x0 -> x1 since by virtue of the coercion f, x0 and x1 are types, but this doesn't work. Can this be made to work or is it a dead-end?

Let me add that I know the underlying type of X, let's call it UX. Given x0 and x1 as above, I can write (x0 : UX) -> (x1 : UX) with a coercion UX -> Type (which doesn't complain about UIC). So if I could get pointed_type X to automatically convert to UX that should solve my issues as well. Any input appreciated!

view this post on Zulip Jarl G. Taxerås Flaten (May 10 2021 at 22:09):

Minimal example (take 3):

Notation "A -> B" := (forall (_ : A), B) (at level 99, right associativity, B at level 200).

Record sig {A} (P : A -> Type) := exist {
  proj1 : A ;
  proj2 : P proj1 ;
}.

Arguments exist {A} P _ _.
Notation "( x ; y )" := (exist _ x y).

Record pType := {
  ptype_type :> Type;
  ptype_pt : ptype_type
}.

Axiom P : Type -> Type.
Axiom Px : forall X, P X.

Definition BAut (X : Type) := sig P.
Coercion BAut_pr1 X : BAut X -> Type := fun x => match x with (x;_) => x end.

Definition pBAut (X : Type) : pType
  := Build_pType (BAut X) (X; Px X).

Coercion pBAut_pr1 X : pBAut X -> Type := BAut_pr1 X.

Context (X : Type) (x0 x1 : pBAut X).
Check ((x0 : BAut X) -> (x1 : BAut X)).
Fail Check (x0 -> x1).

view this post on Zulip Ali Caglayan (May 18 2021 at 22:59):

@Gaëtan Gilbert Do you know what would need to change to get the desired behavior here?

view this post on Zulip Gaëtan Gilbert (May 19 2021 at 09:10):

If I make this a coercion, Coq complains about UIC (because pointed_type is not a class?)

because pointed_type is applied to something that's not a variable

view this post on Zulip Jarl G. Taxerås Flaten (May 20 2021 at 12:50):

Is there a way to get the last line Check (x0 -> x1). to work though, or something similar?


Last updated: Oct 13 2024 at 01:02 UTC