Ana de Almeida Borges (Apr 04 2022 at 17:14): Ana de Almeida Borges (Apr 04 2022 at 17:14):Is it expected that in some circumstances congr F and congr 1 F get stuck (or perhaps just take a long time to think) while congr 2 F or f_equal both succeed instantly?
Ana de Almeida Borges (Apr 04 2022 at 17:16):If I understand correctly, in the presence of some equality F a b = F c d where neither a = c nor b = d can be trivially solved, congr 1 F should complain with Error: No 1-congruence with F. So if it's getting stuck instead, it could be that it's trying very hard to unify either of the equalities and not timing out in a useful amount of time. However, in the case where I ran into this problem, reflexivity is immediate in telling me it can't solve either of those equalities.
Ana de Almeida Borges (Apr 04 2022 at 17:17):No sharable example as of yet, in part because I don't have a good model of what could be going wrong.
Enrico Tassi (Apr 04 2022 at 18:30):I believe the ssr syntax is congr (F _ _). Is it still slow?
Ana de Almeida Borges (Apr 04 2022 at 18:32):Yeah.
Enrico Tassi (Apr 04 2022 at 18:33):Oops, I did not know about congr <num> <term> :-/
Enrico Tassi (Apr 04 2022 at 18:33):It is valid SSR, but I've never used it, so I can't help you
Ana de Almeida Borges (Apr 04 2022 at 18:39):I'm not sure this is necessarily about that version of congr though. I mean, what would you say if I asked the same thing but mentioned only that congr (F _ _) fails and f_equal succeeds?
Paolo Giarrusso (Apr 04 2022 at 19:24):@Ana de Almeida Borges IIUC, you're saying that congr and reflexivity take very different times in solving unification problem, and you're surprised? That's 100% expected, tho for terrible reasons... can you compare reflexivity with apply eq_refl and with apply: eq_refl?
Paolo Giarrusso (Apr 04 2022 at 19:26):Coq has (at least) _two_ unification algorithms — plain Coq tactics typically use tactic unification, ssreflect uses evarconv, and they have incomparable performance.
Paolo Giarrusso (Apr 04 2022 at 19:27):here, reflexivity and apply are plain Coq tactics, while apply: and congr are ssreflect tactics.
Paolo Giarrusso (Apr 04 2022 at 19:31):@Ana de Almeida Borges if the situation isn't a congr bug but is explained by something like above (and maybe even if not), the fix will likely be more sealing in some definition in b or d. Which sealing, and where, is a much larger topic
Ana de Almeida Borges (Apr 04 2022 at 20:45):I didn't know there was more than one unification algorithm, thanks. But it doesn't seem to be the problem. The following all take about 0.002 seconds in both branches after a (successful) f_equal (what would be a = c and b = d in my example above):
Time Fail reflexivity.
Time Fail apply eq_refl.
Time Fail apply: eq_refl.
Time Fail by [].
Regarding the sealing: yeah, I suppose that may be the path I need to take. I though I had sealed everything already, but apparently not. I'll try to see if I can shed some more light on this with my particular example and possibly share a minimized version.
Last updated: Oct 03 2023 at 02:34 UTC