Stream: Coq users

Topic: Identity Coercions


view this post on Zulip Pierre Roux (Feb 24 2022 at 07:59):

I'm trying to understand that paragraph of the refman: https://coq.inria.fr/refman/addendum/implicit-coercions.html#identity-coercions
I think the following setting fits in the use case in the text (with k = 2, n = 3 and m = 2):

Parameters (C : nat -> unit -> bool -> Set) (D : nat -> unit -> Set).

Parameter f : forall (x1 : nat) (x2 : unit) (y : C x1 x2 true), D x1 x2.

indeed, f doesn't satisfy the uniform inheritance condition, which Coq appropriately warns about

Parameter c : C 0 tt true.  (* a C, for testing purpose *)
Parameter T : D 0 tt -> nat.  (* something expecting a D *)

(* Coercion f : C >-> D. *)
(* as expected *)
(* Warning: f does not respect the uniform inheritance condition *)

and the coercion doesn't work (as expected)

(* Fail Check T c.  (* and coercion doesn't apply *) *)

So following the documentation, we declare an identity coercion

Definition C' := fun (x1 : nat) (x2 : unit) => C x1 x2 true.  (* as in the doc *)
Identity Coercion Id_C'_C : C' >-> C.
Print Id_C'_C.  (* as in the doc *)

I would then expect the following to work

Coercion f : C' >-> D.  (* Cannot recognize C' as a source class of f. *)

according to the following sentence in the doc "We can now declare f as coercion from C' to D"

There is an example below in the doc, but it seems reverse to me: it first declares a coercion then an identity coercion. The identity coercion seems useless (commenting it, the example still works the same).

I'm willing to submit a PR to either improve the refman (or the code), but I first need to understand what is the expected behavior.

view this post on Zulip Enrico Tassi (Feb 24 2022 at 10:08):

I would expect it to work, so maybe its a bug. But I'm not a big fan about identity coercions and the non uniform inheritance condition, so if you have energy to work on that code I'd not stop at the bugfix ;-)

The condition has some sense if the coercions describe a hierarchy, @Kazuhiko Sakaguchi can confirm this.
But I bet that the condition was originally put so that the application of coercions does not require type inference.
In particular from an expected type C1 x1 .. xnit lets you fill the _i in the casted term f _1 .. _n t with x1 .. xn. If you don't have the condition, then you could still typecheck the term and infer the missing pieces.

This code is somehow already there since Program uses existsT as a coercion, (you want to map, say, a n:nat to a {n:nat & n > 0}. You can't possibly infer the _ there (the proof of positivity) from the "arguments of the type", but you can elaborate the _ to a new subgoal.

If you use that code I really don't see why one would need identity coercions, which are a poor may way of describing how to synthesize _1 .. _m out of x1 .. xn. The system is already able to figure out silly cases (in your case the true is in the type of c, the casted term) and even let you do interactive (or via TC search) the non trivial ones.

view this post on Zulip Pierre Roux (Feb 24 2022 at 11:06):

Thanks for your opinion. I fully agree and I'll try to prepare a PR along those lines (there may be some work, the fact that existsT seems to be handled in a quite ad-hoc way is a bit frightening: https://github.com/coq/coq/blob/master/pretyping/coercion.mli#L39 ).

view this post on Zulip Enrico Tassi (Feb 24 2022 at 12:13):

I was thinking about the other way around. The one you point to is also ad-hoc because it cannot just be expressed with coercions since the target would be a parameter, not a constant (from sigT A P >-> A)

view this post on Zulip Enrico Tassi (Feb 24 2022 at 12:14):

I was talking abut the other direction

view this post on Zulip Enrico Tassi (Feb 24 2022 at 12:15):

Anyway, I was just writing here what I would do if I had the time ;-)

view this post on Zulip Paolo Giarrusso (Feb 24 2022 at 13:54):

according to the following sentence in the doc "We can now declare f as coercion from C' to D"

IME, as a rule of thumb, coercions ignore definitional equality entirely, so instead of

