Stream: Coq users

Topic: `:> forall {P}, ...`


view this post on Zulip James Wood (Mar 22 2022 at 10:59):

I can't find much documentation on :>. It appears to be being ignored in the following example. Is there a way to work around that (while preserving the dependency on the first field)?

Record foo (n : nat) := {
  foof : nat;
}.
Record bar := {
  x : nat;
  barf :> foo x;
}.

Lemma quux (b : bar) : unit.
Fail Check b.(foof).

view this post on Zulip Paolo Giarrusso (Mar 22 2022 at 11:02):

:> is a shortcut for Coercion, but that's not the problem AFAICT:

Fail Check b.(foof).
Arguments foof {_}.
Check b.(foof).

view this post on Zulip Paolo Giarrusso (Mar 22 2022 at 11:03):

I don't know if the error message is any good, but it's very good for Coq:

Projection foof expected 1 explicit parameter.

view this post on Zulip Paolo Giarrusso (Mar 22 2022 at 11:05):

Basically, foof takes n as an explicit argument by default, so you need to fix that by hand.

Fail Check b.(foof).
About foof.
(* foof : forall n : nat, foo n -> nat [...] *)
Arguments foof {_}.
About foof.
(* foof : forall {n : nat}, foo n -> nat *)

view this post on Zulip Paolo Giarrusso (Mar 22 2022 at 11:06):

I _think_ Agda would be smarter here, but Coq seems like it got implicit arguments late, so you often must ask for them explicitly.

view this post on Zulip James Wood (Mar 22 2022 at 11:06):

Ah, yes, I forgot about this when constructing my minimal example. Hmm, I wonder how it applies to my actual code...

view this post on Zulip Paolo Giarrusso (Mar 22 2022 at 11:07):

Honestly I expected you'd be running into uniform inheritance...

view this post on Zulip James Wood (Mar 22 2022 at 11:08):

What's that?

view this post on Zulip Paolo Giarrusso (Mar 22 2022 at 11:10):

It's described in https://coq.inria.fr/refman/addendum/implicit-coercions.html, but since you didn't find docs on :>, let me desugar that for you. Your minimized Record bar is equivalent to:

Record bar := {
  x : nat;
  barf : foo x;
}.
Coercion barf : bar >-> foo.

view this post on Zulip Paolo Giarrusso (Mar 22 2022 at 11:11):

But "uniform inheritance" is a bit tricky and doesn't apply here, so maybe try minimizing again before reading up on it? That page does have a formal description for it, but it's not immediate...

view this post on Zulip Paolo Giarrusso (Mar 22 2022 at 11:12):

Another thing to remember: coercions always consider _syntactic_ equality, not _definitional_ equality.

view this post on Zulip Paolo Giarrusso (Mar 22 2022 at 11:14):

I'll retract the last for now: I've seen lots of evidence for it, but I can't reproduce it now for some reason — either I need another example or something changed...

view this post on Zulip James Wood (Mar 22 2022 at 11:28):

Maybe it is the uniform inheritance condition:

Record foo {P : nat -> Type} {x : nat} := {
  foof : P x;
}.
Arguments foo N x : clear implicits.
Record bar := {
  n : nat;
  barf :> forall {P}, foo P n;
}.

Lemma quux (M : bar) : unit.
Check barf M.
Fail Check foof M.

view this post on Zulip Pierre Roux (Mar 22 2022 at 11:34):

Paolo Giarrusso said:

Honestly I expected you'd be running into uniform inheritance...

Note that this constraint will be mostly alleviated in next release: https://github.com/coq/coq/pull/15789

view this post on Zulip James Wood (Mar 22 2022 at 11:35):

Paolo Giarrusso said:

I _think_ Agda would be smarter here, but Coq seems like it got implicit arguments late, so you often must ask for them explicitly.

Incidentally, Agda doesn't do anything smart, as such – type parameters are always implicit for constructors and field accessors. That's the correct approach whenever you can rely on them being checked bidirectionally, but my experience is that that's not the case in Coq.

view this post on Zulip Ali Caglayan (Mar 22 2022 at 11:41):

For your first one you want Check b.(foof _).

view this post on Zulip Ali Caglayan (Mar 22 2022 at 11:42):

The parameter n is part of the projection so you need to include it

view this post on Zulip James Wood (Mar 22 2022 at 13:41):

In case it got lost, the problematic field declaration is:

  barf :> forall {P}, foo P n;

view this post on Zulip Ali Caglayan (Mar 22 2022 at 13:49):

That looks like a coercion to funclass to me

view this post on Zulip Ali Caglayan (Mar 22 2022 at 13:55):

One way to get the coercion to accept P as a parameter is to use a section

view this post on Zulip Ali Caglayan (Mar 22 2022 at 13:55):

Section Assumptions.
Context (P : nat -> Type).

Record foo {x : nat} := {
  foof : P x;
}.

Record bar := {
  n : nat;
  barf :> @foo n;
}.
(* Coercion barf : bar >-> foo. *)

Print Graph.

Lemma quux (M : bar) : unit.
Check barf M.
Check foof M.
Abort.

End Assumptions.

view this post on Zulip Ali Caglayan (Mar 22 2022 at 13:55):

Otherwise barf always detects funclass as the target class

view this post on Zulip James Wood (Mar 22 2022 at 14:00):

Do I then have to give P to use the field n?

view this post on Zulip Ali Caglayan (Mar 22 2022 at 14:01):

Looks that way

view this post on Zulip Ali Caglayan (Mar 22 2022 at 14:02):

@Pierre Roux do you know how to get the coercion to recognize foo as the target and not funclass?

view this post on Zulip James Wood (Mar 22 2022 at 14:04):

Thanks for the suggestion, but it would be unacceptable (or at least, less acceptable than explicit projections) in my case.


Last updated: Feb 04 2023 at 21:02 UTC