From dba1f791701d07a936f3ebb77854eadabedf5fac Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 30 Jun 2022 17:00:43 -0700
Subject: [PATCH] feat: improve `isDefEq` for projections

When solving `a.i =?= b.i`, we first reduce `a` and `b` without using
delta reduction. If at least one become a structure, we reduce the
projection. Otherwise, we try to solve `a =?= b`, only reduce `a.i`
and `b.i` if it fails.
---
 src/Lean/Meta/ExprDefEq.lean | 38 +++++++++++++++++++++---------------
 1 file changed, 22 insertions(+), 16 deletions(-)

diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index a1a05173bb5..ae3e8f763f5 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -1588,22 +1588,27 @@ private def isDefEqUnitLike (t : Expr) (s : Expr) : MetaM Bool := do
       return false
 
 private def isExprDefEqExpensive (t : Expr) (s : Expr) : MetaM Bool := do
-  if (← (isDefEqEta t s <||> isDefEqEta s t)) then pure true else
+  if (← (isDefEqEta t s <||> isDefEqEta s t)) then return true
   -- TODO: investigate whether this is the place for putting this check
-  if (← (isDefEqEtaStruct t s <||> isDefEqEtaStruct s t)) then pure true else
-  if (← isDefEqProj t s) then pure true else
-  whenUndefDo (isDefEqNative t s) do
-  whenUndefDo (isDefEqNat t s) do
-  whenUndefDo (isDefEqOffset t s) do
-  whenUndefDo (isDefEqDelta t s) do
-  if t.isConst && s.isConst then
-    if t.constName! == s.constName! then isListLevelDefEqAux t.constLevels! s.constLevels! else return false
-  else if (← pure t.isApp <&&> pure s.isApp <&&> isDefEqApp t s) then
-    return true
+  if (← (isDefEqEtaStruct t s <||> isDefEqEtaStruct s t)) then return true
+  if (← isDefEqProj t s) then return true
+  let t' ← whnfCore t
+  let s' ← whnfCore s
+  if t != t' || s != s' then
+    Meta.isExprDefEqAux t' s'
   else
-    whenUndefDo (isDefEqStringLit t s) do
-    if (← isDefEqUnitLike t s) then return true else
-    isDefEqOnFailure t s
+    whenUndefDo (isDefEqNative t s) do
+    whenUndefDo (isDefEqNat t s) do
+    whenUndefDo (isDefEqOffset t s) do
+    whenUndefDo (isDefEqDelta t s) do
+    if t.isConst && s.isConst then
+      if t.constName! == s.constName! then isListLevelDefEqAux t.constLevels! s.constLevels! else return false
+    else if (← pure t.isApp <&&> pure s.isApp <&&> isDefEqApp t s) then
+      return true
+    else
+      whenUndefDo (isDefEqStringLit t s) do
+      if (← isDefEqUnitLike t s) then return true else
+      isDefEqOnFailure t s
 
 -- We only check DefEq cache for default and all transparency modes
 private def skipDefEqCache : MetaM Bool := do
@@ -1635,8 +1640,9 @@ partial def isExprDefEqAuxImpl (t : Expr) (s : Expr) : MetaM Bool := withIncRecD
   withNestedTraces do
   whenUndefDo (isDefEqQuick t s) do
   whenUndefDo (isDefEqProofIrrel t s) do
-  let t' ← whnfCore t
-  let s' ← whnfCore s
+  -- We perform `whnfCore` again with `deltaAtProj := true` at `isExprDefEqExpensive` after `isDefEqProj`
+  let t' ← whnfCore t (deltaAtProj := false)
+  let s' ← whnfCore s (deltaAtProj := false)
   if t != t' || s != s' then
     isExprDefEqAuxImpl t' s'
   else if (← skipDefEqCache) then