Parameter f : forall (x1 : nat) (x2 : unit) (y : C x1 x2 true), D x1 x2.

you'll probably need

Parameter f : forall (x1 : nat) (x2 : unit) (y : C' x1 x2), D x1 x2.

view this post on Zulip Paolo Giarrusso (Feb 24 2022 at 13:56):

but (while Enrico knows more than me) I don't get how this should work as-is: to coerce from C to D you'll need a coercion from C to C' and one from C' to D — so Id_C'_C is backwards.

view this post on Zulip Paolo Giarrusso (Feb 24 2022 at 13:57):

I think SubClass C' := fun (x1 : nat) (x2 : unit) => C x1 x2 true should produce the right direction (it's a definition + identity coercion)

view this post on Zulip Pierre Roux (Mar 11 2022 at 13:28):

@Enrico Tassi here is the PR: https://github.com/coq/coq/pull/15789 . CI seem impressively happy (appart from one stupid conflict made apparent in math-comp and another simple fix in Unimath)
@Kazuhiko Sakaguchi you may also be interested

view this post on Zulip Ana de Almeida Borges (Mar 22 2022 at 14:00):

https://github.com/coq/coq/pull/15789

This is pretty cool! Does it mean the uniform inheritance condition is now irrelevant in all contexts? I still get warned about it (in the definition of onat_of_obool below), even though the following works on master and the last line fails on 8.15:

Coercion nat_of_bool (b : bool) := if b then 1 else 0.

Check (true : nat).

Coercion onat_of_obool (x : option bool) :=
  match x with
  | Some b => Some (nat_of_bool b)
  | None => None
  end.

Check (Some true : option nat).

view this post on Zulip Pierre Roux (Mar 22 2022 at 14:04):

We kept the warning because, as indicated in the doc, uniform inheritance condition still guarantees completeness of the non-ambiguous-coercion-paths check. So it is still advisable to satisfy the condition if possible, in order to avoid spurious warnings about ambiguous paths.

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

The difference now being the coercion is actually still added rather than silently dropped?

view this post on Zulip Pierre Roux (Mar 22 2022 at 14:05):

Exactly (I still think what is now a warning should have been an error previously).

view this post on Zulip Pierre Roux (Mar 22 2022 at 14:06):

(well, the coercions were still behaving as such for printing, but even that was broken)

view this post on Zulip Ana de Almeida Borges (Mar 22 2022 at 14:08):

So if it is not possible to satisfy the uniform inheritance condition, the idea is to turn off both uniform inheritance and ambiguous paths warnings?

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

I am confused about one thing from that PR however. The UIC is sufficient for non-ambiguous-coercion-paths but is it necessary?

view this post on Zulip Pierre Roux (Mar 22 2022 at 14:27):

The UIC is sufficient for the check to be complete but not necessary (as far as I understand).

view this post on Zulip Pierre Roux (Mar 22 2022 at 14:30):

Ana de Almeida Borges said:

So if it is not possible to satisfy the uniform inheritance condition, the idea is to turn off both uniform inheritance and ambiguous paths warnings?

If it were me, I would turn off the warnings locally when I know they are spurious (with Set Warnings "-uniform-inheritance". Coercion [...]. Set Warnings "uniform-inheritance".)

view this post on Zulip Ana de Almeida Borges (Mar 22 2022 at 14:46):

Yeah, I usually do that, but I'm usually not that confident that they are not spurious, so I always second guess myself :sweat_smile:

view this post on Zulip Cyril Cohen (Mar 23 2022 at 17:29):

Could you add an attribute e.g. #[nonuniform] Coercion [...]?

view this post on Zulip Pierre Roux (Mar 24 2022 at 12:48):

Here it is: https://github.com/coq/coq/pull/15853

view this post on Zulip Ana de Almeida Borges (Apr 02 2022 at 15:17):

That was a great idea and I think it could be extended to other warnings as well: https://github.com/coq/coq/issues/15893


Last updated: Jan 27 2023 at 02:04 UTC