From 3c6ea49d0e4ff3a924452809ca5aeb41b0611bef Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 3 Apr 2026 19:31:16 -0700 Subject: [PATCH] feat: add `mkAppNS`, `mkAppRevS`, `betaRevS`, `betaS`, and related `Sym` functions (#13273) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR adds a comprehensive public API for constructing maximally shared expression applications and performing beta reduction in the `Sym` framework. These functions were previously defined locally in the VC generator and cbv tactic, and are needed by downstream `SymM`-based tools. New functions in `Lean.Meta.Sym.Internal` (generic over `MonadShareCommon`): - `mkAppS₆` through `mkAppS₁₁` (higher-arity application builders) - `mkAppRangeS`, `mkAppNS` (forward application over arrays/ranges) - `mkAppRevRangeS`, `mkAppRevS` (reversed application over arrays/ranges) New public functions in `Lean.Meta.Sym` (`SymM`): - `betaRevS` and `betaS` (beta reduction with max sharing) - `mkForallFVarsS` (forall abstraction with max sharing) The `AlphaShareBuilderM`-specific `mkAppRevRangeS` in `InstantiateS.lean` is replaced by the generic version from `Internal`, and the internal `betaRevS` is renamed to `betaRevS'`. The `Cbv.mkAppNS` now delegates to `Internal.mkAppNS`. --------- Co-authored-by: Claude Opus 4.6 (1M context) --- src/Lean/Meta/Sym/AbstractS.lean | 12 +++++++ src/Lean/Meta/Sym/AlphaShareBuilder.lean | 44 ++++++++++++++++++++++++ src/Lean/Meta/Sym/InstantiateS.lean | 34 +++++++++--------- src/Lean/Meta/Tactic/Cbv/Main.lean | 1 + src/Lean/Meta/Tactic/Cbv/Util.lean | 3 -- 5 files changed, 74 insertions(+), 20 deletions(-) diff --git a/src/Lean/Meta/Sym/AbstractS.lean b/src/Lean/Meta/Sym/AbstractS.lean index c4da5c763f..1c944484f4 100644 --- a/src/Lean/Meta/Sym/AbstractS.lean +++ b/src/Lean/Meta/Sym/AbstractS.lean @@ -97,4 +97,16 @@ public def mkLambdaFVarsS (xs : Array Expr) (e : Expr) : SymM Expr := do let type ← abstractFVarsRange decl.type i xs mkLambdaS decl.userName decl.binderInfo type b +/-- +Similar to `mkForallFVars`, but uses the more efficient `abstractFVars` and `abstractFVarsRange`, +and makes the same assumption made by these functions. +-/ +public def mkForallFVarsS (xs : Array Expr) (e : Expr) : SymM Expr := do + let b ← abstractFVars e xs + xs.size.foldRevM (init := b) fun i _ b => do + let x := xs[i] + let decl ← x.fvarId!.getDecl + let type ← abstractFVarsRange decl.type i xs + mkForallS decl.userName decl.binderInfo type b + end Lean.Meta.Sym diff --git a/src/Lean/Meta/Sym/AlphaShareBuilder.lean b/src/Lean/Meta/Sym/AlphaShareBuilder.lean index 32acdb8c1e..750d3881c0 100644 --- a/src/Lean/Meta/Sym/AlphaShareBuilder.lean +++ b/src/Lean/Meta/Sym/AlphaShareBuilder.lean @@ -189,4 +189,48 @@ def mkAppS₄ (f a₁ a₂ a₃ a₄ : Expr) : m Expr := do def mkAppS₅ (f a₁ a₂ a₃ a₄ a₅ : Expr) : m Expr := do mkAppS (← mkAppS₄ f a₁ a₂ a₃ a₄) a₅ +def mkAppS₆ (f a₁ a₂ a₃ a₄ a₅ a₆ : Expr) : m Expr := do + mkAppS (← mkAppS₅ f a₁ a₂ a₃ a₄ a₅) a₆ + +def mkAppS₇ (f a₁ a₂ a₃ a₄ a₅ a₆ a₇ : Expr) : m Expr := do + mkAppS (← mkAppS₆ f a₁ a₂ a₃ a₄ a₅ a₆) a₇ + +def mkAppS₈ (f a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ : Expr) : m Expr := do + mkAppS (← mkAppS₇ f a₁ a₂ a₃ a₄ a₅ a₆ a₇) a₈ + +def mkAppS₉ (f a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉ : Expr) : m Expr := do + mkAppS (← mkAppS₈ f a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈) a₉ + +def mkAppS₁₀ (f a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉ a₁₀ : Expr) : m Expr := do + mkAppS (← mkAppS₉ f a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉) a₁₀ + +def mkAppS₁₁ (f a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉ a₁₀ a₁₁ : Expr) : m Expr := do + mkAppS (← mkAppS₁₀ f a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉ a₁₀) a₁₁ + +/-- `mkAppRangeS f i j #[a₀, ..., aᵢ, ..., aⱼ, ...]` ==> `f aᵢ ... aⱼ₋₁` with max sharing. -/ +partial def mkAppRangeS (f : Expr) (beginIdx endIdx : Nat) (args : Array Expr) : m Expr := + go endIdx f beginIdx +where + go (endIdx : Nat) (b : Expr) (i : Nat) : m Expr := do + if endIdx ≤ i then return b + else go endIdx (← mkAppS b args[i]!) (i + 1) + +/-- `mkAppNS f #[a₀, ..., aₙ]` constructs `f a₀ ... aₙ` with max sharing. -/ +def mkAppNS (f : Expr) (args : Array Expr) : m Expr := + mkAppRangeS f 0 args.size args + +/-- `mkAppRevRangeS f b e revArgs` ==> `mkAppRev f (revArgs.extract b e)` with max sharing. -/ +partial def mkAppRevRangeS (f : Expr) (beginIdx endIdx : Nat) (revArgs : Array Expr) : m Expr := + go revArgs beginIdx f endIdx +where + go (revArgs : Array Expr) (start : Nat) (b : Expr) (i : Nat) : m Expr := do + if i ≤ start then return b + else + let i := i - 1 + go revArgs start (← mkAppS b revArgs[i]!) i + +/-- Same as `mkAppS f args` but reversing `args`, with max sharing. -/ +def mkAppRevS (f : Expr) (revArgs : Array Expr) : m Expr := + mkAppRevRangeS f 0 revArgs.size revArgs + end Lean.Meta.Sym.Internal diff --git a/src/Lean/Meta/Sym/InstantiateS.lean b/src/Lean/Meta/Sym/InstantiateS.lean index ec29a90ae3..81c0cfa846 100644 --- a/src/Lean/Meta/Sym/InstantiateS.lean +++ b/src/Lean/Meta/Sym/InstantiateS.lean @@ -86,22 +86,8 @@ It assumes the input is maximally shared, and ensures the output is too. public def instantiateS (e : Expr) (subst : Array Expr) : SymM Expr := liftBuilderM <| instantiateS' e subst -/-- `mkAppRevRangeS f b e args == mkAppRev f (revArgs.extract b e)` -/ -def mkAppRevRangeS (f : Expr) (beginIdx endIdx : Nat) (revArgs : Array Expr) : AlphaShareBuilderM Expr := - loop revArgs beginIdx f endIdx -where - loop (revArgs : Array Expr) (start : Nat) (b : Expr) (i : Nat) : AlphaShareBuilderM Expr := do - if i ≤ start then - return b - else - let i := i - 1 - loop revArgs start (← mkAppS b revArgs[i]!) i - -/-- -Beta-reduces `f` applied to reversed arguments `revArgs`, ensuring maximally shared terms. -`betaRevS f #[a₃, a₂, a₁]` computes the beta-normal form of `f a₁ a₂ a₃`. --/ -partial def betaRevS (f : Expr) (revArgs : Array Expr) : AlphaShareBuilderM Expr := +/-- Internal variant of `betaRevS` that runs in `AlphaShareBuilderM`. -/ +private partial def betaRevS' (f : Expr) (revArgs : Array Expr) : AlphaShareBuilderM Expr := if revArgs.size == 0 then return f else @@ -173,7 +159,7 @@ where | .bvar bidx => let f' ← visitBVar f bidx offset if modified || !isSameExpr f f' then - betaRevS f' argsRev + betaRevS' f' argsRev else return e | _ => unreachable! @@ -215,4 +201,18 @@ public def instantiateRevBetaS (e : Expr) (subst : Array Expr) : SymM Expr := do if !e.hasLooseBVars || subst.isEmpty then return e else liftBuilderM <| instantiateRevBetaS' e subst +/-- +Beta-reduces `f` applied to reversed arguments `revArgs`, ensuring maximally shared terms. +`betaRevS f #[a₃, a₂, a₁]` computes the beta-normal form of `f a₁ a₂ a₃`. +-/ +public def betaRevS (f : Expr) (revArgs : Array Expr) : SymM Expr := + liftBuilderM <| betaRevS' f revArgs + +/-- +Apply the given arguments to `f`, beta-reducing if `f` is a lambda expression, +ensuring maximally shared terms. See `betaRevS` for details. +-/ +public def betaS (f : Expr) (args : Array Expr) : SymM Expr := + betaRevS f args.reverse + end Lean.Meta.Sym diff --git a/src/Lean/Meta/Tactic/Cbv/Main.lean b/src/Lean/Meta/Tactic/Cbv/Main.lean index 6239d929e6..9b12426155 100644 --- a/src/Lean/Meta/Tactic/Cbv/Main.lean +++ b/src/Lean/Meta/Tactic/Cbv/Main.lean @@ -283,6 +283,7 @@ def handleProj : Simproc := fun e => do let newProof ← mkEqOfHEq newProof (check := false) return .step (← Lean.Expr.updateProjS! e e') newProof +open Sym.Internal in /-- For an application whose head is neither a constant nor a lambda (e.g. a projection like `p.1 x`), simplify the function head and lift the proof via `congrArg`. diff --git a/src/Lean/Meta/Tactic/Cbv/Util.lean b/src/Lean/Meta/Tactic/Cbv/Util.lean index 6a6282d12a..2aa2179ce1 100644 --- a/src/Lean/Meta/Tactic/Cbv/Util.lean +++ b/src/Lean/Meta/Tactic/Cbv/Util.lean @@ -24,9 +24,6 @@ namespace Lean.Meta.Tactic.Cbv open Lean.Meta.Sym.Simp -public def mkAppNS (f : Expr) (args : Array Expr) : Sym.SymM Expr := do - args.foldlM Sym.Internal.mkAppS f - abbrev isNatValue (e : Expr) : Bool := (Sym.getNatValue? e).isSome abbrev isStringValue (e : Expr) : Bool := (Sym.getStringValue? e).isSome abbrev isIntValue (e : Expr) : Bool := (Sym.getIntValue? e).isSome