Stream: Coq users

Topic: ✔ Rewrite gets stuck

view this post on Zulip Stefan Haan (Dec 20 2022 at 10:14):

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?

view this post on Zulip Paolo Giarrusso (Dec 20 2022 at 16:49):

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)...

view this post on Zulip Stefan Haan (Dec 25 2022 at 14:00):

It seems to be the case that unification is getting stuck trying to unify some number against a polynomial (?). make20.log.gz

view this post on Zulip Paolo Giarrusso (Dec 25 2022 at 22:43):

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

view this post on Zulip Stefan Haan (Dec 26 2022 at 22:34):

Indeed

#[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.

view this post on Zulip Paolo Giarrusso (Dec 27 2022 at 08:14):

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

view this post on Zulip Notification Bot (Dec 30 2022 at 23:54):

Stefan Haan has marked this topic as resolved.

Last updated: Oct 04 2023 at 20:01 UTC