repeated `exists_congr`

Stream: metaprogramming / tactics

[Stuart Presnell]

I'm interested in finally learning how to write tactics, and I think I've found a beginner project to work on. It seems like it should be possible to write a tactic that repeatedly applies exists_congr and intro to turn a goal of the form

(∃ a b c ..., P a b c ...) ↔ (∃ a b c ..., Q a b c ...)

into a goal of the form

a b c ... : α
⊢ P a b c ... ↔ Q a b c ...

This could remove the need for specialised lemmas like exists₂_congr, exists₃_congr etc. introduced in @Yaël Dillies's #11490.

I'm just posting this to check whether this seems like a worthwhile thing to try (at least, worth doing as a learning exercise).

(It's quite likely that everyone reading this is itching to reply with the trivial one-liner solution. Thanks in advance for letting me work it out for myself! :grinning: )

[Alex J. Best]

Lemmas are still useful in term mode! It certainly seems useful as a learning exercise, especially getting it to name things nicely

[Reid Barton]

What does congr do with this currently?

[Kyle Miller]

@Reid Barton congr fails, but congr' turns it into an equality of the underlying lambdas:

example (P Q : ℕ → ℕ → Prop) : (∃ n m, P n m) ↔ (∃ a b, Q a b) :=
begin
  congr',
  -- ⊢ (λ (n : ℕ), ∃ (m : ℕ), P n m) = λ (a : ℕ), ∃ (b : ℕ), Q a b
end

[Kyle Miller]

This reminds me of an earlier idea (in a thread with you and Kevin) to have a more powerful congr that could take a with clause and introduce arguments into the context.

[Kyle Miller]

It would be nice if it could also introduce additional hypotheses that congr lemmas can have, like docs#list.map_congr

[Bhavik Mehta]

tactic#congr' and tactic#rcongr can do some parts of this

[Kyle Miller]

congr' with n m seems to fail to do anything in this example, but rcongr n m works.

[Reid Barton]

That page doesn't contain rcongr...

[Reid Barton]

oh it sort of does, but hidden behind a dropdown menu

[Eric Rodriguez]

i have never seen rcongr in my life, what does it od?

[Reid Barton]

https://leanprover-community.github.io/mathlib_docs/tactic/congr.html#tactic.interactive.rcongr

[Kyle Miller]

@Bhavik Mehta How did you come across rcongr? There are only three uses of it in all of mathlib, and it's almost not in the documentation

[Kyle Miller]

I wonder how many undocumented tactics there are. Is it safe to say that all interactive tactics are in tactic.interactive and return tactic unit?

[Bhavik Mehta]

Kyle Miller said:

Bhavik Mehta How did you come across rcongr? There are only three uses of it in all of mathlib, and it's almost not in the documentation

From reading the documentation of congr, since I wanted to remind myself of the congr' syntax