Stream: Coq users

Topic: [ssr] congr gets stuck when given an incorrect number


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Apr 04 2022 at 18:30):

I believe the ssr syntax is congr (F _ _). Is it still slow?

view this post on Zulip Ana de Almeida Borges (Apr 04 2022 at 18:32):

Yeah.

view this post on Zulip Enrico Tassi (Apr 04 2022 at 18:33):

Oops, I did not know about congr <num> <term> :-/

view this post on Zulip Enrico Tassi (Apr 04 2022 at 18:33):

It is valid SSR, but I've never used it, so I can't help you

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Apr 04 2022 at 19:27):

here, reflexivity and apply are plain Coq tactics, while apply: and congr are ssreflect tactics.

view this post on Zulip 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

view this post on Zulip 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 [].

view this post on Zulip Ana de Almeida Borges (Apr 04 2022 at 20:48):

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: Feb 08 2023 at 22:03 UTC