congr with subsingleton

Stream: general

[Reid Barton]

Is this a bug in congr?

example {α : Type} [subsingleton α] (x y : α) : x = y := by congr -- fails
example {α : Type} [subsingleton α] (x y : α) (f : α → nat) : f x = f y := by congr -- ok

[Kenny Lau]

what is supposed to the state after the first by congr?

[Reid Barton]

"no goals"

[Kenny Lau]

oh

[Reid Barton]

Actually, I made the second example slightly poor.

[Reid Barton]

Edited now.

[Mario Carneiro]

Not in the sense that I'm not surprised by the result

[Mario Carneiro]

congr only gets its subsingleton optimization when it actually applies a function

[Mario Carneiro]

because it simplifies the congruence lemma for f

[Mario Carneiro]

so if congr_core applies 0 times the optimization never gets a chance

[Reid Barton]

I see

[Reid Barton]

I have a more complicated example where congr fails even when there is a function being applied, but I need to minimize it first.

[Reid Barton]

Is simp supposed to understand subsingletons then? What exactly does it do with them? It can't handle either of these goals

[Mario Carneiro]

simp uses congr to enter a term, so it gets subsingleton handling indirectly that way

[Mario Carneiro]

but it won't rewrite x to y if that's what you mean

[Mario Carneiro]

mostly it's helpful for carrying along dependent arguments

[Reid Barton]

Oh, so by "it [congr] simplifies the congruence lemma" you don't mean using simp?

[Mario Carneiro]

No, I mean that the congruence lemma that is generated lacks an equality subgoal for any subsingleton arguments

[Reid Barton]

is this stuff in C++, in mk_specialized_congr_lemma?

[Mario Carneiro]

yes

[Mario Carneiro]

but you can see the resulting lemma by using the mk_congr_lemma function

[Reid Barton]

OK, the reason congr didn't work in my actual code is because I only have a subsingleton instance for a particular value of one of the type arguments, and the generated congruence lemma was too general and didn't specify the value of that type.

[Reid Barton]

(Namely, I have a subsingleton instance for a ⟶ b only when a is the initial object of a category)