Stream: general

Topic: convert with congr lemmas

Yury G. Kudryashov (Jun 11 2020 at 04:40):

Is there a version of convert that uses congr lemmas to dive into structures? E.g., I want to convert ∑ i in s, f i ≤ ∑ i in s, g i to ∑ i in s, f' i ≤ ∑ i in s, g' i and get goals ∀ i ∈ s, f i = f' i and ∀ i ∈ s, g i = g' i.

Yury G. Kudryashov (Jun 11 2020 at 04:41):

Of course, I can use convert ... using ...; apply sum_congr rfl; ... but I'd prefer to use a tactic.

Johan Commelin (Jun 11 2020 at 11:37):

Hmm, I'm actually surprised that convert doesn't just do that (modulo a funext)...

Yury G. Kudryashov (Jun 12 2020 at 02:29):

Currently it generates goals λ i, f i = λ i, f' i and λ i, g i = λ i, g' i.

Yury G. Kudryashov (Jun 12 2020 at 02:30):

Who understands internals of this tactic? @Mario Carneiro ?

Mario Carneiro (Jun 12 2020 at 02:31):

convert is a wrapper around congr', which is a thin veneer over core's congr

Mario Carneiro (Jun 12 2020 at 02:31):

Unfortunately congr doesn't do funext

Mario Carneiro (Jun 12 2020 at 02:32):

You can find plenty of examples of congr, funext, congr if you search mathlib

Yury G. Kudryashov (Jun 12 2020 at 02:34):

Would it be hard to write a version that uses @[congr] lemmas? funext is not the main problem here.

Yury G. Kudryashov (Jun 12 2020 at 02:39):

I mean, for me as a user the main problem is that it asks me to prove λ i, f i = λ i, f' i instead of ∀ i ∈ s, f i = f' i.

I thought it did

Mario Carneiro (Jun 12 2020 at 02:53):

When you give it the equality goal does congr do the right thing?

Yury G. Kudryashov (Jun 12 2020 at 03:36):

Tried these examples right after lemma prod_congr in algebra/big_operators:

example [has_le β] (h : 1   x in s₁, f x) : 1   x in s₂, g x :=
begin
convert h,
end
α : Type u,
β : Type v,
s₁ s₂ : finset α,
f g : α  β,
_inst_1 : comm_monoid β,
_inst_2 : has_le β,
h : 1   (x : α) in s₁, f x
1   (x : α) in s₂, g x
example : ( x in s₁, f x) =  x in s₂, f x :=
begin
congr,
end
α : Type u,
β : Type v,
s₁ s₂ : finset α,
f : α  β,
_inst_1 : comm_monoid β
s₁ = s₂

Yury G. Kudryashov (Jun 17 2020 at 14:59):

@Gabriel Ebner says that this is the intended behaviour: neither congr nor convert use @[congr]. It seems that none of @Mario Carneiro , @Johan Commelin and me knew for sure about this fact. I'll make a doc PR tonight.

Last updated: Aug 03 2023 at 10:10 UTC