fix: mkEqnTypes

stop as soon as `lhs` and `rhs` are definitionally equal, and avoid
unnecessary case analysis.

This commit fixes the last issue exposed by #1074

fixes #1074

src/Lean/Elab/PreDefinition/Eqns.lean

@@ -89,6 +89,11 @@ private def lhsDependsOn (type : Expr) (fvarId : FVarId) : MetaM Bool :=
     else
       dependsOn type fvarId
 
+/-- Try to close goal using `rfl` with smart unfolding turned off. -/
+def tryURefl (mvarId : MVarId) : MetaM Bool :=
+  withOptions (smartUnfolding.set · false) do
+    try applyRefl mvarId; return true catch _ => return false
+
 /--
   Eliminate `namedPatterns` from equation, and trivial hypotheses.
 -/
@@ -203,6 +208,10 @@ partial def mkEqnTypes (declNames : Array Name) (mvarId : MVarId) : MetaM (Array
 where
   go (mvarId : MVarId) : ReaderT Context (StateRefT (Array Expr) MetaM) Unit := do
     trace[Elab.definition.structural.eqns] "mkEqnTypes step\n{MessageData.ofGoal mvarId}"
+    if (← tryURefl mvarId) then
+      saveEqn mvarId
+      return ()
+
     if let some mvarId ← expandRHS? mvarId then
       return (← go mvarId)
 --  The following `funext?` was producing an overapplied `lhs`. Possible refinement: only do it if we want to apply `splitMatch` on the body of the lambda
@@ -249,11 +258,6 @@ where
         xsNew := xsNew.reverse
         return (lctx.mkForall xsNew type, lctx.mkLambda xsNew value)
 
-/-- Try to close goal using `rfl` with smart unfolding turned off. -/
-def tryURefl (mvarId : MVarId) : MetaM Bool :=
-  withOptions (smartUnfolding.set · false) do
-    try applyRefl mvarId; return true catch _ => return false
-
 /-- Delta reduce the equation left-hand-side -/
 def deltaLHS (mvarId : MVarId) : MetaM MVarId := withMVarContext mvarId do
   let target ← getMVarType' mvarId

tests/lean/1074a.lean

@@ -0,0 +1,21 @@
+inductive Term
+| id2: Term -> Term -> Term
+
+inductive Brx: Term -> Prop
+| id2: Brx z -> Brx (Term.id2 n z)
+
+def Brx.interp {a} (H: Brx a): Nat :=
+  match a with
+  | Term.id2 n z => by
+    let ⟨Hn, Hz⟩: True ∧ Brx z
+      := by cases H <;> exact ⟨by simp, by assumption⟩;
+    exact Hz.interp
+
+def Brx.interp_nil (H: Brx a): H.interp = H.interp
+  :=
+  by {
+    unfold interp
+    rfl
+  }
+
+#check Brx.interp._eq_1

tests/lean/1074a.lean.expected.out

@@ -0,0 +1,5 @@
+Brx.interp._eq_1 : ∀ (n z : Term) (H_2 : Brx (Term.id2 n z)),
+  Brx.interp H_2 =
+    let x := (_ : True ∧ Brx z);
+    match x with
+    | (_ : True ∧ Brx z) => Brx.interp Hz

tests/lean/986.lean.expected.out

@@ -3,9 +3,8 @@
 @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)
+    let_fun h' := (_ : j' < Array.size a);
+    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

tests/lean/run/structuralEqns.lean

@@ -53,7 +53,6 @@ def h (xs : List Nat) (y : Nat) : Nat :=
 #eval tst ``h
 #check h._eq_1
 #check h._eq_2
-#check h._eq_3
 #check h._unfold
 
 def r (i j : Nat) : Nat :=