Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: repeated `exists_congr`


Stuart Presnell (Feb 20 2022 at 16:08):

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 (Feb 20 2022 at 16:17):

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

Reid Barton (Feb 20 2022 at 16:20):

What does congr do with this currently?

Kyle Miller (Feb 20 2022 at 17:15):

@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 (Feb 20 2022 at 17:16):

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 (Feb 20 2022 at 17:17):

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

Bhavik Mehta (Feb 20 2022 at 17:17):

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

Kyle Miller (Feb 20 2022 at 17:20):

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

Reid Barton (Feb 20 2022 at 17:21):

That page doesn't contain rcongr...

Reid Barton (Feb 20 2022 at 17:22):

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

Eric Rodriguez (Feb 20 2022 at 17:24):

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

Reid Barton (Feb 20 2022 at 17:24):

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

Kyle Miller (Feb 20 2022 at 17:24):

@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 (Feb 20 2022 at 17:27):

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 (Feb 20 2022 at 19:06):

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


Last updated: Dec 20 2023 at 11:08 UTC