From 13bcbe91cd072a2cbb15c4d021d3bdc96f90c1a1 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 23 Apr 2022 14:42:00 -0700
Subject: [PATCH] fix: regression reported at issue #1113

see issue #1113
---
 src/Lean/Meta/Tactic/Simp/Main.lean        | 22 +++++++++++++++++++---
 tests/lean/congrThmIssue.lean.expected.out |  5 ++++-
 tests/lean/run/1113b.lean                  |  9 +++++++++
 3 files changed, 32 insertions(+), 4 deletions(-)
 create mode 100644 tests/lean/run/1113b.lean

diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean
index 2f693c9b83..88232379e1 100644
--- a/src/Lean/Meta/Tactic/Simp/Main.lean
+++ b/src/Lean/Meta/Tactic/Simp/Main.lean
@@ -469,7 +469,7 @@ where
       withParent e <| e.withApp fun f args => do
         congrArgs (← simp f) args
 
-  /- Return true iff processing the given congruence theorem hypothesis produced a non-refl proof. -/
+  /-- Process the given congruence theorem hypothesis. Return true if it made "progress". -/
   processCongrHypothesis (h : Expr) : M Bool := do
     forallTelescopeReducing (← inferType h) fun xs hType => withNewLemmas xs do
       let lhs ← instantiateMVars hType.appFn!.appArg!
@@ -481,9 +481,25 @@ where
           throwCongrHypothesisFailed
         unless (← isDefEq h (← mkLambdaFVars xs (← r.getProof))) do
           throwCongrHypothesisFailed
-        return r.proof?.isSome
+        /- We used to return `false` if `r.proof? = none` (i.e., an implicit `rfl` proof) because we
+           assumed `dsimp` would also be able to simplify the term, but this is not true
+           for non-trivial user-provided theorems.
+           Example:
+           ```
+           @[congr] theorem image_congr {f g : α → β} {s : Set α} (h : ∀ a, mem a s → f a = g a) : image f s = image g s :=
+           ...
 
-  /- Try to rewrite `e` children using the given congruence theorem -/
+           example {Γ: Set Nat}: (image (Nat.succ ∘ Nat.succ) Γ) = (image (fun a => a.succ.succ) Γ) := by
+             simp only [Function.comp_apply]
+           ```
+           `Function.comp_apply` is a `rfl` theorem, but `dsimp` will not apply it because the composition
+           is not fully applied. See comment at issue #1113
+
+           Thus, we have an extra check now if `xs.size > 0`. TODO: refine this test.
+        -/
+        return r.proof?.isSome || (xs.size > 0 && lhs != r.expr)
+
+  /-- Try to rewrite `e` children using the given congruence theorem -/
   trySimpCongrTheorem? (c : SimpCongrTheorem) (e : Expr) : M (Option Result) := withNewMCtxDepth do
     trace[Debug.Meta.Tactic.simp.congr] "{c.theoremName}, {e}"
     let thm ← mkConstWithFreshMVarLevels c.theoremName
diff --git a/tests/lean/congrThmIssue.lean.expected.out b/tests/lean/congrThmIssue.lean.expected.out
index c8fa9d59c2..0b54d05197 100644
--- a/tests/lean/congrThmIssue.lean.expected.out
+++ b/tests/lean/congrThmIssue.lean.expected.out
@@ -7,4 +7,7 @@ h_size : size ≤ cap
 h_full : ∀ (i : Nat), i < size → Option.isSome (backing { val := i, isLt := (_ : i < cap) }) = true
 i : Nat
 h : i < size
-⊢ Option.isSome (if h : i < cap then backing { val := i, isLt := h } else none) = true
+⊢ Option.isSome
+      (if h_1 : i < cap then backing { val := i, isLt := (_ : { val := i, isLt := (_ : i < cap + cap) }.val < cap) }
+      else none) =
+    true
diff --git a/tests/lean/run/1113b.lean b/tests/lean/run/1113b.lean
new file mode 100644
index 0000000000..1ce7ae59dd
--- /dev/null
+++ b/tests/lean/run/1113b.lean
@@ -0,0 +1,9 @@
+def Set (α : Type u) := α → Prop
+def mem (a : α) (s : Set α) := s a
+def image (f : α → β) (s : Set α) : Set β := fun b => ∃ a, mem a s ∧ f a = b
+
+@[congr] theorem image_congr {f g : α → β} {s : Set α} (h : ∀ a, mem a s → f a = g a) : image f s = image g s :=
+  sorry
+
+example {Γ: Set Nat}: (image (Nat.succ ∘ Nat.succ) Γ) = (image (fun a => a.succ.succ) Γ) := by
+  simp only [Function.comp_apply]