Tactic for applying a function to equation in hypothesis?

Stream: Is there code for X?

[Casavaca]

How to do this?

example {α β : Type} (f : α → β) (a b : α) (h : a = b) : True := by
  magic_apply f at h
  -- α β : Type
  -- f : α → β
  -- a b : α
  -- h : f a = f b

Right now I have to do: have h' : (h a = h b) := by rw [h]; clear h. but when a and b is very long this is not very pretty.

[Kim Morrison]

import Mathlib.Tactic.ApplyFun

example {α β : Type} (f : α → β) (a b : α) (h : a = b) : True := by
  apply_fun f at h
  -- α β : Type
  -- f : α → β
  -- a b : α
  -- h : f a = f b

[Damiano Testa]

Maybe also apply f at h?

[Jz Pan]

You can also use replace h := congr(f $h). Personally, I think this is more flexible.

Maybe also apply f at h?

No, this doesn't work; apply f at h is the same as replace h := f h which is not correct.

[Matt Diamond]

apply_fun looks very useful... in term mode you can use docs#congrArg

[Kyle Miller]

apply_fun can handle some dependent situations that congrArg can't, like if there's a DecidableEq or Fintype argument that comes after. (In term mode, congr(f $h) can handle similar things as apply_fun. In simpler cases, it's the same as congrArg f h. This congr(...) thing also generalizes, for example congr($h1 + $h2 + $h3) to get a1 + a2 + a3 = b1 + b2 + b3 for h1 : a1 = b1, etc.)

[Jz Pan]

Kyle Miller said:

for example congr($h1 + $h2 + $h3) to get a1 + a2 + a3 = b1 + b2 + b3 for h1 : a1 = b1, etc.)

So congr can do the things linear_combination can do?

[Michael Stoll]

I think linear_combination also moves stuff between the left and right hand sides, e.g.,

import Mathlib

example (x y : ℤ) (h : x = y) : x - y = 0 := by linear_combination h

[Kyle Miller]

congr(...) and linear_combination do have a slightly intertwined history. When linear_combination's syntax was being designed a few years ago, there were thoughts about what the general congruence syntax could be, but linear_combination can take advantage of what linear combinations look like, to be able to use proofs right in the term without any special syntax. Heather Macbeth then were talking about this again last year, inspired by the metaprogramming possibilities of Lean 4, and we thought about whether we could get a general congruence syntax to work (imagine congr(h1 + h2 + h3)) and maybe use this to implement other tactics, but eventually it was clear it would be much more reliable to write it with $ prefixes. Unlike linear_combination, the congr(...) term aims to be able to handle arbitrary Lean expressions.

By the way, the congrm tactic uses congr(...) under the hood, where congrm ?_ + ?_ + ?_ turns into refine congr($?_ + $?_ + $?_).

[Jz Pan]

The familiar $ prefix reminds me of environmental variables in bash script :joy:

[Kyle Miller]

The reason that congr(...) uses it is to have uniformity with antiquotations in syntax quotations and in Qq expression quotations (re-using $ also saves us from needing to introduce our own global notation). I'm not sure why Lean chose $ for antiquotations, but it's certainly used in a number of languages as a variable sigil! It's helpful leaning on that familiarity.