congrm

Stream: Is there code for X?

[Alex Kontorovich]

What happened to the lean3 tactic congrm? Thanks!

[Kyle Miller]

@Alex Kontorovich It's under review -- I can ping you once it's in mathlib4

[Alex Kontorovich]

That'd be great, thanks!

[Kyle Miller]

@Alex Kontorovich congrm was just merged (#2544), and it's imported in Mathlib.Tactic.Common so you probably don't need to import anything to use it.

It now uses gcongr-like syntax, where in the pattern you use ?_ holes to signify where the congruence holes are. You can use _ holes where the value doesn't change from one side to the other.

[Kyle Miller]

A new feature this PR introduces is "congruence quotations."

Do you not remember which is congr_arg, congr_fun, or congr? Now you don't need to:

example {α β : Sort _} (f : α → β) (x y : α) (h : x = y) :
    f x = f y := congr(f $h)

example {α : Sort _} {β : α → Sort _} (f g : (x : α) → β x) (h : f = g) (x : α) :
    f x = g x := congr($h x)

example {α β : Sort _} (f g : α → β) (hf : f = g) (x y : α) (hx : x = y) :
    f x = g y := congr($hf $hx)

Another example:

example (a b c d e f : Nat) (hab : a = b) (hcd : c = d) (hef : e = f) :
    1 + a + c * e = 1 + b + d * f :=
  congr(1 + $hab + $hcd * $hef)

It can also handle Subsingleton instance arguments automatically. Here's an example you can't do with congr_arg:

example [Fintype α] [Fintype β] (h : α = β) : Fintype.card α = Fintype.card β :=
  congr(Fintype.card $h)

[Kyle Miller]

Congruence quotations can work with iffs, eqs, and heqs.

[Yaël Dillies]

Question: Why is it congr(...), not congr (...)?

[Yaël Dillies]

Is it supposed to mimic QQ quotations?

[Kyle Miller]

One reason is if it were congr (...) then congr would become a keyword and you wouldn't be able to use docs#congr

Another is that not having a space is already set aside for new syntax. Writing f(x) for f (x) is a syntax error in Lean 4. And yes, it's supposed to be like other sorts of quotations, including QQ's.