From e53952f1674af5ac8f6bdfb5e1e28f3f10015ecd Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sun, 29 Oct 2023 10:14:54 -0700
Subject: [PATCH] chore: fix tests

---
 tests/lean/matchPatternPartialApp.lean  | 2 +-
 tests/lean/mutwf1.lean                  | 2 +-
 tests/lean/run/discrTreeSimp.lean       | 3 ++-
 tests/lean/run/mutwf3.lean              | 2 +-
 tests/lean/run/setOptionTermTactic.lean | 6 +++---
 tests/lean/run/wfEqns2.lean             | 2 +-
 tests/lean/run/wfEqns4.lean             | 2 +-
 tests/lean/simpZetaFalse.lean           | 2 +-
 tests/lean/simp_trace.lean              | 2 +-
 tests/lean/simp_trace.lean.expected.out | 4 ++--
 10 files changed, 14 insertions(+), 13 deletions(-)

diff --git a/tests/lean/matchPatternPartialApp.lean b/tests/lean/matchPatternPartialApp.lean
index f3b634dc6b..a8bcc50b28 100644
--- a/tests/lean/matchPatternPartialApp.lean
+++ b/tests/lean/matchPatternPartialApp.lean
@@ -1,5 +1,5 @@
 def test2 : (Function.comp id id) = λ x : Nat => x := by
   conv in (Function.comp _) =>
     trace_state
-    simp [Function.comp, id]
+    simp (config := { unfoldPartialApp := true }) [Function.comp, id]
     trace_state
diff --git a/tests/lean/mutwf1.lean b/tests/lean/mutwf1.lean
index aa7886e1cb..16488d6658 100644
--- a/tests/lean/mutwf1.lean
+++ b/tests/lean/mutwf1.lean
@@ -19,7 +19,7 @@ termination_by'
      | PSum.inr n => (n, 0))
   $ Prod.lex sizeOfWFRel sizeOfWFRel
 decreasing_by
-  simp [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel, WellFoundedRelation.rel]
+  simp_wf
   first
   | apply Prod.Lex.left
     apply Nat.pred_lt
diff --git a/tests/lean/run/discrTreeSimp.lean b/tests/lean/run/discrTreeSimp.lean
index 1e2c1b377f..3c50f95921 100644
--- a/tests/lean/run/discrTreeSimp.lean
+++ b/tests/lean/run/discrTreeSimp.lean
@@ -1,4 +1,5 @@
 prelude
+import Init.MetaTypes
 import Init.Data.List.Basic
 
 @[simp] theorem map_comp_map (f : α → β) (g : β → γ) : List.map g ∘ List.map f = List.map (g ∘ f) :=
@@ -18,4 +19,4 @@ theorem ex2 (f : Nat → Nat) : List.map f ∘ List.map f ∘ List.map f = List.
 attribute [simp] map_map
 
 theorem ex3 (f : Nat → Nat) (xs : List Nat) : (xs.map f |>.map f |>.map f) = xs.map (fun x => f (f (f x))) := by
-  simp [Function.comp]
+  simp (config := { unfoldPartialApp := true }) [Function.comp]
diff --git a/tests/lean/run/mutwf3.lean b/tests/lean/run/mutwf3.lean
index af9b12a531..05af6cdd4f 100644
--- a/tests/lean/run/mutwf3.lean
+++ b/tests/lean/run/mutwf3.lean
@@ -20,7 +20,7 @@ termination_by'
       | PSum.inr <| PSum.inr ⟨_, _, n⟩ => (n, 0))
     (Prod.lex sizeOfWFRel sizeOfWFRel)
 decreasing_by
-  simp [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel, WellFoundedRelation.rel]
+  simp_wf
   first
   | apply Prod.Lex.left
     apply Nat.lt_succ_self
diff --git a/tests/lean/run/setOptionTermTactic.lean b/tests/lean/run/setOptionTermTactic.lean
index 8089af352a..da6b6cdd59 100644
--- a/tests/lean/run/setOptionTermTactic.lean
+++ b/tests/lean/run/setOptionTermTactic.lean
@@ -4,6 +4,6 @@ def f (x : Nat) : Nat :=
 def g (x : Nat) : Nat := 0 + x.succ
 
 theorem ex : f = g := by
-  simp only [f]
-  set_option trace.Meta.Tactic.simp true in simp only [Nat.add_succ, g]
-  simp only [Nat.zero_add]
+  simp (config := { unfoldPartialApp := true }) only [f]
+  set_option trace.Meta.Tactic.simp true in simp (config := { unfoldPartialApp := true }) only [Nat.add_succ, g]
+  simp (config := { unfoldPartialApp := true }) only [Nat.zero_add]
diff --git a/tests/lean/run/wfEqns2.lean b/tests/lean/run/wfEqns2.lean
index 72c36784ef..80228ba917 100644
--- a/tests/lean/run/wfEqns2.lean
+++ b/tests/lean/run/wfEqns2.lean
@@ -23,7 +23,7 @@ termination_by'
       | PSum.inr n => (n, 1))
     (Prod.lex sizeOfWFRel sizeOfWFRel)
 decreasing_by
