congr unexpectedly fails with Set.image

Stream: mathlib4

[Terence Tao]

For some reason congr cannot seem to reduce with Set.image:

import Mathlib

example {X Y:Type} (f: X → Y) (E F: Set X) (h: E = F) : f '' E = f '' F := by
  congr -- does nothing!
  exact h -- fails due to inability of congr to reduce

example {X Y:Type} (f: X → Y) (E F: Set X) (h: E = F) : @Set.image X Y f E = @Set.image X Y f F := by
  congr -- does nothing!
  exact h -- fails due to inability of congr to reduce

Is this a bug? convert rfl works, though it manages to somehow reverse the equality:

import Mathlib

example {X Y:Type} (f: X → Y) (E F: Set X) (h: E = F) : f '' E = f '' F := by
  convert rfl  -- works, though with equality reversed
  exact h.symm

Also, congr! closes the goal completely.

[Kyle Miller]

It's likely a bug — I wrote congr! to be a replacement of congr, and the eventual plan is to improve the core congr.

[Kyle Miller]

Here are a few more approaches to congruence here (these all use the same underlying system):

import Mathlib

example {X Y:Type} (f: X → Y) (E F: Set X) (h: E = F) : f '' E = f '' F :=
  congr(f '' $h)

example {X Y:Type} (f: X → Y) (E F: Set X) (h: E = F) : f '' E = f '' F := by
  refine congr(f '' $(?_))
  exact h

example {X Y:Type} (f: X → Y) (E F: Set X) (h: E = F) : f '' E = f '' F := by
  congrm f '' ?_
  exact h

[Terence Tao]

Yeah, everything other than vanilla congr seems to work just fine here

[Kyle Miller]

Terence Tao said:

convert rfl works

That's amusing that it reverses the equality... I'm not sure exactly why that is, but I imagine it has something to do with unification order (you can see hints of it with convert rfl using 0).

The convert tactic is a frontend for congr!, so it makes sense that it works here.

[Kyle Miller]

I believe the underlying bug is that congr miscalculates the arity of Set.image. The arity is 4, and it's given four arguments, but it's unfolding Set and seeing it as having arity 5.

(This affects simp too, but there are some other features that paper over the issue, so long as functions involved don't have some complicated dependent types.)

[Terence Tao]

congr also fails to work with the other argument of Set.image, which seems consistent with your diagnosis:

example {X Y:Type} (f g: X → Y) (E: Set X) (h: f = g) : f '' E = g '' E := by
  congr -- does nothing!
  exact h -- fails due to inability of congr to reduce

[Kyle Miller]

At some point I fixed the corresponding bug in conv mode's arg/enter/congr tactics

example {X Y:Type} (f: X → Y) (E F: Set X) (h: E = F) : f '' E = f '' F := by
  conv =>
    enter [1,2]
    rw [h]

example {X Y:Type} (f: X → Y) (E F: Set X) (h: E = F) : f '' E = f '' F := by
  conv =>
    congr
    congr
    rfl
    rw [h]

It's not the same congr, so it didn't fix the main tactic mode congr

[Terence Tao]

ok so hopefully it is just a matter of porting some previous bugfix to the congr code?

[Kyle Miller]

(Or it was another bug I fixed, but in any case conv mode works!)

[Kyle Miller]

They work pretty differently, so it's not going to be a bugfix port, but the principle is similar. I'd suggest using congr! for now, unless you have a reason not to.

[Kyle Miller]

I think there's a good chance that there will be some attention on improving congr this summer.

[Kyle Miller]

lean4#9225 has a fix, though it likely will need a number of mathlib adaptations

[Kevin Buzzard]

Note also #25889 which fixes issues with conv? miscounting.

[Kyle Miller]

(Looking through some old issues, I was just reminded of the fact that I reported this issue with congr and Set.image back in #lean4 > mkCongrSimp? error for Set @ 💬! Happy to see it's resolved.)