feat: unify equational theorems between wf and structural recursion (#…

…5055) by removing the `tryRefl` variation between the two. Part of #3983
leanprover · Aug 19, 2024 · b4db495 · b4db495
1 parent 9f47e08
commit b4db495
Show file tree

Hide file tree

Showing 4 changed files with 4 additions and 9 deletions.
diff --git a/src/Lean/Elab/PreDefinition/Eqns.lean b/src/Lean/Elab/PreDefinition/Eqns.lean
@@ -228,16 +228,12 @@ private def shouldUseSimpMatch (e : Expr) : MetaM Bool := do
             throwThe Unit ()
   return (← (find e).run) matches .error _
 
-partial def mkEqnTypes (tryRefl : Bool) (declNames : Array Name) (mvarId : MVarId) : MetaM (Array Expr) := do
+partial def mkEqnTypes (declNames : Array Name) (mvarId : MVarId) : MetaM (Array Expr) := do
   let (_, eqnTypes) ← go mvarId |>.run { declNames } |>.run #[]
   return eqnTypes
 where
   go (mvarId : MVarId) : ReaderT Context (StateRefT (Array Expr) MetaM) Unit := do
     trace[Elab.definition.eqns] "mkEqnTypes step\n{MessageData.ofGoal mvarId}"
-    if tryRefl then
-      if (← tryURefl mvarId) then
-        saveEqn mvarId
-        return ()
 
     if let some mvarId ← expandRHS? mvarId then
       return (← go mvarId)

diff --git a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean b/src/Lean/Elab/PreDefinition/Structural/Eqns.lean
@@ -64,7 +64,7 @@ def mkEqns (info : EqnInfo) : MetaM (Array Name) :=
     let us := info.levelParams.map mkLevelParam
     let target ← mkEq (mkAppN (Lean.mkConst info.declName us) xs) body
     let goal ← mkFreshExprSyntheticOpaqueMVar target
-    mkEqnTypes (tryRefl := true) info.declNames goal.mvarId!
+    mkEqnTypes info.declNames goal.mvarId!
   let baseName := info.declName
   let mut thmNames := #[]
   for i in [: eqnTypes.size] do

diff --git a/src/Lean/Elab/PreDefinition/WF/Eqns.lean b/src/Lean/Elab/PreDefinition/WF/Eqns.lean
@@ -81,7 +81,7 @@ def mkEqns (declName : Name) (info : EqnInfo) : MetaM (Array Name) :=
     let target ← mkEq (mkAppN (Lean.mkConst declName us) xs) body
     let goal ← mkFreshExprSyntheticOpaqueMVar target
     withReducible do
-      mkEqnTypes (tryRefl := false) info.declNames goal.mvarId!
+      mkEqnTypes info.declNames goal.mvarId!
   let mut thmNames := #[]
   for i in [: eqnTypes.size] do
     let type := eqnTypes[i]!

diff --git a/tests/lean/run/986.lean b/tests/lean/run/986.lean
@@ -11,8 +11,7 @@ info: Array.insertionSort.swapLoop.eq_1.{u_1} {α : Type u_1} (lt : α → α
 info: Array.insertionSort.swapLoop.eq_2.{u_1} {α : Type u_1} (lt : α → α → Bool) (a : Array α) (j' : Nat)
   (h : j'.succ < a.size) :
   Array.insertionSort.swapLoop lt a j'.succ h =
-    let_fun h' := ⋯;
-    if lt a[j'.succ] a[j'] = true then Array.insertionSort.swapLoop lt (a.swap ⟨j'.succ, h⟩ ⟨j', h'⟩) j' ⋯ else a
+    if lt a[j'.succ] a[j'] = true then Array.insertionSort.swapLoop lt (a.swap ⟨j'.succ, h⟩ ⟨j', ⋯⟩) j' ⋯ else a
 -/
 #guard_msgs in
 #check Array.insertionSort.swapLoop.eq_2