Stream: Coq users

Topic: `cbv`,`Set Debug Cbv`, and `Hint Transparent`


view this post on Zulip Janno (Jan 19 2021 at 16:01):

If I copy the output of Set Debug Cbv on let x := eval cbv in y in assert (x = y), convert all Unfolding <constant> lines into Hint Transparent <constant> : my_db, and then try to solve the goal (x = y) with autoapply @eq_refl with my_db, should I expect this to succeed? It doesn't solve the goal in my local example but I don't have anything minimized yet and wanted to check if my assumptions make any sense.

view this post on Zulip Matthieu Sozeau (Jan 19 2021 at 19:13):

It should I guess, just beware of the type being reduced too

view this post on Zulip Janno (Jan 20 2021 at 09:54):

Interesting point about the type. Luckily the type in my example is super simple and both x and y have the same type even without any reduction. As far as I can tell, tactic unification in autoapply (@eq_refl my_type x) with my_db fails on the terms itself but it doesn't give me any useful information:

Debug: Starting unification
Debug: Leaving unification with failure
[...]
Unable to unify "x = x" with "x = y"

view this post on Zulip Matthieu Sozeau (Jan 20 2021 at 10:38):

What's in the [...] ?

view this post on Zulip Janno (Jan 21 2021 at 12:54):

Just the context of the goal. No more output from Set Debug Tactic Unification.

view this post on Zulip Matthieu Sozeau (Jan 21 2021 at 13:20):

Then that's a bug I guess :)


Last updated: Feb 09 2023 at 00:03 UTC