Quentin VERMANDE (Oct 17 2023 at 13:40): Quentin VERMANDE (Oct 17 2023 at 13:40):Hi. I have an error that I struggle to understand. In the following script, I declare proj1_sig as a coercion using elpi, then declare some additive structure on nat and a subtype evenof integers. Then, typechecking n + m : nat with n : nat and m : even fails with the error "Ill-typed evar instance". In case that is relevant, debugging shows that, at some point after mis coerced to nat, the only missing piece in the term is the additive structure of nat. Besides, replacing in the elpi code @sig lp:E _ by @sig lp:E lp:P and proj1_sigby @proj1_sig lp:E lp:P makes the error disappear. Can someone help me make sense of what happens here?
The code:
From elpi.apps Require Import coercion.
Definition set (T : Type) := T -> Prop.
Class mem T (X : set T) (x : T) : Prop := Mem { IsMem : X x }.
Coercion mem_of_set T (X : set T) : Type := @sig T X.
Elpi Accumulate coercion.db lp:{{
coercion _ V T E X :-
std.spy (coq.unify-eq T {{ @sig lp:E _ }} ok),
std.spy (coq.elaborate-skeleton {{ proj1_sig lp:V }} E X ok).
}}.
Elpi Typecheck coercion.
Class hasAdd T := HasAdd { add_op : T -> T -> T }.
Structure addType := AddType {
add_sort :> Type;
add_of_addType : hasAdd add_sort;
}.
Definition add {T} := (@add_op _ (add_of_addType T)).
Canonical generic_addType T a := AddType T a.
Instance nat_add : hasAdd nat := HasAdd nat plus.
Definition even : set nat := sig (fun n => exists m, n = 2 * m).
Section tests.
Variables (n : nat) (m : even).
Set Printing All.
Check (add n m) : nat.
The error message (with debugging) :
----<<---- enter:
coq.unify-eq
(app
[global (const «mem_of_set»), global (indt «nat»),
global (const «even»)])
(app
[global (indt «memType»),
app
[global (const «add_sort»),
app [global (const «generic_addType»), global (indt «nat»), X0]],
X1]) ok
---->>---- exit:
coq.unify-eq
(app
[global (const «mem_of_set»), global (indt «nat»),
global (const «even»)])
(app
[global (indt «memType»),
app
[global (const «add_sort»),
app [global (const «generic_addType»), global (indt «nat»), X2]],
global (const «even»)]) ok
----<<---- enter:
coq.elaborate-skeleton
(app [global (const «this»), X3, X4, global (const «m»)])
(app
[global (const «add_sort»),
app [global (const «generic_addType»), global (indt «nat»), X2]]) X5
ok
---->>---- exit:
coq.elaborate-skeleton
(app [global (const «this»), X3, X4, global (const «m»)])
(app
[global (const «add_sort»),
app [global (const «generic_addType»), global (indt «nat»), X6]])
(app
[global (const «this»), global (indt «nat»), global (const «even»),
global (const «m»)]) ok
@Quentin VERMANDE I do not see the error message.
Quentin VERMANDE (Oct 17 2023 at 14:32):Sorry, I messed up with Zulip's code formatting, it should appear now.
Quentin VERMANDE (Oct 17 2023 at 15:34):As I actually managed to work around the issue in the previous one, it might not be that interesting. Here is one where I actually do not find a solution. It is slightly more involved as I also have to declare an additive structure on even and have things being inferred automatically.
From Coq Require Import Lia.
From Coq Require Import PeanoNat.
From Coq Require Import ssreflect ssrbool ssrfun.
From elpi.apps Require Import coercion.
Ltac done :=
trivial; hnf; intros; solve
[ do ![solve [trivial | apply: sym_equal; trivial]
| discriminate | contradiction | split]
| case not_locked_false_eq_true; assumption
| match goal with H : ~ _ |- _ => solve [case H; trivial] end
| typeclasses eauto ].
Definition set (T : Type) := T -> Prop.
Class mem T (X : set T) (x : T) : Prop := Mem { IsMem : X x }.
Notation "x \in X" := (@mem _ X x).
Coercion mem_of_set T (X : set T) : Type := @sig T (@mem T X).
Elpi Accumulate coercion.db lp:{{
coercion _ V T E {{ @proj1_sig lp:E lp:X lp:V }} :-
coq.unify-eq T {{ @sig lp:E lp:X }} ok.
coercion _ V T E R :-
coq.unify-eq E {{ @sig lp:T lp:X }} ok,
R = {{ @exist lp:T lp:X lp:V _ }},
coq.ltac.collect-goals R [G] [],
coq.ltac.open (coq.ltac.call-ltac1 "done") G [].
}}.
Elpi Typecheck coercion.
Class hasAdd T := HasAdd { add_op : T -> T -> T }.
Structure addType := AddType {
add_sort :> Type;
add_of_addType : hasAdd add_sort;
}.
Definition add {T} := (@add_op _ (add_of_addType T)).
Canonical generic_addType T a := AddType T a.
#[global] Instance nat_add : hasAdd nat := HasAdd nat plus.
Definition even : set nat := fun n => exists m, n = 2 * m.
Lemma even_add (a : even) (b : even) : @add nat a b \in even.
Proof.
case: a b => a H [b H0].
have [[m/= ->]] := H. have [[n/= ->]] := H0.
by exists; exists (add m n); rewrite /add/=; lia.
Qed.
Program Instance even_hasAdd : hasAdd even :=
HasAdd even (fun (x y : even) => @exist _ _ (@add nat x y) _).
Next Obligation.
by apply: even_add.
Qed.
Section tests.
Variables (n : nat) (n_even : n \in even) (m : even).
Check add m (n : even) : even.
Fail Check add m n : even.
The first error is likely a bug on my side, so please open an issue. For the second problem, I hope I'll have time to look into it next week
Quentin VERMANDE (Oct 18 2023 at 11:37):I opened the issue here : https://github.com/LPCIC/coq-elpi/issues/523
Last updated: Oct 13 2024 at 01:02 UTC