## Stream: Coq users

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

#### 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?

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

#### 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: Jun 18 2024 at 20:02 UTC