From c30380e2fa0fcaed60ef79c97e6724b8763633a0 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 2 Feb 2022 18:23:18 -0800
Subject: [PATCH] feat: lift the restriction in `congr` theorems that all
 function arguments on the lhs must be free variables

see #988
---
 src/Lean/Meta/Tactic/Simp/CongrLemmas.lean |  7 +++----
 tests/lean/run/988.lean                    | 20 ++++++++++++++++++++
 2 files changed, 23 insertions(+), 4 deletions(-)

diff --git a/src/Lean/Meta/Tactic/Simp/CongrLemmas.lean b/src/Lean/Meta/Tactic/Simp/CongrLemmas.lean
index a758a8abbe..82b22fce5d 100644
--- a/src/Lean/Meta/Tactic/Simp/CongrLemmas.lean
+++ b/src/Lean/Meta/Tactic/Simp/CongrLemmas.lean
@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 import Lean.ScopedEnvExtension
 import Lean.Util.Recognizers
+import Lean.Util.CollectMVars
 import Lean.Meta.Basic
 
 namespace Lean.Meta
@@ -54,10 +55,8 @@ def mkCongrLemma (declName : Name) (prio : Nat) : MetaM CongrLemma := withReduci
         throwError "invalid 'congr' theorem, equality left/right-hand sides must be applications of the same function{indentExpr type}"
       let mut foundMVars : MVarIdSet := {}
       for lhsArg in lhsArgs do
-        unless lhsArg.isSort do
-          unless lhsArg.isMVar do
-            throwError "invalid 'congr' theorem, arguments in the left-hand-side must be variables or sorts{indentExpr lhs}"
-          foundMVars := foundMVars.insert lhsArg.mvarId!
+        for mvarId in (lhsArg.collectMVars {}).result do
+          foundMVars := foundMVars.insert mvarId
       let mut i := 0
       let mut hypothesesPos := #[]
       for x in xs, bi in bis do
diff --git a/tests/lean/run/988.lean b/tests/lean/run/988.lean
index 17f31582c6..72205b957e 100644
--- a/tests/lean/run/988.lean
+++ b/tests/lean/run/988.lean
@@ -33,3 +33,23 @@ example (as : Array (Nat → Nat)) (h : 0 + x < as.size) :
   rfl
 
 example [Decidable p] : decide (p ∧ True) = decide p := by simp -- should work
+
+def Pi.single [DecidableEq ι] {f : ι → Type u} [∀ i, Inhabited (f i)] (i : ι) (x : f i) : ∀ i, f i :=
+  fun j => if h : j = i then h ▸ x else default
+
+structure Set (α : Type u) where of :: mem : α → Prop
+
+instance : CoeSort (Set α) (Type u) where coe s := Subtype s.mem
+
+@[congr]
+theorem dep_congr [DecidableEq ι] {p : ι → Set α} [∀ i, Inhabited (p i)] :
+    ∀ {i j} (h : i = j) (x : p i) (y : α) (hx : x = y), Pi.single (f := (p ·)) i x = Pi.single (f := (p ·)) j ⟨y, hx ▸ h ▸ x.2⟩
+  | _, _, rfl, _, _, rfl => rfl
+
+theorem aux {p : Nat → Set Nat} {i j y : Nat} (x : p j) (h₁ : x = y) (h₂ : i = j) : Set.mem (p i) y := by
+  have := x.2
+  subst h₁ h₂
+  assumption
+
+example {p : Nat → Set Nat} [∀ i, Inhabited (p i)] (i : Nat) (x : p (0 + i)) (y : Nat) : Pi.single (f := (p ·)) (0 + i) x = Pi.single (f := (p ·)) i ⟨x, aux x rfl (Nat.zero_add i).symm ⟩ := by
+  simp