gcongr handling equality?

Stream: mathlib4

[Terence Tao]

Thanks! That worked. Interestingly, gcongr totally chokes on proving equalities, such as

import Mathlib
open Finset
open BigOperators

example (n : ℕ) : ∏ j in range n, (n-j+j) = ∏ j in range n, n := by
  gcongr with i a
  sorry

and congr won't work either (n-j+j and n differ for j>n). prod_congr rfl will work here, but again it would be nice to have the "one-stop-shop".

[Jireh Loreaux]

Did you try using congr? prod_congr is marked with that attribute, so it should just apply that lemma. If not, it's likely a priority issue. I'll have time to try it tomorrow morning, but probably not before then.

[Terence Tao]

Jireh Loreaux said:

Did you try using congr? prod_congr is marked with that attribute, so it should just apply that lemma. If not, it's likely a priority issue. I'll have time to try it tomorrow morning, but probably not before then.

congr reduces ∏ j in range n, (n-j+j) = ∏ j in range n, n to (fun j => n - j + j) = fun j => n, which is not true for j : ℕ (the side condition j ∈ range n is not provided by congr). So indeed as you indicate the "default" congr simplification is applied before the prod_congr one is. If one could elevate the priority of prod_congr and sum_congr within the congr tactic, that would indeed be convenient.

[Kyle Miller]

You might try the congr! tactic, which is a mathlib-defined tactic that is able to handle more than the core congr. It can pick up on so-called "congruence lemmas" that are user-defined, and I believe prod_congr/sum_congr are marked as such.

[Jireh Loreaux]

Oh, that's the point, congr! is what uses that attribute. My bad

[Terence Tao]

Indeed, that solved that particular toy problem, though the inequality problem ∏ j in range n, (j+1) ≤ ∏ j in range n, n is not usefully simplified by congr! out of the box. (But perhaps one just then has to add other user-defined congruence lemmas such as Finset.prod_le_prod? Or maybe this should go into a gcongr! tactic?)

[Kyle Miller]

congr! is solving the restricted problem "given an eq/heq/iff, reduce the problem to showing an eq/heq/iff of corresponding parts of the LHS and RHS". It knows about ≤ insofar as it knows that it suffices to show an equality to prove ≤ (in general, it is aware of @[rfl]-tagged lemmas, which are lemmas that prove R x x for a given relation R, and it uses these lemmas to say it suffices to prove x = y to prove R x y).

[Kyle Miller]

You're not supposed to make @[congr] lemmas for relations other than eq/heq, as far as I understand.

[Kyle Miller]

Potentially gcongr (which is a mathlib tactic) could know about Finset.prod, but I don't personally know much about its design.

[Kyle Miller]

(Maybe @Heather Macbeth might have something to say about whether gcongr could one day be used for Finset.prod inequalities? In particular where you get that the index is in the given finset as an additional hypothesis? This is something that congr! can do for equalities. Edit: never mind, I didn't read the thread carefully, and I'm not familiar enough with how gcongr works)

[Terence Tao]

Kyle Miller said:

(Maybe Heather Macbeth might have something to say about whether gcongr could one day be used for Finset.prod inequalities? In particular where you get that the index is in the given finset as an additional hypothesis?)

It does this already (see above discussion), though one has to specify names for the index variable and the additional hypothesis using with if one actually wants to use that data.

[Kyle Miller]

Oh, sorry, it seems I'm not paying a basic level of attention to the thread. In that case, I'll just say that while perhaps congr! could apply to relations that aren't equality-like, it's only designed for equality-like relations -- I see congr! as being a technical sort of tactic that is good at equating things that are meant to be equal (even in the face of complicated dependent types), but gcongr is meant to be more useful for mathematical users, and it uses heuristics based on what's likely to be useful. (Note that congr! also takes a with clause to name these additional variables and hypotheses that appear.)

[Heather Macbeth]

@Mario Carneiro and I have talked about having gcongr support equality eventually, to offer the "one-stop shop" as Terry calls it. But the correct gcongr analogy for equality is somewhere between congr! and congrm, so it requires a new implementation.

Specifically, gcongr supports both custom congruence lemmas (like congr! does with docs#Finset.prod_congr) and pattern-matching (like congrm does).

[Heather Macbeth]

Compare:

import Mathlib
open Finset BigOperators

variable (a : ℕ)

example (n : ℕ) : a + ∏ j in range n, (n-j+j) ^ 2 ≤ a + ∏ j in range n, n ^ 2 := by
  gcongr a + Finset.prod _ ?_ with i h
  sorry

example (n : ℕ) : a + ∏ j in range n, (n-j+j) ^ 2 = a + ∏ j in range n, n ^ 2 := by
  congr! 2 with i h
  sorry

example (n : ℕ) : a + ∏ j in range n, (n-j+j) ^ 2 = a + ∏ j in range n, n ^ 2 := by
  congrm a + Finset.prod _ (fun i ↦ ?_)
  sorry

In the gcongr and congr! examples, we get a hypothesis h : i ∈ range n, which may well turn out to be necessary in such a problem. In the congrm example it applies the more naive congruence lemma which doesn't give you any such hypothesis.

[Heather Macbeth]

But that missing feature also allows an even nicer pattern-matching syntax for congrm than for gcongr: this works:

example (n : ℕ) : a + ∏ j in range n, (n-j+j) ^ 2 = a + ∏ j in range n, n ^ 2 := by
  congrm a + ∏ j in range n, ?_
  sorry

(There'd be no way, with that syntax, to specify the name of a hypothesis h.)

[Notification Bot]

16 messages were moved here from #mathlib4 > Why does gcongr hide variables? by Heather Macbeth.

[Yaël Dillies]

What about it leaves as goal j ∈ range n → (n-j+j) ^ 2 = n ^ 2 instead of (n-j+j) ^ 2 = n ^ 2? and if the ?_ is replaced by a more complicated pattern, append all the goals with j ∈ range n →? It would be nice if the assumption was automatically introduced, but not introducing it sounds like a good compromise if naming it is hard.