-  simp [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel, WellFoundedRelation.rel]
+  simp_wf
   first
   | apply Prod.Lex.left
     apply Nat.lt_succ_self
diff --git a/tests/lean/run/wfEqns4.lean b/tests/lean/run/wfEqns4.lean
index f2104eadab..2e42ca81cf 100644
--- a/tests/lean/run/wfEqns4.lean
+++ b/tests/lean/run/wfEqns4.lean
@@ -26,7 +26,7 @@ termination_by'
       | PSum.inr <| PSum.inr ⟨_, _, n⟩ => (n, 0))
     (Prod.lex sizeOfWFRel sizeOfWFRel)
 decreasing_by
-  simp [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel, WellFoundedRelation.rel]
+  simp_wf
   first
   | apply Prod.Lex.left
     apply Nat.lt_succ_self
diff --git a/tests/lean/simpZetaFalse.lean b/tests/lean/simpZetaFalse.lean
index e4a92a94bf..04ec4bbe28 100644
--- a/tests/lean/simpZetaFalse.lean
+++ b/tests/lean/simpZetaFalse.lean
@@ -18,7 +18,7 @@ theorem ex2 (x z : Nat) (h : f (f x) = x) (h' : z = x) : (let y := f (f x); y) =
 theorem ex3 (x z : Nat) : (let α := Nat; (fun x : α => 0 + x)) = id := by
   simp (config := { zeta := false, failIfUnchanged := false })
   trace_state -- should not simplify let body since `fun α : Nat => fun x : α => 0 + x` is not type correct
-  simp [id]
+  simp (config := { unfoldPartialApp := true }) [id]
 
 theorem ex4 (p : Prop) (h : p) : (let n := 10; fun x : { z : Nat // z < n } => x = x) = fun z => p := by
   simp (config := { zeta := false })
diff --git a/tests/lean/simp_trace.lean b/tests/lean/simp_trace.lean
index 54cb70de89..f879cfa0ce 100644
--- a/tests/lean/simp_trace.lean
+++ b/tests/lean/simp_trace.lean
@@ -59,7 +59,7 @@ def f2 : StateM Nat Unit := do
 -- Note: prior to PR #2489, the `Try this` suggestion reported by this `simp`
 -- call was incomplete.
 example : f1 = f2 := by
-  simp [f1, f2, bind, StateT.bind, get, getThe, MonadStateOf.get, StateT.get, pure, set, StateT.set, modify, modifyGet, MonadStateOf.modifyGet, StateT.modifyGet]
+  simp (config := {unfoldPartialApp := true}) [f1, f2, bind, StateT.bind, get, getThe, MonadStateOf.get, StateT.get, pure, set, StateT.set, modify, modifyGet, MonadStateOf.modifyGet, StateT.modifyGet]
 
 def h (x : Nat) : Sum (Nat × Nat) Nat := Sum.inl (x, x)
 
diff --git a/tests/lean/simp_trace.lean.expected.out b/tests/lean/simp_trace.lean.expected.out
index 4e66a9dad0..febf277f79 100644
--- a/tests/lean/simp_trace.lean.expected.out
+++ b/tests/lean/simp_trace.lean.expected.out
@@ -19,8 +19,8 @@ Try this: simp only [g, Id.pure_eq]
       (let x := x;
       pure x)
 [Meta.Tactic.simp.rewrite] @Id.pure_eq:1000, pure x ==> x
-Try this: simp only [f1, modify, modifyGet, MonadStateOf.modifyGet, StateT.modifyGet, pure, f2, bind, StateT.bind, get,
-  getThe, MonadStateOf.get, StateT.get, set, StateT.set]
+Try this: simp (config := { unfoldPartialApp := true }) only [f1, modify, modifyGet, MonadStateOf.modifyGet,
+  StateT.modifyGet, pure, f2, bind, StateT.bind, get, getThe, MonadStateOf.get, StateT.get, set, StateT.set]
 [Meta.Tactic.simp.rewrite] unfold f1, f1 ==> modify fun x => g x
 [Meta.Tactic.simp.rewrite] unfold modify, modify fun x => g x ==> modifyGet fun s => (PUnit.unit, (fun x => g x) s)
 [Meta.Tactic.simp.rewrite] unfold StateT.modifyGet, StateT.modifyGet fun s =>