From 9fe0d28107f7c6c0626cfb996d02ced8a4664c99 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 9 Feb 2022 17:43:35 -0800
Subject: [PATCH] fix: do not split on if-then-else terms when generating
 equation theorems

Reason: avoid unnecessary case-analysis explosion
It is also unnecessary since we only refine the `below` and `F`
arguments over `match`-expressions.

This fixes the last case at issue #998
```
attribute [simp] BinaryHeap.heapifyDown
```

closes #998
---
 src/Lean/Elab/PreDefinition/Eqns.lean | 4 ++--
 tests/lean/run/heapSort.lean          | 2 ++
 tests/lean/run/structuralEqns2.lean   | 1 -
 tests/lean/run/wfEqns2.lean           | 1 -
 4 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Lean/Elab/PreDefinition/Eqns.lean b/src/Lean/Elab/PreDefinition/Eqns.lean
index 2298f89163..230c925618 100644
--- a/src/Lean/Elab/PreDefinition/Eqns.lean
+++ b/src/Lean/Elab/PreDefinition/Eqns.lean
@@ -154,7 +154,7 @@ where
       go mvarId
     else if let some mvarId ← simpMatch? mvarId then
       go mvarId
-    else if let some mvarIds ← splitTarget? mvarId then
+    else if let some mvarIds ← splitTarget? mvarId (splitIte := false) then
       mvarIds.forM go
     else
       saveEqn mvarId
@@ -239,7 +239,7 @@ partial def mkUnfoldProof (declName : Name) (mvarId : MVarId) : MetaM Unit := do
       go mvarId
     else if let some mvarId ← simpMatch? mvarId then
       go mvarId
-    else if let some mvarIds ← splitTarget? mvarId then
+    else if let some mvarIds ← splitTarget? mvarId (splitIte := false) then
       mvarIds.forM go
     else
      throwError "failed to generate unfold theorem for '{declName}'\n{MessageData.ofGoal mvarId}"
diff --git a/tests/lean/run/heapSort.lean b/tests/lean/run/heapSort.lean
index 1b8f2db02a..34a8b68ffe 100644
--- a/tests/lean/run/heapSort.lean
+++ b/tests/lean/run/heapSort.lean
@@ -174,3 +174,5 @@ decreasing_by assumption
 
 attribute [simp] Array.heapSort.loop
 #check @Array.heapSort.loop._eq_1
+
+attribute [simp] BinaryHeap.heapifyDown
diff --git a/tests/lean/run/structuralEqns2.lean b/tests/lean/run/structuralEqns2.lean
index bb96df04cf..4d9d9a1fac 100644
--- a/tests/lean/run/structuralEqns2.lean
+++ b/tests/lean/run/structuralEqns2.lean
@@ -14,7 +14,6 @@ def g (i j : Nat) : Nat :=
 #eval tst ``g
 #check g._eq_1
 #check g._eq_2
-#check g._eq_3
 #check g._unfold
 
 def h (i j : Nat) : Nat :=
diff --git a/tests/lean/run/wfEqns2.lean b/tests/lean/run/wfEqns2.lean
index e9c08f9e8c..af26806193 100644
--- a/tests/lean/run/wfEqns2.lean
+++ b/tests/lean/run/wfEqns2.lean
@@ -33,7 +33,6 @@ decreasing_by
 #eval tst ``g
 #check g._eq_1
 #check g._eq_2
-#check g._eq_3
 #check g._unfold
 #eval tst ``h
 #check h._eq_1