Hi, I'm trying to use rewrite to replace some term with it's upper bound in the goal. This requires some
Proper (le ==> ... ==> le) instances to be declared which inspired this PR.
However I have found that under some circumstances
rewrite seems to get stuck. To be precise it does seem to loop indefinitely here .
The output of
Set Typeclasses Debug Verbosity 2. gives me
COQC theories/NP/SAT/CookLevin/Reductions/FlatSingleTMGenNP_to_FlatTCC.v Debug: Calling typeclass resolution with flags: depth = ∞,unique = false,do_split = false,fail = true Debug: Starting resolution with 5 goal(s) under focus and 0 shelved goal(s) in only_classes mode, unbounded Debug: Launching resolution fixpoint on 5 goals: ?X6955 : (Proper (le ==> ?r) (Init.Nat.add (poly__makeAllEvalEnvFlat 1 4 0 0 (size (enc tm))))) ?X6958 : (Proper (?r ==> ?r1 ==> ?r0) Init.Nat.add) ?X6959 : (ProperProxy ?r1 c__flatMTRCards) ?X6964 : (Proper (?r0 ==> ?r2 ==> Basics.flip Basics.impl) le) ?X6965 : (ProperProxy ?r2 (poly__flatMTRCards (size (enc tm)))) Debug: Calling fixpoint on : 5 initial goals, 0 stuck goals and 0 non-stuck failures kept with no progress made in this run. Stuck: Failed: Initial: Goal 1 evar: ?X6955 status: initial Goal 2 evar: ?X6958 status: initial Goal 3 evar: ?X6959 status: initial Goal 4 evar: ?X6964 status: initial Goal 5 evar: ?X6965 status: initial Debug: considering goal 1 of status initial Debug: 1: looking for (Proper (le ==> ?r) (Init.Nat.add (poly__makeAllEvalEnvFlat 1 4 0 0 (size (enc tm))))) with backtracking
There is no more output even though
rewrite is clearly doing something. I know that removing the
makeAllEvalEnvFlat_mono instance will make rewrite succeed, but there seems to be some bigger problem here. How can I figure out what is going wrong?
Set Debug "tactic-unification,unification". might be helpful if _unification_ is getting stuck... I also thought higher verbosity levels for TC debugging were allowed (even if they don't seem documented)...
It seems to be the case that unification is getting stuck trying to unify some number against a polynomial (?). make20.log.gz
Just saw this: Haven't looked at the trace yet, but you might need to make the polynomial function typeclass opaque (and maybe also to tell rewrite to treat addition as binary via a Params instance?)... I'll try to take a look but feel free to ping
#[export] Typeclasses Opaque poly__makeAllEvalEnvFlat.
makes everything work again. :tada:
About declaring addition as binary, using any other value than 0 in
Params Nat.add 0 makes rewrite fail which seems strange.
Using 0 is correct (it means "0 arguments of Nat.add should be excluded from setoid rewriting), and it should already make a difference and forbid the trace you showed in the OP.
Docs for Params: https://gitlab.mpi-sws.org/iris/stdpp/-/blob/b391a3c262be1c10672a5456144c12a5f3290734/stdpp/base.v#L329
Stefan Haan has marked this topic as resolved.
Last updated: Oct 04 2023 at 20:01 UTC