feat: gcongr works with eta and proofs (#15364)

* `gcongr` now recognizes eta-expanded variables as variables
* `gcongr` now recognizes all proofs as "defeq" even if the proofs have different types (in e.g. `Finset.sup'_mono`
* Give a bit more information in the error message when not accepting a `gcongr`-lemma.

Author: fpvandoorn

Mathlib/Algebra/Order/BigOperators/Group/Finset.lean

@@ -96,7 +96,7 @@ variable {f g : ι → N} {s t : Finset ι}
 /-- In an ordered commutative monoid, if each factor `f i` of one finite product is less than or
 equal to the corresponding factor `g i` of another finite product, then
 `∏ i ∈ s, f i ≤ ∏ i ∈ s, g i`. -/
-@[to_additive sum_le_sum]
+@[to_additive (attr := gcongr) sum_le_sum]
 theorem prod_le_prod' (h : ∀ i ∈ s, f i ≤ g i) : ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i :=
   Multiset.prod_map_le_prod_map f g h
 
@@ -105,22 +105,6 @@ or equal to the corresponding summand `g i` of another finite sum, then
 `∑ i ∈ s, f i ≤ ∑ i ∈ s, g i`. -/
 add_decl_doc sum_le_sum
 
-/-- In an ordered commutative monoid, if each factor `f i` of one finite product is less than or
-equal to the corresponding factor `g i` of another finite product, then `s.prod f ≤ s.prod g`.
-
-This is a variant (beta-reduced) version of the standard lemma `Finset.prod_le_prod'`, convenient
-for the `gcongr` tactic. -/
-@[to_additive (attr := gcongr) GCongr.sum_le_sum]
-theorem _root_.GCongr.prod_le_prod' (h : ∀ i ∈ s, f i ≤ g i) : s.prod f ≤ s.prod g :=
-  s.prod_le_prod' h
-
-/-- In an ordered additive commutative monoid, if each summand `f i` of one finite sum is less than
-or equal to the corresponding summand `g i` of another finite sum, then `s.sum f ≤ s.sum g`.
-
-This is a variant (beta-reduced) version of the standard lemma `Finset.sum_le_sum`, convenient
-for the `gcongr` tactic. -/
-add_decl_doc GCongr.sum_le_sum
-
 @[to_additive sum_nonneg]
 theorem one_le_prod' (h : ∀ i ∈ s, 1 ≤ f i) : 1 ≤ ∏ i ∈ s, f i :=
   le_trans (by rw [prod_const_one]) (prod_le_prod' h)
@@ -385,29 +369,18 @@ theorem prod_lt_prod' (hle : ∀ i ∈ s, f i ≤ g i) (hlt : ∃ i ∈ s, f i <
     ∏ i ∈ s, f i < ∏ i ∈ s, g i :=
   Multiset.prod_lt_prod' hle hlt
 
-@[to_additive sum_lt_sum_of_nonempty]
+/-- In an ordered commutative monoid, if each factor `f i` of one nontrivial finite product is
+strictly less than the corresponding factor `g i` of another nontrivial finite product, then
+`s.prod f < s.prod g`. -/
+@[to_additive (attr := gcongr) sum_lt_sum_of_nonempty]
 theorem prod_lt_prod_of_nonempty' (hs : s.Nonempty) (hlt : ∀ i ∈ s, f i < g i) :
     ∏ i ∈ s, f i < ∏ i ∈ s, g i :=
   Multiset.prod_lt_prod_of_nonempty' (by aesop) hlt
 
-/-- In an ordered commutative monoid, if each factor `f i` of one nontrivial finite product is
-strictly less than the corresponding factor `g i` of another nontrivial finite product, then
-`s.prod f < s.prod g`.
-
-This is a variant (beta-reduced) version of the standard lemma `Finset.prod_lt_prod_of_nonempty'`,
-convenient for the `gcongr` tactic. -/
-@[to_additive (attr := gcongr) GCongr.sum_lt_sum_of_nonempty]
-theorem _root_.GCongr.prod_lt_prod_of_nonempty' (hs : s.Nonempty) (Hlt : ∀ i ∈ s, f i < g i) :
-    s.prod f < s.prod g :=
-  s.prod_lt_prod_of_nonempty' hs Hlt
-
 /-- In an ordered additive commutative monoid, if each summand `f i` of one nontrivial finite sum is
 strictly less than the corresponding summand `g i` of another nontrivial finite sum, then
-`s.sum f < s.sum g`.
-
-This is a variant (beta-reduced) version of the standard lemma `Finset.sum_lt_sum_of_nonempty`,
-convenient for the `gcongr` tactic. -/
-add_decl_doc GCongr.sum_lt_sum_of_nonempty
+`s.sum f < s.sum g`. -/
+add_decl_doc sum_lt_sum_of_nonempty
 
 -- Porting note (#11215): TODO -- calc indentation
 @[to_additive sum_lt_sum_of_subset]

Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean

@@ -32,6 +32,7 @@ lemma prod_nonneg (h0 : ∀ i ∈ s, 0 ≤ f i) : 0 ≤ ∏ i ∈ s, f i :=
 /-- If all `f i`, `i ∈ s`, are nonnegative and each `f i` is less than or equal to `g i`, then the
 product of `f i` is less than or equal to the product of `g i`. See also `Finset.prod_le_prod'` for
 the case of an ordered commutative multiplicative monoid. -/
+@[gcongr]
 lemma prod_le_prod (h0 : ∀ i ∈ s, 0 ≤ f i) (h1 : ∀ i ∈ s, f i ≤ g i) :
     ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i := by
   induction' s using Finset.cons_induction with a s has ih h
@@ -44,16 +45,6 @@ lemma prod_le_prod (h0 : ∀ i ∈ s, 0 ≤ f i) (h1 : ∀ i ∈ s, f i ≤ g i)
     · apply prod_nonneg fun x H ↦ h0 x (subset_cons _ H)
     · apply le_trans (h0 a (mem_cons_self a s)) (h1 a (mem_cons_self a s))
 
-/-- If all `f i`, `i ∈ s`, are nonnegative and each `f i` is less than or equal to `g i`, then the
-product of `f i` is less than or equal to the product of `g i`.
-
-This is a variant (beta-reduced) version of the standard lemma `Finset.prod_le_prod`, convenient
-for the `gcongr` tactic. -/
-@[gcongr]
-lemma _root_.GCongr.prod_le_prod (h0 : ∀ i ∈ s, 0 ≤ f i) (h1 : ∀ i ∈ s, f i ≤ g i) :
-    s.prod f ≤ s.prod g :=
-  s.prod_le_prod h0 h1
-
 /-- If each `f i`, `i ∈ s` belongs to `[0, 1]`, then their product is less than or equal to one.
 See also `Finset.prod_le_one'` for the case of an ordered commutative multiplicative monoid. -/
 lemma prod_le_one (h0 : ∀ i ∈ s, 0 ≤ f i) (h1 : ∀ i ∈ s, f i ≤ 1) : ∏ i ∈ s, f i ≤ 1 := by

Mathlib/Combinatorics/Schnirelmann.lean

@@ -108,7 +108,7 @@ lemma schnirelmannDensity_eq_zero_of_one_not_mem (h : 1 ∉ A) : schnirelmannDen
 lemma schnirelmannDensity_le_of_subset {B : Set ℕ} [DecidablePred (· ∈ B)] (h : A ⊆ B) :
     schnirelmannDensity A ≤ schnirelmannDensity B :=
   ciInf_mono ⟨0, fun _ ⟨_, hx⟩ ↦ hx ▸ by positivity⟩ fun _ ↦ by
-    gcongr; exact monotone_filter_right _ h
+    gcongr; exact h
 
 /-- The Schnirelmann density of `A` is `1` if and only if `A` contains all the positive naturals. -/
 lemma schnirelmannDensity_eq_one_iff : schnirelmannDensity A = 1 ↔ {0}ᶜ ⊆ A := by

Mathlib/Data/Finset/Basic.lean

@@ -2221,7 +2221,7 @@ theorem filter_subset_filter {s t : Finset α} (h : s ⊆ t) : s.filter p ⊆ t.
 
 theorem monotone_filter_left : Monotone (filter p) := fun _ _ => filter_subset_filter p
 
--- TODO: `@[gcongr]` doesn't accept this lemma because of the `DecidablePred` arguments
+@[gcongr]
 theorem monotone_filter_right (s : Finset α) ⦃p q : α → Prop⦄ [DecidablePred p] [DecidablePred q]
     (h : p ≤ q) : s.filter p ⊆ s.filter q :=
   Multiset.subset_of_le (Multiset.monotone_filter_right s.val h)

Mathlib/Data/Finset/Lattice.lean

@@ -844,18 +844,11 @@ lemma sup'_comp_eq_map {s : Finset γ} {f : γ ↪ β} (g : β → α) (hs : s.N
     s.sup' hs (g ∘ f) = (s.map f).sup' (map_nonempty.2 hs) g :=
   .symm <| sup'_map _ _
 
+
+@[gcongr]
 theorem sup'_mono {s₁ s₂ : Finset β} (h : s₁ ⊆ s₂) (h₁ : s₁.Nonempty) :
     s₁.sup' h₁ f ≤ s₂.sup' (h₁.mono h) f :=
   Finset.sup'_le h₁ _ (fun _ hb => le_sup' _ (h hb))
-
-/-- A version of `Finset.sup'_mono` acceptable for `@[gcongr]`.
-Instead of deducing `s₂.Nonempty` from `s₁.Nonempty` and `s₁ ⊆ s₂`,
-this version takes it as an argument. -/
-@[gcongr]
-lemma _root_.GCongr.finset_sup'_le {s₁ s₂ : Finset β} (h : s₁ ⊆ s₂)
-    {h₁ : s₁.Nonempty} {h₂ : s₂.Nonempty} : s₁.sup' h₁ f ≤ s₂.sup' h₂ f :=
-  sup'_mono f h h₁
-
 end Sup'
 
 section Inf'
@@ -1001,18 +994,11 @@ lemma inf'_comp_eq_map {s : Finset γ} {f : γ ↪ β} (g : β → α) (hs : s.N
     s.inf' hs (g ∘ f) = (s.map f).inf' (map_nonempty.2 hs) g :=
   sup'_comp_eq_map (α := αᵒᵈ) g hs
 
+@[gcongr]
 theorem inf'_mono {s₁ s₂ : Finset β} (h : s₁ ⊆ s₂) (h₁ : s₁.Nonempty) :
     s₂.inf' (h₁.mono h) f ≤ s₁.inf' h₁ f :=
   Finset.le_inf' h₁ _ (fun _ hb => inf'_le _ (h hb))
 
-/-- A version of `Finset.inf'_mono` acceptable for `@[gcongr]`.
-Instead of deducing `s₂.Nonempty` from `s₁.Nonempty` and `s₁ ⊆ s₂`,
-this version takes it as an argument. -/
-@[gcongr]
-lemma _root_.GCongr.finset_inf'_mono {s₁ s₂ : Finset β} (h : s₁ ⊆ s₂)
-    {h₁ : s₁.Nonempty} {h₂ : s₂.Nonempty} : s₂.inf' h₂ f ≤ s₁.inf' h₁ f :=
-  inf'_mono f h h₁
-
 end Inf'
 
 section Sup

Mathlib/MeasureTheory/Integral/Lebesgue.lean

@@ -87,17 +87,17 @@ theorem lintegral_mono' {m : MeasurableSpace α} ⦃μ ν : Measure α⦄ (hμν
   rw [lintegral, lintegral]
   exact iSup_mono fun φ => iSup_mono' fun hφ => ⟨le_trans hφ hfg, lintegral_mono (le_refl φ) hμν⟩
 
--- workaround for the known eta-reduction issue with `@[gcongr]`
+-- version where `hfg` is an explicit forall, so that `@[gcongr]` can recognize it
 @[gcongr] theorem lintegral_mono_fn' ⦃f g : α → ℝ≥0∞⦄ (hfg : ∀ x, f x ≤ g x) (h2 : μ ≤ ν) :
-    lintegral μ f ≤ lintegral ν g :=
+    ∫⁻ a, f a ∂μ ≤ ∫⁻ a, g a ∂ν :=
   lintegral_mono' h2 hfg
 
 theorem lintegral_mono ⦃f g : α → ℝ≥0∞⦄ (hfg : f ≤ g) : ∫⁻ a, f a ∂μ ≤ ∫⁻ a, g a ∂μ :=
   lintegral_mono' (le_refl μ) hfg
 
--- workaround for the known eta-reduction issue with `@[gcongr]`
+-- version where `hfg` is an explicit forall, so that `@[gcongr]` can recognize it
 @[gcongr] theorem lintegral_mono_fn ⦃f g : α → ℝ≥0∞⦄ (hfg : ∀ x, f x ≤ g x) :
-    lintegral μ f ≤ lintegral μ g :=
+    ∫⁻ a, f a ∂μ ≤ ∫⁻ a, g a ∂μ :=
   lintegral_mono hfg
 
 theorem lintegral_mono_nnreal {f g : α → ℝ≥0} (h : f ≤ g) : ∫⁻ a, f a ∂μ ≤ ∫⁻ a, g a ∂μ :=

Mathlib/Tactic/GCongr/Core.lean

@@ -156,25 +156,32 @@ initialize registerBuiltinAttribute {
   add := fun decl _ kind ↦ MetaM.run' do
     let declTy := (← getConstInfo decl).type
     withReducible <| forallTelescopeReducing declTy fun xs targetTy => do
-    let fail := throwError "\
-      @[gcongr] attribute only applies to lemmas proving \
-      x₁ ~₁ x₁' → ... xₙ ~ₙ xₙ' → f x₁ ... xₙ ∼ f x₁' ... xₙ', got {declTy}"
-    -- verify that conclusion of the lemma is of the form `rel (head x₁ ... xₙ) (head y₁ ... yₙ)`
-    let .app (.app rel lhs) rhs ← whnf targetTy | fail
-    let some relName := rel.getAppFn.constName? | fail
-    let (some head, lhsArgs) := lhs.withApp fun e a => (e.constName?, a) | fail
-    let (some head', rhsArgs) := rhs.withApp fun e a => (e.constName?, a) | fail
-    unless head == head' && lhsArgs.size == rhsArgs.size do fail
+    let fail (m : MessageData) := throwError "\
+      @[gcongr] attribute only applies to lemmas proving f x₁ ... xₙ ∼ f x₁' ... xₙ'.\n \
+      {m} in the conclusion of {declTy}"
+    -- verify that conclusion of the lemma is of the form `f x₁ ... xₙ ∼ f x₁' ... xₙ'`
+    let .app (.app rel lhs) rhs ← whnf targetTy |
+      fail "No relation with at least two arguments found"
+    let some relName := rel.getAppFn.constName? | fail "No relation found"
+    let (some head, lhsArgs) := lhs.withApp fun e a => (e.constName?, a) |
+      fail "LHS is not a function"
+    let (some head', rhsArgs) := rhs.withApp fun e a => (e.constName?, a) |
+      fail "RHS is not a function"
+    unless head == head' && lhsArgs.size == rhsArgs.size do
+      fail "LHS and RHS do not have the same head function and arity"
     let mut varyingArgs := #[]
     let mut pairs := #[]
     -- iterate through each pair of corresponding (LHS/RHS) inputs to the head function `head` in
     -- the conclusion of the lemma
     for e1 in lhsArgs, e2 in rhsArgs do
       -- we call such a pair a "varying argument" pair if the LHS/RHS inputs are not defeq
-      let isEq ← isDefEq e1 e2
+      -- (and not proofs)
+      let isEq := (← isDefEq e1 e2) || ((← isProof e1) && (← isProof e2))
       if !isEq then
-        -- verify that the "varying argument" pairs are free variables
-        unless e1.isFVar && e2.isFVar do fail
+        let e1 := e1.eta
+        let e2 := e2.eta
+        -- verify that the "varying argument" pairs are free variables (after eta-reduction)
+        unless e1.isFVar && e2.isFVar do fail "Not all arguments are free variables"
         -- add such a pair to the `pairs` array
         pairs := pairs.push (varyingArgs.size, e1, e2)
       -- record in the `varyingArgs` array a boolean (true for varying, false if LHS/RHS are defeq)
@@ -337,9 +344,12 @@ partial def _root_.Lean.MVarId.gcongr
       -- (if not, stop and report the existing goal)
       return (false, names, #[g])
     -- and also build an array of booleans according to which arguments `_ ... _` to the head
-    -- function differ between the LHS and RHS
-    (lhsArgs.zip rhsArgs).mapM fun (lhsArg, rhsArg) =>
-      return (none, !(← withReducibleAndInstances <| isDefEq lhsArg rhsArg))
+    -- function differ between the LHS and RHS. We treat always treat proofs as being the same
+    -- (even if they have differing types).
+    (lhsArgs.zip rhsArgs).mapM fun (lhsArg, rhsArg) => do
+      let isSame ← withReducibleAndInstances <|
+        return (← isDefEq lhsArg rhsArg) || ((← isProof lhsArg) && (← isProof rhsArg))
+      return (none, !isSame)
   -- Name the array of booleans `varyingArgs`: this records which arguments to the head function are
   -- supposed to vary, according to the template (if there is one), and in the absence of a template
   -- to record which arguments to the head function differ between the two sides of the goal.

test/GCongr/inequalities.lean

@@ -5,6 +5,7 @@ Authors: Heather Macbeth
 -/
 import Mathlib.Algebra.Order.BigOperators.Ring.Finset
 import Mathlib.Algebra.Order.Field.Basic
+import Mathlib.Data.Finset.Lattice
 import Mathlib.Tactic.Linarith
 import Mathlib.Tactic.GCongr
 import Mathlib.Tactic.SuccessIfFailWithMsg
@@ -169,6 +170,12 @@ example {a b c d e : ℝ} (_h1 : 0 ≤ b) (_h2 : 0 ≤ c) (hac : a * b + 1 ≤ c
   guard_target =ₛ a * b ≤ c * d
   linarith
 
+-- test big operators
+example (f g : ℕ → ℕ) (s : Finset ℕ) (h : ∀ i ∈ s, f i ≤ g i) :
+    ∑ i ∈ s, (3 + f i ^ 2) ≤ ∑ i ∈ s, (3 + g i ^ 2) := by
+  gcongr with i hi
+  exact h i hi
+
 -- this tests templates with binders
 example (f g : ℕ → ℕ) (s : Finset ℕ) (h : ∀ i ∈ s, f i ^ 2 + 1 ≤ g i ^ 2 + 1) :
     ∑ i ∈ s, f i ^ 2 ≤ ∑ i ∈ s, g i ^ 2 := by
@@ -209,3 +216,15 @@ example {x y : ℕ} (h : x ≤ y) (l) : dontUnfoldMe 14 l + x ≤ 0 + y := by
   gcongr
   guard_target = dontUnfoldMe 14 l ≤ 0
   apply test_sorry
+
+/-! Test that `gcongr` works well with proof arguments -/
+
+example {α β : Type*}  [SemilatticeSup α] (f : β → α)
+    {s₁ s₂ : Finset β} (h : s₁ ⊆ s₂) (h₁ : s₁.Nonempty) :
+    s₁.sup' h₁ f ≤ s₂.sup' (h₁.mono h) f := by
+  gcongr
+
+example {α β : Type*}  [SemilatticeSup α] (f : β → α)
+    {s₁ s₂ : Finset β} (h : s₁ ⊆ s₂) (h₁ : s₁.Nonempty) (h₂ : s₂.Nonempty) :
+    s₁.sup' h₁ f ≤ s₂.sup' h₂ f := by
+  gcongr