diff --git a/src/Lean/Meta/Sym/Simp.lean b/src/Lean/Meta/Sym/Simp.lean index a4aa483b38..632ebbfae8 100644 --- a/src/Lean/Meta/Sym/Simp.lean +++ b/src/Lean/Meta/Sym/Simp.lean @@ -22,3 +22,4 @@ public import Lean.Meta.Sym.Simp.EvalGround public import Lean.Meta.Sym.Simp.Discharger public import Lean.Meta.Sym.Simp.ControlFlow public import Lean.Meta.Sym.Simp.Goal +public import Lean.Meta.Sym.Simp.Telescope diff --git a/src/Lean/Meta/Sym/Simp/Forall.lean b/src/Lean/Meta/Sym/Simp/Forall.lean index 381d4f169b..33accd7e08 100644 --- a/src/Lean/Meta/Sym/Simp/Forall.lean +++ b/src/Lean/Meta/Sym/Simp/Forall.lean @@ -94,17 +94,17 @@ Returns the simplified result paired with the remaining `ArrowInfo` list. When a collapses (e.g., to `True`), the returned `infos` list is empty, signaling to `toForall` that no reconstruction is needed. -/ -partial def simpArrows (e : Expr) (infos : List ArrowInfo) : SimpM (Result × List ArrowInfo) := do +partial def simpArrows (e : Expr) (infos : List ArrowInfo) (simpBody : Simproc) : SimpM (Result × List ArrowInfo) := do match infos with - | [] => return ((← simp e), []) + | [] => return ((← simpBody e), []) | info :: infos' => - let_expr f@Arrow p q := e | return ((← simp e), infos) + let_expr f@Arrow p q := e | return ((← simpBody e), infos) let p_r ← simp p if (← isFalseExpr (p_r.getResultExpr p)) && info.v.isZero then match p_r with | .rfl _ => return (.step (← getTrueExpr) (mkApp (mkConst ``false_arrow) q), []) | .step _ h _ => return (.step (← getTrueExpr) (mkApp3 (mkConst ``false_arrow_congr) p q h), []) - let (q_r, infos') ← simpArrows q infos' + let (q_r, infos') ← simpArrows q infos' simpBody if (← isTrueExpr (q_r.getResultExpr q)) then match q_r with | .rfl _ => return (.step (← getTrueExpr) (mkApp (mkConst ``arrow_true [info.u]) p), []) @@ -157,10 +157,10 @@ a chance to apply `post` methods to the intermediate arrow `p → p`. Thus, this is a simproc that is meant to be used as a pre-method and marks the result as fully simplified to prevent `simpArrow` from being applied. -/ -public def simpArrowTelescope : Simproc := fun e => do +public def simpArrowTelescope (simpBody : Simproc := simp) : Simproc := fun e => do unless e.isArrow do return .rfl -- not applicable let { arrow, infos, v } ← toArrow e - let (.step arrow' h _, infos) ← simpArrows arrow infos | return .rfl (done := true) + let (.step arrow' h _, infos) ← simpArrows arrow infos simpBody | return .rfl (done := true) let e' ← toForall arrow' infos let α := mkSort v let v1 := v.succ @@ -190,7 +190,7 @@ public def simpArrow (e : Expr) : SimpM Result := do let e' ← e.updateForallS! p' q' return .step e' <| mkApp6 (mkConst ``implies_congr [u, v]) p p' q q' h₁ h₂ -public def simpForall (e : Expr) : SimpM Result := do +public def simpForall' (simpArrow : Simproc) (simpBody : Simproc) (e : Expr) : SimpM Result := do if e.isArrow then simpArrow e else if (← isProp e) then @@ -201,7 +201,7 @@ public def simpForall (e : Expr) : SimpM Result := do return .rfl where main (xs : Array Expr) (b : Expr) : SimpM Result := do - match (← simp b) with + match (← simpBody b) with | .rfl _ => return .rfl | .step b' h _ => let h ← mkLambdaFVars xs h @@ -216,4 +216,7 @@ where | .forallE _ _ b _ => if b.hasLooseBVar 0 then getForallTelescopeSize b (n+1) else n | _ => n +public def simpForall : Simproc := + simpForall' simpArrow simp + end Lean.Meta.Sym.Simp diff --git a/src/Lean/Meta/Sym/Simp/Have.lean b/src/Lean/Meta/Sym/Simp/Have.lean index f9f8c64042..484014f520 100644 --- a/src/Lean/Meta/Sym/Simp/Have.lean +++ b/src/Lean/Meta/Sym/Simp/Have.lean @@ -6,7 +6,7 @@ Authors: Leonardo de Moura module prelude public import Lean.Meta.Sym.Simp.SimpM -import Lean.Meta.Sym.Simp.Lambda +public import Lean.Meta.Sym.Simp.Lambda import Lean.Meta.Sym.AlphaShareBuilder import Lean.Meta.Sym.InstantiateS import Lean.Meta.Sym.ReplaceS @@ -316,7 +316,8 @@ For each application `f a`: - If only `a` changed: use `congrArg : a = a' → f a = f a'` - If neither changed: return `.rfl` -/ -def simpBetaApp (e : Expr) (fType : Expr) (fnUnivs argUnivs : Array Level) : SimpM Result := do +def simpBetaApp (e : Expr) (fType : Expr) (fnUnivs argUnivs : Array Level) + (simpBody : Simproc) : SimpM Result := do return (← go e 0).1 where go (e : Expr) (i : Nat) : SimpM (Result × Expr) := do @@ -339,7 +340,7 @@ where let h := mkApp6 (← mkCongrPrefix ``congr fType i) f f' a a' hf ha pure <| .step e' h return (r, fType.bindingBody!) - | .lam .. => return (← simpLambda e, fType) + | .lam .. => return (← simpBody e, fType) | _ => unreachable! mkCongrPrefix (declName : Name) (fType : Expr) (i : Nat) : SymM Expr := do @@ -375,12 +376,12 @@ e₃ = e₄ (by rfl, definitional equality from toHave) e₁ = e₄ (by transitivity) ``` -/ -def simpHaveCore (e : Expr) : SimpM SimpHaveResult := do +def simpHaveCore (e : Expr) (simpBody : Simproc) : SimpM SimpHaveResult := do let e₁ := e let r ← toBetaApp e₁ let e₂ := r.e let { fnUnivs, argUnivs } ← getUnivs r.fType - match (← simpBetaApp e₂ r.fType fnUnivs argUnivs) with + match (← simpBetaApp e₂ r.fType fnUnivs argUnivs simpBody) with | .rfl _ => return { result := .rfl, α := r.α, u := r.u } | .step e₃ h _ => let h₁ := mkApp6 (mkConst ``Eq.trans [r.u]) r.α e₁ e₂ e₃ r.h h @@ -397,8 +398,8 @@ Simplify a `have`-telescope. This is the main entry point for `have`-telescope simplification in `Sym.simp`. See module documentation for the algorithm overview. -/ -public def simpHave (e : Expr) : SimpM Result := do - return (← simpHaveCore e).result +public def simpHave (e : Expr) (simpBody : Simproc) : SimpM Result := do + return (← simpHaveCore e simpBody).result /-- Simplify a `have`-telescope and eliminate unused bindings. @@ -406,8 +407,8 @@ Simplify a `have`-telescope and eliminate unused bindings. This combines simplification with dead variable elimination in a single pass, avoiding quadratic behavior from multiple passes. -/ -public def simpHaveAndZetaUnused (e₁ : Expr) : SimpM Result := do - let r ← simpHaveCore e₁ +public def simpHaveAndZetaUnused (e₁ : Expr) (simpBody : Simproc) : SimpM Result := do + let r ← simpHaveCore e₁ simpBody match r.result with | .rfl _ => let e₂ ← zetaUnused e₁ @@ -425,7 +426,7 @@ public def simpHaveAndZetaUnused (e₁ : Expr) : SimpM Result := do (mkApp2 (mkConst ``Eq.refl [r.u]) r.α e₃) return .step e₃ h -public def simpLet (e : Expr) : SimpM Result := do +public def simpLet' (simpBody : Simproc) (e : Expr) : SimpM Result := do if !e.letNondep! then /- **Note**: We don't do anything if it is a dependent `let`. @@ -433,6 +434,9 @@ public def simpLet (e : Expr) : SimpM Result := do -/ return .rfl else - simpHaveAndZetaUnused e + simpHaveAndZetaUnused e simpBody + +public def simpLet : Simproc := + simpLet' simpLambda end Lean.Meta.Sym.Simp diff --git a/src/Lean/Meta/Sym/Simp/Lambda.lean b/src/Lean/Meta/Sym/Simp/Lambda.lean index 78050f2997..3ea0363bf4 100644 --- a/src/Lean/Meta/Sym/Simp/Lambda.lean +++ b/src/Lean/Meta/Sym/Simp/Lambda.lean @@ -46,12 +46,12 @@ def mkFunextFor (xs : Array Expr) (β : Expr) : MetaM Expr := do let result ← mkLambdaFVars #[f, g, h] result return result -public def simpLambda (e : Expr) : SimpM Result := do +public def simpLambda' (simpBody : Simproc) (e : Expr) : SimpM Result := do lambdaTelescope e fun xs b => withoutModifyingCacheIfNotWellBehaved do main xs (← shareCommon b) where main (xs : Array Expr) (b : Expr) : SimpM Result := do - match (← simp b) with + match (← simpBody b) with | .rfl _ => return .rfl | .step b' h _ => let h ← mkLambdaFVars xs h @@ -69,4 +69,7 @@ where modify fun s => { s with funext := s.funext.insert { expr := key } h } return h +public def simpLambda : Simproc := + simpLambda' simp + end Lean.Meta.Sym.Simp diff --git a/src/Lean/Meta/Sym/Simp/Telescope.lean b/src/Lean/Meta/Sym/Simp/Telescope.lean new file mode 100644 index 0000000000..629b14bc0d --- /dev/null +++ b/src/Lean/Meta/Sym/Simp/Telescope.lean @@ -0,0 +1,25 @@ +/- +Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ +module +prelude +public import Lean.Meta.Sym.Simp.SimpM +import Lean.Meta.Sym.Simp.Have +import Lean.Meta.Sym.Simp.Forall +namespace Lean.Meta.Sym.Simp +/-- +Simplify telescope binders (`have`-expression values, and arrow hypotheses) +but not the final body. This simproc is useful to simplify target before +introducing. +-/ +public partial def simpTelescope : Simproc := fun e => do + match e with + | .letE .. => + simpLet' (simpLambda' simpTelescope) e + | .forallE .. => + simpForall' (simpArrow := simpArrowTelescope simpTelescope) (simpBody := simpLambda' simpTelescope) e + | _ => return .rfl + +end Lean.Meta.Sym.Simp diff --git a/tests/lean/run/sym_simp_5.lean b/tests/lean/run/sym_simp_5.lean new file mode 100644 index 0000000000..f835667cff --- /dev/null +++ b/tests/lean/run/sym_simp_5.lean @@ -0,0 +1,33 @@ +import Lean +open Lean Meta Elab Tactic + +elab "sym_simp" "[" declNames:ident,* "]" : tactic => do + let rewrite ← Sym.mkSimprocFor (← declNames.getElems.mapM fun s => realizeGlobalConstNoOverload s.raw) Sym.Simp.dischargeSimpSelf + let methods : Sym.Simp.Methods := { + pre := Sym.Simp.simpTelescope + post := Sym.Simp.evalGround.andThen rewrite + } + liftMetaTactic1 fun mvarId => Sym.SymM.run do + let mvarId ← Sym.preprocessMVar mvarId + (← Sym.simpGoal mvarId methods).toOption + +set_option warn.sorry false + +/-! +Recall that `simpTelescope` does not simplify the body of a telescope. +This is why `0 + x = 0 + id x` is not simplified in the following example. +-/ +/-- +trace: p q : Prop +⊢ q → + ∀ (x : Nat), + p → + have x := x; + have y := x; + x = y → 0 + x = 0 + id x +-/ +#guard_msgs in +example (p q : Prop) : q → ∀ x : Nat, p ∧ True → have x := 0 + x; have y := x; True → x = 0 + 0 + id y → 0 + x = 0 + id x := by + sym_simp [and_true, Nat.zero_add, id_eq] + trace_state + admit