From dbb6dcd9a96ad8c0e05f393bbf830e7e61fb1b28 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 2 Feb 2022 15:39:51 -0800
Subject: [PATCH] fix: remove irrelevant hypotheses in auto-generated equation
 theorems

---
 src/Lean/Elab/PreDefinition/Eqns.lean | 21 ++++++++++++++++++++-
 tests/lean/986.lean                   |  4 ++++
 tests/lean/986.lean.expected.out      | 11 +++++++++++
 3 files changed, 35 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/986.lean
 create mode 100644 tests/lean/986.lean.expected.out

diff --git a/src/Lean/Elab/PreDefinition/Eqns.lean b/src/Lean/Elab/PreDefinition/Eqns.lean
index d641e7a261..b6f14476d5 100644
--- a/src/Lean/Elab/PreDefinition/Eqns.lean
+++ b/src/Lean/Elab/PreDefinition/Eqns.lean
@@ -70,13 +70,24 @@ private def keepGoing (mvarId : MVarId) : ReaderT Context (StateRefT (Array Expr
   let ctx ← read
   return Option.isSome <| rhs.find? fun e => ctx.declNames.any e.isAppOf && e.hasLooseBVars
 
+private def lhsDependsOn (type : Expr) (fvarId : FVarId) : MetaM Bool :=
+  forallTelescope type fun _ type => do
+    if let some (_, lhs, _) ← matchEq? type then
+      dependsOn lhs fvarId
+    else
+      dependsOn type fvarId
+
+/--
+  Eliminate `namedPatterns` from equation, and trivial hypotheses.
+-/
 def simpEqnType (eqnType : Expr) : MetaM Expr := do
   forallTelescopeReducing (← instantiateMVars eqnType) fun ys type => do
     let proofVars := collect type
-    trace[Meta.debug] "proofVars: {proofVars.toList.map mkFVar}"
+    trace[Meta.debug] "simpEqnType: {type}"
     let mut type ← Match.unfoldNamedPattern type
     let mut eliminated : FVarIdSet := {}
     for y in ys.reverse do
+      trace[Meta.debug] ">> simpEqnType: {← inferType y}, {type}"
       if proofVars.contains y.fvarId! then
         let some (_, Expr.fvar fvarId _, rhs) ← matchEq? (← inferType y) | throwError "unexpected hypothesis in altenative{indentExpr eqnType}"
         eliminated := eliminated.insert fvarId
@@ -85,6 +96,14 @@ def simpEqnType (eqnType : Expr) : MetaM Expr := do
         if (← dependsOn type y.fvarId!) then
           type ← mkForallFVars #[y] type
       else
+        if let some (_, lhs, rhs) ← matchEq? (← inferType y) then
+          if (← isDefEq lhs rhs) then
+            if !(← dependsOn type y.fvarId!) then
+              continue
+            else if !(← lhsDependsOn type y.fvarId!) then
+              -- Since the `lhs` of the `type` does not depend on `y`, we replace it with `Eq.refl` in the `rhs`
+              type := type.replaceFVar y (← mkEqRefl lhs)
+              continue
         type ← mkForallFVars #[y] type
     return type
 where
diff --git a/tests/lean/986.lean b/tests/lean/986.lean
new file mode 100644
index 0000000000..3f88415f86
--- /dev/null
+++ b/tests/lean/986.lean
@@ -0,0 +1,4 @@
+attribute [simp] Array.insertionSort.swapLoop
+
+#check @Array.insertionSort.swapLoop._eq_1
+#check @Array.insertionSort.swapLoop._eq_2
diff --git a/tests/lean/986.lean.expected.out b/tests/lean/986.lean.expected.out
new file mode 100644
index 0000000000..08c1a162b5
--- /dev/null
+++ b/tests/lean/986.lean.expected.out
@@ -0,0 +1,11 @@
+@Array.insertionSort.swapLoop._eq_1 : ∀ {α : Type u_1} (lt : α → α → Bool) (a : Array α) (h : 0 < Array.size a),
+  Array.insertionSort.swapLoop lt a 0 h = a
+@Array.insertionSort.swapLoop._eq_2 : ∀ {α : Type u_1} (lt : α → α → Bool) (a : Array α) (j' : Nat)
+  (h : Nat.succ j' < Array.size a),
+  Array.insertionSort.swapLoop lt a (Nat.succ j') h =
+    (fun h' =>
+        if lt (Array.get a { val := Nat.succ j', isLt := h }) (Array.get a { val := j', isLt := h' }) = true then
+          Array.insertionSort.swapLoop lt (Array.swap a { val := Nat.succ j', isLt := h } { val := j', isLt := h' }) j'
+            (_ : j' < Array.size (Array.swap a { val := Nat.succ j', isLt := h } { val := j', isLt := h' }))
+        else a)
+      (_ : j' < Array.size a)