James Wood (Mar 22 2022 at 10:59): 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).
:> is a shortcut for Coercion, but that's not the problem AFAICT:
Fail Check b.(foof).
Arguments foof {_}.
Check b.(foof).
I don't know if the error message is any good, but it's very good for Coq:
Projection foof expected 1 explicit parameter.
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 *)
I _think_ Agda would be smarter here, but Coq seems like it got implicit arguments late, so you often must ask for them explicitly.
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...
Paolo Giarrusso (Mar 22 2022 at 11:07):Honestly I expected you'd be running into uniform inheritance...
James Wood (Mar 22 2022 at 11:08):What's that?
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.
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...
Paolo Giarrusso (Mar 22 2022 at 11:12):Another thing to remember: coercions always consider _syntactic_ equality, not _definitional_ equality.
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...
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.
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
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.
Ali Caglayan (Mar 22 2022 at 11:41):For your first one you want Check b.(foof _).
Ali Caglayan (Mar 22 2022 at 11:42):The parameter n is part of the projection so you need to include it
James Wood (Mar 22 2022 at 13:41):In case it got lost, the problematic field declaration is:
barf :> forall {P}, foo P n;
That looks like a coercion to funclass to me
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
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.
Otherwise barf always detects funclass as the target class
James Wood (Mar 22 2022 at 14:00):Do I then have to give P to use the field n?
Ali Caglayan (Mar 22 2022 at 14:01):Looks that way
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?
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: Apr 20 2024 at 08:02 UTC