Hi. In the following script, I have a Check
that fails due to a failed assertion in coq_elpi_HOAS.ml
.
I define two tactics that print their goal, try to solve it and fallback on tc's typeclass instanciation upon failure. Then I declare a structure for sets, a class for the set membership predicate and a structure memType
bundling the two (hence mimicking sig, but with a structure). I define a coercion from a type to any of its induced memTypes that delegates finding the missing membership proof to one of the previously declared tactic. Then I declare an instance of mem
that delegates finding the proof term to one of the tactics. Now, trying to coerce an element of nat
to some dummy memType nat P
fails exactly when the coercion uses the done
tactic, with the above mentioned error.
Debugging shows that the coercion calls the tactic, which in turn calls typeclass inference. The tc-mem
predicate goes to the line where it should call the tactic and then fails without the tactic ever printing anything. If I change the dummy predicate to something that done2
can not prove, the whole process fails normally.
The question here is not so much how I should make the tactic work (since this example is minimized), but rather what happens at the failure point. Does anyone have an idea?
The code:
From Coq Require Import ssreflect.
From elpi.apps Require Import tc coercion.
Ltac done := (match goal with |- ?G => idtac "goal " G end);
(do ![trivial | split]); idtac "apply"; apply _ .
Ltac done2 := (match goal with |- ?G => idtac "goal2 " G end);
(do !split); trivial; idtac "apply"; apply _.
Structure set (T : Type) := MkSet {
set_to_pred : T -> Prop
}.
Class mem T (X : set T) (x : T) : Prop := Mem { IsMem : set_to_pred T X x }.
Structure memType T (X : set T) := MemType {
this : T;
memP : mem T X this
}.
Elpi Accumulate coercion.db lp:{{
coercion _ V T E R :-
coq.unify-eq E {{ @memType lp:T (lp:X : set lp:T) }} ok,
R = {{ @MemType lp:T lp:X lp:V _ }},
% we call the solver
coq.ltac.collect-goals R [G] [],
coq.ltac.open (coq.ltac.call-ltac1 "done") G [].
}}.
Elpi Typecheck coercion.
Elpi Accumulate TC.Solver lp:{{
tc-buffer3.tc-mem T X V R :-
R = {{ @Mem lp:T lp:X lp:V _ }},
coq.say R,
% we call the solver
coq.ltac.collect-goals R [G] [],
std.spy (coq.ltac.open (coq.ltac.call-ltac1 "done") G []).
}}.
Elpi Typecheck TC.Solver.
Check fun (x : nat) => x : memType nat (@MkSet nat (fun x : nat => True)).
Fail Check fun (x : nat) => x : memType nat (@MkSet nat (fun x : nat => exists y, y = x)).
The error and debugging messages :
Anomaly
"File "src/coq_elpi_HOAS.ml", line 3365, characters 42-48: Assertion failed."
Please report at http://coq.inria.fr/bugs/.
goal (mem nat {| set_to_pred := fun _ : nat => True |} x)
apply
app
[global (indc «Mem»), global (indt «nat»),
app
[global (indc «MkSet»), global (indt «nat»),
fun `elpi_ctx_entry_1_` (global (indt «nat»)) c1 \
global (indt «True»)], c0, X0^1]
----<<---- enter:
coq.ltac.open (coq.ltac.call-ltac1 done)
(nabla c1 \
seal
(goal [decl c1 `x` (global (indt «nat»))] (X1 c1) (X2 c1) (X1 c1) []))
[]
That could be an instance of a problem I'm trying to fix. Can you try to cherry pick this commit: https://github.com/LPCIC/coq-elpi/pull/537/commits/eec420c1cd7ee16d1b72b62d745149955c9c9274
Last updated: Oct 13 2024 at 01:02 UTC