fix: issue 2042

RELEASES.md

@@ -41,6 +41,9 @@ v4.3.0
 * The `:=` syntax for configuration declarations (i.e., `package`, `lean_lib`, and `lean_exe`) has been deprecated. For example, `package foo := {...}` is deprecated.
 * [support for overriding package URLs via `LAKE_PKG_URL_MAP`](https://github.com/leanprover/lean4/pull/2709)
 
+* `simp [f]` does not unfold partial applications of `f` anymore. See issue [#2042](https://github.com/leanprover/lean4/issues/2042).
+  To fix proofs affected by this change, use `unfold f` or `simp (config := { unfoldPartialApp := true }) [f]`.
+
 v4.2.0
 ---------
 

src/Lean/Expr.lean

@@ -1332,6 +1332,14 @@ lambda expression. See docstring for `betaRev` for examples.
 def beta (f : Expr) (args : Array Expr) : Expr :=
   betaRev f args.reverse
 
+/--
+Count the number of lambdas at the head of the given expression.
+-/
+def getNumHeadLambdas : Expr → Nat
+  | .lam _ _ b _ => getNumHeadLambdas b + 1
+  | .mdata _ b => getNumHeadLambdas b
+  | _ => 0
+
 /--
 Return true if the given expression is the function of an expression that is target for (head) beta reduction.
 If `useZeta = true`, then `let`-expressions are visited. That is, it assumes

src/Lean/Meta/Tactic/Simp/Main.lean

@@ -194,6 +194,23 @@ private def unfold? (e : Expr) : SimpM (Option Expr) := do
       if eNew == e then return none
       trace[Meta.Tactic.simp.ground] "{e}\n---->\n{eNew}"
       return some eNew
+  let rec unfoldDeclToUnfold? : SimpM (Option Expr) := do
+    let options ← getOptions
+    let cfg ← getConfig
+    -- Support for issue #2042
+    if cfg.unfoldPartialApp -- If we are unfolding partial applications, ignore issue #2042
+       -- When smart unfolding is enabled, and `f` supports it, we don't need to worry about issue #2042
+       || (smartUnfolding.get options && (← getEnv).contains (mkSmartUnfoldingNameFor fName)) then
+      withDefault <| unfoldDefinition? e
+    else
+      -- `We are not unfolding partial applications, and `fName` does not have smart unfolding support.
+      -- Thus, we must check whether the arity of the function >= number of arguments.
+      let some cinfo := (← getEnv).find? fName | return none
+      let some value := cinfo.value? | return none
+      let arity := value.getNumHeadLambdas
+      -- Partially applied function, return `none`. See issue #2042
+      if arity > e.getAppNumArgs then return none
+      withDefault <| unfoldDefinition? e
   if let some eNew ← unfoldGround? then
     return some eNew
   else if (← isProjectionFn fName) then
@@ -210,7 +227,7 @@ private def unfold? (e : Expr) : SimpM (Option Expr) := do
     else
       return none
   else if ctx.isDeclToUnfold fName then
-    withDefault <| unfoldDefinition? e
+    unfoldDeclToUnfold?
   else
     return none
 
@@ -352,18 +369,18 @@ where
 
   simpStep (e : Expr) : M Result := do
     match e with
-    | Expr.mdata m e   => let r ← simp e; return { r with expr := mkMData m r.expr }
-    | Expr.proj ..     => simpProj e
-    | Expr.app ..      => simpApp e
-    | Expr.lam ..      => simpLambda e
-    | Expr.forallE ..  => simpForall e
-    | Expr.letE ..     => simpLet e
-    | Expr.const ..    => simpConst e
-    | Expr.bvar ..     => unreachable!
-    | Expr.sort ..     => return { expr := e }
-    | Expr.lit ..      => simpLit e
-    | Expr.mvar ..     => return { expr := (← instantiateMVars e) }
-    | Expr.fvar ..     => return { expr := (← reduceFVar (← getConfig) (← getSimpTheorems) e) }
+    | .mdata m e   => let r ← simp e; return { r with expr := mkMData m r.expr }
+    | .proj ..     => simpProj e
+    | .app ..      => simpApp e
+    | .lam ..      => simpLambda e
+    | .forallE ..  => simpForall e
+    | .letE ..     => simpLet e
+    | .const ..    => simpConst e
+    | .bvar ..     => unreachable!
+    | .sort ..     => return { expr := e }
+    | .lit ..      => simpLit e
+    | .mvar ..     => return { expr := (← instantiateMVars e) }
+    | .fvar ..     => return { expr := (← reduceFVar (← getConfig) (← getSimpTheorems) e) }
 
   simpLit (e : Expr) : M Result := do
     match e.natLit? with
@@ -766,7 +783,7 @@ where
       return { expr := (← dsimp e) }
 
   simpLet (e : Expr) : M Result := do
-    let Expr.letE n t v b _ := e | unreachable!
+    let .letE n t v b _ := e | unreachable!
     if (← getConfig).zeta then
       return { expr := b.instantiate1 v }
     else

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

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

tests/lean/run/2042.lean

@@ -0,0 +1,21 @@
+@[simp] def foo (a : Nat) : Nat :=
+  2 * a
+
+example : foo = fun a => a + a :=
+by
+  fail_if_success simp -- should not unfold `foo` into a lambda
+  funext x
+  simp -- unfolds `foo`
+  trace_state
+  simp_arith
+
+@[simp] def boo : Nat → Nat
+  | a => 2 * a
+
+example : boo = fun a => a + a :=
+by
+  fail_if_success simp -- should not unfold `boo` into a lambda
+  funext x
+  simp -- unfolds `boo`
+  trace_state
+  simp_arith

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]

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

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]

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

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

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 })

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)
 

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 =>