Quentin VERMANDE (Oct 25 2023 at 07:47): Quentin VERMANDE (Oct 25 2023 at 07:47):In the following script, I want to use an element f of @sig (A -> B) _ as a function from A to B. I declared a coercion using the coercion predicate from coq-elpi, but the coercion fails unless I explicitly ask for it (with f : A -> B). Actually, the debugging message does not even get printed. Using Set Debug "unification" reveals the expected unification problem from @sig (A -> B) _ to a dependent product type. Am I missing something?
The code :
From elpi.apps Require Import coercion.
Elpi Accumulate coercion.db lp:{{
coercion _ V T E {{ @proj1_sig lp:U lp:X lp:V }} :-
coq.say "default coercion from sig",
coq.unify-eq T {{ @sig lp:U lp:X }} ok.
}}.
Elpi Typecheck coercion.
Set Debug "unification".
Fail Goal forall A B (X : (A -> B) -> Prop) (f : @sig (A -> B) X) (x : A), (f : A -> B) x = f x.
The error and debugging messages :
[unification] sig|ZApp(A -> B, X)
sig|ZApp(?e0, ?e2)
default coercion from sig
[unification] sig|ZApp(A -> B, X)
forall H : ?T, ?T0@{y:=H}|
[unification] sig|ZApp(A -> B, X)
forall H : ?T, ?T0@{y:=H}|
The command has indeed failed with message:
Illegal application (Non-functional construction):
The expression "f" of type "{x : A -> B | X x}"
cannot be applied to the term
"x" : "A"
I cannot reproduce for now, can you print more debugging info? eg
coq.say "default coercion from sig where V=" V ", T =" T ", E = " E,
also it would help me if you had a statement like :
forall A B (X : (A -> B) -> Prop) (f : @sig (A -> B) X) (x : A) (y : B), f x = y.
So as to trigger at most one coercion and focus on the given problem
Quentin VERMANDE (Oct 25 2023 at 09:29):Your code only produces the error message :
From elpi.apps Require Import coercion.
Elpi Accumulate coercion.db lp:{{
coercion _ V T E {{ @proj1_sig lp:U lp:X lp:V }} :-
coq.say "default coercion from sig V = " V ", T =" T ", E =" E,
coq.unify-eq T {{ @sig lp:U lp:X }} ok.
}}.
Elpi Typecheck coercion.
Fail Goal forall A B (X : (A -> B) -> Prop) (f : @sig (A -> B) X) (x : A) (y : B), f x = y.
The command has indeed failed with message:
Illegal application (Non-functional construction):
The expression "f" of type "{x : A -> B | X x}"
cannot be applied to the term
"x" : "A"
Calling @Pierre Roux to the rescue on this one
Pierre Roux (Oct 25 2023 at 09:57):I'll have a look after lunch
Pierre Roux (Oct 25 2023 at 10:56):Looks like the coercion predicate isn't called but I don't know why. I need to investigate further but won't have time for it before tonight.
Enrico Tassi (Oct 25 2023 at 12:42):indeed it is not called. I think we made a mistake in setting up the hook in Coq.
It is the coercion to funclass which is not captured by the hook.
If you change your conclusion to x = f in your example, the elpi code is run (just put another rule to display how it is called).
Quentin VERMANDE (Oct 25 2023 at 13:02):Actually, with the conclusion x = f, I still do not get a message, but if I also change the type of x to A -> B it appears (and the elaboration succeeds).
Quentin VERMANDE (Oct 25 2023 at 13:07):Ok, I see what you meant. With the following code I receive a message from the first rule, but I also expected a message from the second one.
From elpi.apps Require Import coercion.
Elpi Accumulate coercion.db lp:{{
coercion _ V T E _ :-
coq.say V T E,
fail.
coercion _ V T E {{ @proj1_sig lp:U lp:X lp:V }} :-
coq.say "default coercion from sig V = " V ", T =" T ", E =" E,
coq.unify-eq T {{ @sig lp:U lp:X }} ok.
}}.
Elpi Typecheck coercion.
Fail Goal forall A B (X : (A -> B) -> Prop) (f : @sig (A -> B) X) (x : A) (y : B), x = f.
Well, yes. Internally coq has 3 points where coercions can be inserted:
F T with F : A -> B and T : A'F T and F : A with A =/= _ -> _fun x : T => and T : A for A =/= Type (or Prop, or SProp..)I guess we did not call the hook in the last two cases :-/
Quentin VERMANDE (Oct 26 2023 at 12:21):@Pierre Roux Do you plan on looking into this? Otherwise, Enrico and I will probably do it sometime next week.
Pierre Roux (Oct 26 2023 at 12:23):I think Enrico's understanding of the issue is just as good as mine, so if I don't do it by the end of the week (which I'll try but can't promise), please go ahead next week.
Pierre Roux (Oct 30 2023 at 15:23):Sorry, as I feared I didn't had time for this. Everything should happen in the coercion.ml file, probably in function inh_app_fun https://github.com/coq/coq/blob/master/pretyping/coercion.ml#L549 where the hook should be called similarly to what's done in inh_coerce_to_fail https://github.com/coq/coq/blob/master/pretyping/coercion.ml#L690
Quentin VERMANDE (Oct 30 2023 at 16:18):Ok, nevermind, we will do it. Thank you for the pointers.
Last updated: Oct 13 2024 at 01:02 UTC