fix: an equation lemma with autoParam arguments fails to rewrite (#…

…3316)

closes #2243

src/Lean/Elab/PreDefinition/Structural/Eqns.lean

@@ -57,7 +57,7 @@ where
 
 def mkEqns (info : EqnInfo) : MetaM (Array Name) :=
   withOptions (tactic.hygienic.set · false) do
-  let eqnTypes ← withNewMCtxDepth <| lambdaTelescope info.value fun xs body => do
+  let eqnTypes ← withNewMCtxDepth <| lambdaTelescope (cleanupAnnotations := true) info.value fun xs body => do
     let us := info.levelParams.map mkLevelParam
     let target ← mkEq (mkAppN (Lean.mkConst info.declName us) xs) body
     let goal ← mkFreshExprSyntheticOpaqueMVar target

src/Lean/Elab/PreDefinition/WF/Eqns.lean

@@ -107,7 +107,7 @@ private partial def mkProof (declName : Name) (type : Expr) : MetaM Expr := do
 def mkEqns (declName : Name) (info : EqnInfo) : MetaM (Array Name) :=
   withOptions (tactic.hygienic.set · false) do
   let baseName := mkPrivateName (← getEnv) declName
-  let eqnTypes ← withNewMCtxDepth <| lambdaTelescope info.value fun xs body => do
+  let eqnTypes ← withNewMCtxDepth <| lambdaTelescope (cleanupAnnotations := true) info.value fun xs body => do
     let us := info.levelParams.map mkLevelParam
     let target ← mkEq (mkAppN (Lean.mkConst declName us) xs) body
     let goal ← mkFreshExprSyntheticOpaqueMVar target

src/Lean/Meta/Basic.lean

@@ -1084,19 +1084,21 @@ private def forallBoundedTelescopeImp (type : Expr) (maxFVars? : Option Nat) (k
 def forallBoundedTelescope (type : Expr) (maxFVars? : Option Nat) (k : Array Expr → Expr → n α) : n α :=
   map2MetaM (fun k => forallBoundedTelescopeImp type maxFVars? k) k
 
-private partial def lambdaTelescopeImp (e : Expr) (consumeLet : Bool) (k : Array Expr → Expr → MetaM α) : MetaM α := do
+private partial def lambdaTelescopeImp (e : Expr) (consumeLet : Bool) (k : Array Expr → Expr → MetaM α) (cleanupAnnotations := false) : MetaM α := do
   process consumeLet (← getLCtx) #[] 0 e
 where
   process (consumeLet : Bool) (lctx : LocalContext) (fvars : Array Expr) (j : Nat) (e : Expr) : MetaM α := do
     match consumeLet, e with
     | _, .lam n d b bi =>
       let d := d.instantiateRevRange j fvars.size fvars
+      let d := if cleanupAnnotations then d.cleanupAnnotations else d
       let fvarId ← mkFreshFVarId
       let lctx := lctx.mkLocalDecl fvarId n d bi
       let fvar := mkFVar fvarId
       process consumeLet lctx (fvars.push fvar) j b
     | true, .letE n t v b _ => do
       let t := t.instantiateRevRange j fvars.size fvars
+      let t := if cleanupAnnotations then t.cleanupAnnotations else t
       let v := v.instantiateRevRange j fvars.size fvars
       let fvarId ← mkFreshFVarId
       let lctx := lctx.mkLetDecl fvarId n t v
@@ -1108,16 +1110,23 @@ where
         withNewLocalInstancesImp fvars j do
           k fvars e
 
-/-- Similar to `lambdaTelescope` but for lambda and let expressions. -/
-def lambdaLetTelescope (e : Expr) (k : Array Expr → Expr → n α) : n α :=
-  map2MetaM (fun k => lambdaTelescopeImp e true k) k
+/--
+Similar to `lambdaTelescope` but for lambda and let expressions.
+
+If `cleanupAnnotations` is `true`, we apply `Expr.cleanupAnnotations` to each type in the telescope.
+-/
+def lambdaLetTelescope (e : Expr) (k : Array Expr → Expr → n α) (cleanupAnnotations := false) : n α :=
+  map2MetaM (fun k => lambdaTelescopeImp e true k (cleanupAnnotations := cleanupAnnotations)) k
 
 /--
   Given `e` of the form `fun ..xs => A`, execute `k xs A`.
   This combinator will declare local declarations, create free variables for them,
-  execute `k` with updated local context, and make sure the cache is restored after executing `k`. -/
-def lambdaTelescope (e : Expr) (k : Array Expr → Expr → n α) : n α :=
-  map2MetaM (fun k => lambdaTelescopeImp e false k) k
+  execute `k` with updated local context, and make sure the cache is restored after executing `k`.
+
+  If `cleanupAnnotations` is `true`, we apply `Expr.cleanupAnnotations` to each type in the telescope.
+-/
+def lambdaTelescope (e : Expr) (k : Array Expr → Expr → n α) (cleanupAnnotations := false) : n α :=
+  map2MetaM (fun k => lambdaTelescopeImp e false k (cleanupAnnotations := cleanupAnnotations)) k
 
 /-- Return the parameter names for the given global declaration. -/
 def getParamNames (declName : Name) : MetaM (Array Name) := do

src/Lean/Meta/Eqns.lean

@@ -62,7 +62,7 @@ builtin_initialize eqnsExt : EnvExtension EqnsExtState ←
 -/
 private def mkSimpleEqThm (declName : Name) : MetaM (Option Name) := do
   if let some (.defnInfo info) := (← getEnv).find? declName then
-    lambdaTelescope info.value fun xs body => do
+    lambdaTelescope (cleanupAnnotations := true) info.value fun xs body => do
       let lhs := mkAppN (mkConst info.name <| info.levelParams.map mkLevelParam) xs
       let type  ← mkForallFVars xs (← mkEq lhs body)
       let value ← mkLambdaFVars xs (← mkEqRefl lhs)

tests/lean/run/2243.lean

@@ -0,0 +1,35 @@
+import Lean
+
+open Lean Elab Tactic in
+elab "exact_false" : tactic =>
+  closeMainGoal (mkConst ``Bool.false)
+
+def f (b : Bool := by exact_false) : Nat := bif b then 1 else 0
+
+example : f false = bif false then 1 else 0 := by rw [f]
+example : f true = bif true then 1 else 0 := by rw [f]
+example (b : Bool) : f b = bif b then 1 else 0 := by rw [f]
+
+def g (x : Nat) (b : Bool := by exact_false) : Nat :=
+  match x with
+  | 0 => bif b then 1 else 0
+  | x+1 => g x b + 1
+
+example : g (x+1) true = g x true + 1 := by rw [g]
+example : g (x+1) false = g x false + 1 := by rw [g]
+example : g (x+1) = g x false + 1 := by rw [g]
+example : g (x+1) b = g x b + 1 := by rw [g]
+
+def foo (x n : Nat) (b : Bool := by exact_false) : Nat :=
+  if _ : x < n then
+    foo (x+1) n b + 1
+  else
+    g x b
+termination_by n - x
+
+example : foo x n true = if _ : x < n then foo (x+1) n true + 1 else g x true := by
+  rw [foo]
+example : foo x n b = if _ : x < n then foo (x+1) n b + 1 else g x b := by
+  rw [foo]
+example : foo x n false = if _ : x < n then foo (x+1) n false + 1 else g x false := by
+  rw [foo]

tests/lean/run/2939.lean

@@ -0,0 +1,3 @@
+def foo (x := 0) : Nat := x
+example : foo x = x := by simp only [foo] -- ok
+example : foo x = x := by rw [foo]