Revert "Maybe in two steps?"

This reverts commit 0d64516.
leanprover · Feb 6, 2025 · ca8ae18 · ca8ae18
1 parent 0d64516
commit ca8ae18
Showing 1 changed file with 16 additions and 20 deletions.
diff --git a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean b/src/Lean/Elab/PreDefinition/Structural/Eqns.lean
@@ -32,39 +32,35 @@ private partial def mkProof (declName : Name) (unfold : MVarId → MetaM MVarId)
     let main ← mkFreshExprSyntheticOpaqueMVar type
     let (_, mvarId) ← main.mvarId!.intros
     unless (← tryURefl mvarId) do -- catch easy cases
-      go1 mvarId
+      go (← unfold mvarId)
     instantiateMVars main
 where
-  go1 (mvarId : MVarId) : MetaM Unit := do
-    trace[Elab.definition.structural.eqns] "go1\n{MessageData.ofGoal mvarId}"
-    if let some mvarId ← simpIf? mvarId then
-      go1 mvarId
-    else if let some mvarId ← deltaRHS? mvarId declName then
-      go1 mvarId
-    else if let some mvarIds ← splitTarget? mvarId then
-      mvarIds.forM go1
-    else
-      go2 (← unfold mvarId)
-
-
-  go2 (mvarId : MVarId) : MetaM Unit := do
-    trace[Elab.definition.structural.eqns] "go2\n{MessageData.ofGoal mvarId}"
+  go (mvarId : MVarId) : MetaM Unit := do
+    trace[Elab.definition.structural.eqns] "step\n{MessageData.ofGoal mvarId}"
     if (← tryURefl mvarId) then
       return ()
     else if (← tryContradiction mvarId) then
       return ()
     else if let some mvarId ← simpMatch? mvarId then
-      go2 mvarId
+      go mvarId
+    else if let some mvarId ← simpIf? mvarId then
+      go mvarId
     else
       let ctx ← Simp.mkContext (config := { iota := false })
       match (← simpTargetStar mvarId ctx (simprocs := {})).1 with
       | TacticResultCNM.closed => return ()
-      | TacticResultCNM.modified mvarId => go2 mvarId
+      | TacticResultCNM.modified mvarId => go mvarId
       | TacticResultCNM.noChange =>
-        if let some mvarIds ← casesOnStuckLHS? mvarId then
-          mvarIds.forM go2
+        if let some mvarId ← deltaRHS? mvarId declName then
+          go mvarId
+        -- The order of the following two cases is crucial, and I have not yet found
+        -- one that works for all test cases. Needs more thought.
+        else if let some mvarIds ← casesOnStuckLHS? mvarId then
+          mvarIds.forM go
+        else if let some mvarIds ← splitTarget? mvarId then
+          mvarIds.forM go
         else if let some mvarId ← whnfReducibleLHS? mvarId then
-          go2 mvarId
+          go mvarId
         else
           throwError "failed to generate equational theorem for '{declName}'\n{MessageData.ofGoal mvarId}"