From ef9a6bb839c9f3e8d301a5291d2e785f869735fc Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 17 Feb 2024 05:42:34 -0800 Subject: [PATCH] fix: an equation lemma with `autoParam` arguments fails to rewrite (#3316) closes #2243 --- .../Elab/PreDefinition/Structural/Eqns.lean | 2 +- src/Lean/Elab/PreDefinition/WF/Eqns.lean | 2 +- src/Lean/Meta/Basic.lean | 23 ++++++++---- src/Lean/Meta/Eqns.lean | 2 +- tests/lean/run/2243.lean | 35 +++++++++++++++++++ tests/lean/run/2939.lean | 3 ++ 6 files changed, 57 insertions(+), 10 deletions(-) create mode 100644 tests/lean/run/2243.lean create mode 100644 tests/lean/run/2939.lean diff --git a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean b/src/Lean/Elab/PreDefinition/Structural/Eqns.lean index ecb458c943cf..566217d5d707 100644 --- a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean +++ b/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 diff --git a/src/Lean/Elab/PreDefinition/WF/Eqns.lean b/src/Lean/Elab/PreDefinition/WF/Eqns.lean index 096cb5cc1061..cfecc7654309 100644 --- a/src/Lean/Elab/PreDefinition/WF/Eqns.lean +++ b/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 diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index 69ba7ec1fc5e..140e12dfa566 100644 --- a/src/Lean/Meta/Basic.lean +++ b/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 diff --git a/src/Lean/Meta/Eqns.lean b/src/Lean/Meta/Eqns.lean index ae9fb789f24f..1f24631df82c 100644 --- a/src/Lean/Meta/Eqns.lean +++ b/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) diff --git a/tests/lean/run/2243.lean b/tests/lean/run/2243.lean new file mode 100644 index 000000000000..893e482a8f96 --- /dev/null +++ b/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] diff --git a/tests/lean/run/2939.lean b/tests/lean/run/2939.lean new file mode 100644 index 000000000000..00a99495c3e0 --- /dev/null +++ b/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]