From 7a1ec17e1ab7691688272cf559a9c6cc77b0e398 Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Thu, 5 Nov 2026 22:56:38 +0000 Subject: [PATCH 1/4] feat: `vcgen` destructures binders by `@[vcgen_rintro]` rules MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The attribute `@[vcgen_rintro]` registers a theorem whose conclusion is a `∀` telescope ending in an application of a parameter `G`. `vcgen` keys the rules in a discrimination tree by their conclusion. At each binder of a `∀` target, it applies the first matching rule as a backward rule, and otherwise introduces the binder. With rules for `x ∈ a :: l` and `x ∈ []`, the target `∀ n, n ∈ [1, 2, 3] → G n` splits into the goals `G 1`, `G 2` and `G 3`. `vcgen` always uses the rules `Prod.forall_intro`, `PUnit.forall_intro` and `True.forall_intro`. `Prod.forall_intro` replaces the special case for binders over pairs. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01QPKmiUooPkkAEYh2giBqfH --- src/Lean/Elab/Tactic/VCGen.lean | 2 + src/Lean/Elab/Tactic/VCGen/Context.lean | 5 + src/Lean/Elab/Tactic/VCGen/Frontend.lean | 2 +- src/Lean/Elab/Tactic/VCGen/RIntroAttr.lean | 99 +++++ src/Lean/Elab/Tactic/VCGen/RuleCache.lean | 12 + src/Lean/Elab/Tactic/VCGen/Solve.lean | 54 ++- src/Lean/Elab/Tactic/VCGen/Util.lean | 13 +- src/Std/WP/Automation.lean | 12 + tests/elab/vcgenJPs.lean | 12 +- tests/elab/vcgenRIntro.lean | 418 +++++++++++++++++++++ 10 files changed, 594 insertions(+), 35 deletions(-) create mode 100644 src/Lean/Elab/Tactic/VCGen/RIntroAttr.lean create mode 100644 tests/elab/vcgenRIntro.lean diff --git a/src/Lean/Elab/Tactic/VCGen.lean b/src/Lean/Elab/Tactic/VCGen.lean index fa097014e547..c755cb0c3fff 100644 --- a/src/Lean/Elab/Tactic/VCGen.lean +++ b/src/Lean/Elab/Tactic/VCGen.lean @@ -16,6 +16,7 @@ public import Lean.Elab.Tactic.VCGen.Entails public import Lean.Elab.Tactic.VCGen.Solve public import Lean.Elab.Tactic.VCGen.Driver public import Lean.Elab.Tactic.VCGen.SimpAttr +public import Lean.Elab.Tactic.VCGen.RIntroAttr public import Lean.Elab.Tactic.VCGen.Frontend /-! @@ -31,5 +32,6 @@ The `vcgen` tactic, split across the modules above. - `VCGen.Solve` — the main `solve` step / `SolveResult`. - `VCGen.Driver` — the worklist driver (`work`, `emitVC`, `main`, `Result`). - `VCGen.SimpAttr` — the `@[vcgen_simp]` theorem set. +- `VCGen.RIntroAttr` — the `@[vcgen_rintro]` binder destructuring rules. - `VCGen.Frontend` — the `vcgen` syntax + tactic elaborator + `mkSpecContext`. -/ diff --git a/src/Lean/Elab/Tactic/VCGen/Context.lean b/src/Lean/Elab/Tactic/VCGen/Context.lean index 59244bca18ba..59d55f0a8d34 100644 --- a/src/Lean/Elab/Tactic/VCGen/Context.lean +++ b/src/Lean/Elab/Tactic/VCGen/Context.lean @@ -11,6 +11,7 @@ public import Lean.Elab.Tactic.VCGen.SpecDB public import Lean.Elab.Tactic.VCGen.FrameProc public import Lean.Meta.Sym.Apply public import Lean.Meta.Sym.Simp.DiscrTree +public import Lean.Elab.Tactic.VCGen.RIntroAttr public import Lean.Meta.Sym.Simp.SimpM public import Lean.Meta.Tactic.Grind.Types @@ -106,6 +107,8 @@ public structure Context where /-- The `@[frameproc]` registry snapshot taken at frontend init. `solve` selects a procedure per program node by the node's monad. -/ frameProcs : FrameProcs := {} + /-- The `@[vcgen_rintro]` rules, keyed by their conclusion. -/ + rintros : DiscrTree RIntroEntry := .empty /-- The `Sym.simp` methods that rewrite hypotheses, state arguments and verification conditions with the `@[vcgen_simp]` theorems and those of the `simp [...]` clause. `none` when the `simp` config option is `false`. -/ @@ -201,6 +204,8 @@ public structure State where /-- Caches the frame rule (`meet_op_wp_upperAdjoint_le_wp`), keyed by the `WPMonad` instance and the number of excess state arguments. -/ frameBackwardRuleCache : Std.HashMap (ExprPtr × Nat) FrameBackwardRule := {} + /-- Caches the backward rules of the `@[vcgen_rintro]` rules, keyed by declaration name. -/ + rintroBackwardRuleCache : Std.HashMap Name BackwardRule := {} /-- The frame database from the `frames` clause. -/ frameDB : FrameDB := {} /-- diff --git a/src/Lean/Elab/Tactic/VCGen/Frontend.lean b/src/Lean/Elab/Tactic/VCGen/Frontend.lean index 4b47ceadbcda..4e35919e6a9d 100644 --- a/src/Lean/Elab/Tactic/VCGen/Frontend.lean +++ b/src/Lean/Elab/Tactic/VCGen/Frontend.lean @@ -152,7 +152,7 @@ public def mkContext (lemmas : Syntax) (goal : MVarId) (ignoreStarArg := false) catch _ => continue let backwardRules ← mkBackwardRules let allSpecThms ← addSimpSpecs specThms simpThms - let ctx : Context := { backwardRules } + let ctx : Context := { backwardRules, rintros := ← getRIntros } return (ctx, { specs := allSpecThms }) /-- True iff `m` carries a `WPMonad m _ _` instance, i.e. it is a genuine weakest-precondition monad diff --git a/src/Lean/Elab/Tactic/VCGen/RIntroAttr.lean b/src/Lean/Elab/Tactic/VCGen/RIntroAttr.lean new file mode 100644 index 000000000000..14f2499fe338 --- /dev/null +++ b/src/Lean/Elab/Tactic/VCGen/RIntroAttr.lean @@ -0,0 +1,99 @@ +/- +Copyright (c) 2026 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sebastian Graf +-/ +module + +prelude +public import Lean.ScopedEnvExtension +public import Lean.Attributes +public import Lean.Meta.Sym.Apply +public import Lean.Meta.Sym.Simp.DiscrTree + +/-! +The `@[vcgen_rintro]` attribute registers the rules by which `vcgen` destructures a binder while it +introduces the binders of the target, like an `rintro` pattern fixed per binder type. + +A rule is a theorem whose conclusion is a `∀` telescope ending in an application of a parameter +`G`. Its premises are the binders up to the last one that mentions `G`, and its conclusion is the +rest. Take +``` +theorem List.forall_mem_cons_intro {G : α → Prop} (ha : G a) (hl : ∀ x, x ∈ l → G x) : + ∀ x, x ∈ a :: l → G x +``` +with the conclusion `∀ x, x ∈ a :: l → G x`. It turns the target `∀ x ∈ [a, b], G x` into the +goals `G a` and `∀ x ∈ [b], G x`. The rules are keyed in a discrimination tree by their +conclusion, whose `∀` binders become `.arrow` keys over the binder type and the body. At each +binder of the target, `vcgen` applies the first matching rule in priority order as a backward rule +to the remaining target, and otherwise introduces the binder. + +`vcgen` always uses the rules `Prod.forall_intro`, `PUnit.forall_intro` and `True.forall_intro`. +-/ + +open Lean Meta Sym + +public section + +namespace Lean.Elab.Tactic.VCGen + +/-- One `@[vcgen_rintro]` rule: the theorem `declName`, whose first `numPremises` binders are the +premises, with the discrimination tree keys `keys` of its conclusion. -/ +structure RIntroEntry where + declName : Name + numPremises : Nat + keys : Array DiscrTree.Key + prio : Nat + deriving Inhabited + +instance : BEq RIntroEntry where + beq e₁ e₂ := e₁.declName == e₂.declName + +/-- The rules `vcgen` uses without registration. -/ +def builtinRIntros : Array Name := #[`Prod.forall_intro, `PUnit.forall_intro, `True.forall_intro] + +builtin_initialize rintroExt : SimpleScopedEnvExtension RIntroEntry (DiscrTree RIntroEntry) ← + registerSimpleScopedEnvExtension { + initial := .empty + addEntry := fun d e => d.insertKeyValue e.keys e + } + +/-- Check that the conclusion of `declName` is a `∀` telescope ending in an application of a +parameter, and compute its `RIntroEntry`. -/ +def mkRIntroEntry (declName : Name) (prio : Nat) : MetaM RIntroEntry := do + let info ← getConstInfo declName + let (numBinders, numPremises) ← forallTelescope info.type fun xs body => do + let some g := body.getAppFn.fvarId? + | throwError "`@[vcgen_rintro]`: the conclusion of `{declName}` does not end in an \ + application of a parameter" + let mut numPremises := 0 + for h : i in [:xs.size] do + if xs[i].fvarId! == g || (← inferType xs[i]).containsFVar g then + numPremises := i + 1 + return (xs.size, numPremises) + if numPremises == numBinders then + throwError "`@[vcgen_rintro]`: the conclusion of `{declName}` is not a `∀`" + let rule ← mkBackwardRuleFromDecl declName (some numPremises) + return { declName, numPremises, keys := rule.pattern.mkDiscrTreeKeys, prio } + +/-- The rules registered with `@[vcgen_rintro]`, and the rules of `builtinRIntros` that exist in +the environment. -/ +def getRIntros : MetaM (DiscrTree RIntroEntry) := do + let mut d := rintroExt.getState (← getEnv) + for declName in builtinRIntros do + if (← getEnv).contains declName then + let e ← mkRIntroEntry declName (eval_prio default) + d := d.insertKeyValue e.keys e + return d + +builtin_initialize registerBuiltinAttribute { + ref := by exact decl_name% + name := `vcgen_rintro + descr := "register a rule by which `vcgen` destructures a binder while introducing binders" + add := fun declName stx kind => do + let prio ← getAttrParamOptPrio stx[1] + let e ← (mkRIntroEntry declName prio).run' + rintroExt.add e kind +} + +end Lean.Elab.Tactic.VCGen diff --git a/src/Lean/Elab/Tactic/VCGen/RuleCache.lean b/src/Lean/Elab/Tactic/VCGen/RuleCache.lean index df3bd5989e7c..368a2504ec7f 100644 --- a/src/Lean/Elab/Tactic/VCGen/RuleCache.lean +++ b/src/Lean/Elab/Tactic/VCGen/RuleCache.lean @@ -96,5 +96,17 @@ public def mkFrameBackwardRuleCached (fp : FrameProc) (info : WPApp) : modify fun st => { st with frameBackwardRuleCache := st.frameBackwardRuleCache.insert key frule } return frule +/-- +Cached construction of the backward rule of the `@[vcgen_rintro]` rule `e`. The rule abstracts +the `e.numPremises` premises and matches the conclusion of `e`. + +Cache key: the declaration name of `e`. +-/ +public def mkBackwardRuleForRIntroCached (e : RIntroEntry) : VCGenM BackwardRule := do + if let some rule := (← get).rintroBackwardRuleCache[e.declName]? then return rule + let rule ← (← liftMetaM <| mkBackwardRuleFromDecl e.declName (some e.numPremises)).shareCommon + modify fun st => { st with rintroBackwardRuleCache := st.rintroBackwardRuleCache.insert e.declName rule } + return rule + end Lean.Elab.Tactic.VCGen diff --git a/src/Lean/Elab/Tactic/VCGen/Solve.lean b/src/Lean/Elab/Tactic/VCGen/Solve.lean index f9f876f0000e..c389422e2c9e 100644 --- a/src/Lean/Elab/Tactic/VCGen/Solve.lean +++ b/src/Lean/Elab/Tactic/VCGen/Solve.lean @@ -15,7 +15,6 @@ public import Lean.Meta.Sym.InstantiateS public import Lean.Meta.Sym.Simp.App import Lean.Meta.Sym.InferType import Lean.Meta.Sym.InstantiateMVarsS -import Init.Data.Prod open Lean Meta Elab Tactic Sym Sym.Internal open Lean.Elab.Tactic.VCGen.SpecAttr @@ -64,22 +63,39 @@ def consumeMData? (goal : MVarId) (target : Expr) : VCGenM (Option MVarId) := do unless target.isMData do return none return some (← goal.replaceTargetDefEqFast target.consumeMData) -/-- Split `∀ p : Nat × Nat, P p` into `∀ a b, P (a, b)`. -/ -def splitProdBinder (goal : MVarId) (target : Expr) : VCGenM MVarId := - goal.withContext do - let .forallE _ dom body _ := target | return goal - let dom ← instantiateMVarsIfMVarAppS dom - let_expr c@Prod α β := dom | return goal - let us := c.constLevels! - let mk ← mkAppNS (← mkConstS ``Prod.mk us) #[α, β, .bvar 1, .bvar 0] - let newTarget := Expr.forallE `a α (.forallE `b β (body.instantiate1 mk) .default) .default - let g ← liftMetaM <| mkFreshExprSyntheticOpaqueMVar (← shareCommon newTarget) - let motive := Expr.lam `p dom body .default - let prodForall ← mkAppNS (← mkConstS ``Prod.forall us) #[α, β, motive] - goal.assign <| mkApp4 (.const ``Iff.mpr []) target newTarget prodForall g - return g.mvarId! - -/-- Strategy 1: simp the target, then introduce binders if the target is a `∀`. -/ +/-- Apply the backward rule `rule` of a `@[vcgen_rintro]` rule to `goal`. The types of the new goals +are instantiated, so that the rule parameter `G` is beta-reduced at its arguments. -/ +def applyRIntroRule (goal : MVarId) (rule : BackwardRule) : VCGenM (Option (List MVarId)) := do + let .goals gs ← rule.apply goal | return none + some <$> gs.mapM fun g => do + let ty ← g.getType + let ty' ← instantiateMVarsS ty + if isSameExpr ty ty' then return g + g.replaceTargetDefEqFast ty' + +/-- Strategy 1a: apply the first `@[vcgen_rintro]` rule, in priority order, whose conclusion matches +the target `∀ y, …`. -/ +def forallRIntro? (goal : MVarId) (target : Expr) : VCGenM (Option (List MVarId)) := do + let entries := Sym.getMatch (← getMCtx) (← read).rintros target + if entries.isEmpty then return none + for entry in entries.insertionSort (·.prio > ·.prio) do + if let some gs ← applyRIntroRule goal (← mkBackwardRuleForRIntroCached entry) then + trace[Elab.Tactic.Do.vcgen] "Applied rintro rule {entry.declName}" + return some gs + return none + +/-- The number of binders `forallIntro?` introduces at once from `type`: one `∀` binder and the +`let` binders that follow it. -/ +def numBindersToIntroOne : Expr → Nat + | .forallE _ _ b _ => go b 1 + | _ => 0 +where + go : Expr → Nat → Nat + | .letE _ _ _ b _, n => go b (n + 1) + | _, n => n + +/-- Strategy 1: simp the target, then introduce its binders. At each `∀` binder, a matching +`@[vcgen_rintro]` rule destructures the binder instead. -/ def forallIntro? (oldGoal : MVarId) (target : Expr) : VCGenM (Option (List MVarId)) := do unless target.isForall do return none let oldGoal ← instantiateBinderDomains oldGoal @@ -89,8 +105,8 @@ def forallIntro? (oldGoal : MVarId) (target : Expr) : VCGenM (Option (List MVarI | .noProgress => pure oldGoal let mut target ← goal.getType while target.isForall do - let n := numBindersToIntro target - let goal' ← if n == 0 then splitProdBinder goal target else introsHygienicN goal n + if let some gs ← forallRIntro? goal target then return some gs + let goal' ← introsHygienicN goal (numBindersToIntroOne target) if goal' == goal then break goal := goal' target ← goal.getType diff --git a/src/Lean/Elab/Tactic/VCGen/Util.lean b/src/Lean/Elab/Tactic/VCGen/Util.lean index 38b397fe927e..6fe6bc31b00a 100644 --- a/src/Lean/Elab/Tactic/VCGen/Util.lean +++ b/src/Lean/Elab/Tactic/VCGen/Util.lean @@ -116,10 +116,9 @@ public def processHypotheses (goal : Grind.Goal) : VCGenM Grind.Goal := do public def isProgramName (n : Name) : Bool := !n.hasMacroScopes && !n.isImplementationDetail -/-- The leading binders of `type`, stopping at a binder over a product: `∀ (n : Nat) (p : α × β)` -counts one, because `solve` splits `p` into one binder per component first. -/ +/-- The number of leading `∀` and `let` binders of `type`. -/ public def numBindersToIntro : Expr → Nat - | .forallE _ d b _ => if d.isAppOf ``Prod then 0 else numBindersToIntro b + 1 + | .forallE _ _ b _ => numBindersToIntro b + 1 | .letE _ _ _ b _ => numBindersToIntro b + 1 | _ => 0 @@ -172,9 +171,10 @@ public def simpGoalTelescope (goal : MVarId) : VCGenM Sym.SimpGoalResult := do Introduce the excess state arguments of an entailment goal `pre ⊑ rhs` whose lattice type is a function type `σ₁ → … → σₙ → α`: repeatedly apply `stateArgIntro` (a backward rule for `Lean.Order.le_of_forall_le`) and introduce the new state binder, until the lattice type is -no longer a function type. Returns `none` when the carrier is not a function type (nothing to -introduce); throws when the carrier is a function type that `le_of_forall_le` cannot peel, such as a -dependent function lattice `(a : α) → β a → …`. +no longer a function type. A state binder that a `@[vcgen_rintro]` rule matches stays in the +target for `solve` to destructure. Returns `none` when the carrier is not a function type (nothing +to introduce); throws when the carrier is a function type that `le_of_forall_le` cannot peel, such +as a dependent function lattice `(a : α) → β a → …`. -/ public partial def introsExcessArgs (goal : MVarId) : VCGenM (Option MVarId) := goal.withContext do @@ -183,6 +183,7 @@ public partial def introsExcessArgs (goal : MVarId) : unless α.isForall do return none let .goals [goal] ← (← read).backwardRules.stateArgIntro.applyChecked goal | throwError "failed to apply {.ofConstName ``Lean.Order.le_of_forall_le} to goal{indentExpr type}" + unless (Sym.getMatch (← getMCtx) (← read).rintros (← goal.getType)).isEmpty do return some goal let goal ← introsHygienic goal return (← introsExcessArgs goal) <|> some goal diff --git a/src/Std/WP/Automation.lean b/src/Std/WP/Automation.lean index 01da612d1710..a524cc295598 100644 --- a/src/Std/WP/Automation.lean +++ b/src/Std/WP/Automation.lean @@ -32,4 +32,16 @@ attribute [simp, grind norm] Variant.evalsTo_ofMeasure Variant.evalsBelow_ofMeas end Std.WP +/-! ## The built-in `vcgen_rintro` rules -/ + +theorem Prod.forall_intro {α : Type _} {β : Type _} {G : α × β → Prop} (h : ∀ a b, G (a, b)) : + ∀ p, G p := + fun (a, b) => h a b + +theorem PUnit.forall_intro {G : PUnit → Prop} (h : G ⟨⟩) : ∀ u, G u := + fun ⟨⟩ => h + +theorem True.forall_intro {G : True → Prop} (h : G trivial) : ∀ h, G h := + fun ⟨⟩ => h + end diff --git a/tests/elab/vcgenJPs.lean b/tests/elab/vcgenJPs.lean index 5ddad37263df..38b6e392604d 100644 --- a/tests/elab/vcgenJPs.lean +++ b/tests/elab/vcgenJPs.lean @@ -271,18 +271,14 @@ theorem wide_triple : ⦃ fun _ => True ⦄ wide x ⦃ fun r => ⌜r > 1⌝ ⦄ /-- trace: case vc1 b : Nat → Bool -s₀ s✝¹ : Nat -x✝ : PUnit -s✝ : Nat +s₀ s✝¹ s✝ : Nat h✝¹ : b 0 = true ∧ s✝ = s₀ + 1 ∨ ¬b 0 = true ∧ s✝ = s₀ + 2 h✝ : b 1 = true ⊢ s₀ + 2 ≤ s✝ + 1 case vc2 b : Nat → Bool -s₀ s✝¹ : Nat -x✝ : PUnit -s✝ : Nat +s₀ s✝¹ s✝ : Nat h✝¹ : b 0 = true ∧ s✝ = s₀ + 1 ∨ ¬b 0 = true ∧ s✝ = s₀ + 2 h✝ : ¬b 1 = true ⊢ s₀ + 2 ≤ s✝ + 2 @@ -340,9 +336,7 @@ def root_match (x : Nat) (b : Bool) : StateM Nat Nat := do trace: case vc1 k : Nat b : Bool -s✝ : Nat -x✝¹ : PUnit -x✝ s : Nat +s✝ x✝ s : Nat h✝ : b = true ∧ x✝ = 2 ∧ s = s✝ ∨ ¬b = true ∧ x✝ = 3 ∧ s = s✝ ⊢ 0 < x✝ + s -/ diff --git a/tests/elab/vcgenRIntro.lean b/tests/elab/vcgenRIntro.lean new file mode 100644 index 000000000000..bf775f1216e3 --- /dev/null +++ b/tests/elab/vcgenRIntro.lean @@ -0,0 +1,418 @@ +import Std.WP +import Std.Data.HashSet + +/-! +`vcgen` destructures a binder with the rules registered by `@[vcgen_rintro]`. The rules +`forall_mem_cons_intro` and `forall_mem_nil_intro` split a binder +`∀ x, x ∈ l → G x` over a literal list `l` into one goal `G a` per element `a` of `l`. +-/ + +open Std.WP Lean.Order +set_option experimental.vcgen true + +abbrev M := StateM Nat + +theorem forall_mem_cons_intro {α : Type _} {G : α → Prop} {a : α} {l : List α} + (ha : G a) (hl : ∀ x, x ∈ l → G x) : ∀ x, x ∈ a :: l → G x := + List.forall_mem_cons.mpr ⟨ha, hl⟩ + +theorem forall_mem_nil_intro {α : Type _} {G : α → Prop} : ∀ x, x ∈ ([] : List α) → G x := + fun _ h => nomatch h + +/-! Without a registered rule, `vcgen` introduces the membership hypothesis. -/ + +/-- +trace: case vc1 +G : Nat → Prop +n✝ : Nat +a✝ : n✝ ∈ [1, 2, 3] +s✝ : Nat +⊢ G n✝ +--- +warning: declaration uses `sorry` +-/ +#guard_msgs in +example (G : Nat → Prop) : + ∀ n, n ∈ [1, 2, 3] → ⦃ fun _ => True ⦄ (pure n : M Nat) ⦃ fun r _ => G r ⦄ := by + vcgen + trace_state + all_goals sorry + +attribute [vcgen_rintro] forall_mem_cons_intro forall_mem_nil_intro + +/-! The rules split the binder `∀ n, n ∈ [1, 2, 3] → …` into one goal per element. -/ + +/-- +trace: case vc1 +G : Nat → Prop +s✝ : Nat +⊢ G 1 + +case vc2 +G : Nat → Prop +s✝ : Nat +⊢ G 2 + +case vc3 +G : Nat → Prop +s✝ : Nat +⊢ G 3 +--- +warning: declaration uses `sorry` +-/ +#guard_msgs in +example (G : Nat → Prop) : + ∀ n, n ∈ [1, 2, 3] → ⦃ fun _ => True ⦄ (pure n : M Nat) ⦃ fun r _ => G r ⦄ := by + vcgen + trace_state + all_goals sorry + +/-! The binders before the destructured variable are introduced. -/ + +/-- +trace: case vc1 +G : Nat → Prop +k✝ s✝ : Nat +⊢ G k✝ + +case vc2 +G : Nat → Prop +k✝ s✝ : Nat +⊢ G (k✝ + 1) +--- +warning: declaration uses `sorry` +-/ +#guard_msgs in +example (G : Nat → Prop) : + ∀ k n, n ∈ [k, k + 1] → ⦃ fun _ => True ⦄ (pure n : M Nat) ⦃ fun r _ => G r ⦄ := by + vcgen + trace_state + all_goals sorry + +/-! The binder over the empty list leaves no goal. -/ + +example (G : Nat → Prop) : + ∀ n, n ∈ ([] : List Nat) → ⦃ fun _ => True ⦄ (pure n : M Nat) ⦃ fun r _ => G r ⦄ := by + vcgen + +/-! A binder `x` whose premise mentions `x` falls back to plain introduction, since `G x` cannot +abstract the premise. -/ + +/-- +trace: case vc1 +G : (x : Nat) → x ∈ [1, 2] → Prop +x✝ : Nat +h✝ : x✝ ∈ [1, 2] +s✝ : Nat +⊢ G x✝ h✝ +--- +warning: declaration uses `sorry` +-/ +#guard_msgs in +example (G : (x : Nat) → x ∈ [1, 2] → Prop) : + ∀ x (h : x ∈ [1, 2]), ⦃ fun _ => True ⦄ (pure x : M Nat) ⦃ fun _ _ => G x h ⦄ := by + vcgen + trace_state + all_goals sorry + +/-! Membership in a `Std.HashSet` matches no rule and falls back to plain introduction. -/ + +/-- +trace: case vc1 +G : Nat → Prop +s : Std.HashSet Nat +x✝ : Nat +a✝ : x✝ ∈ s +s✝ : Nat +⊢ G x✝ +--- +warning: declaration uses `sorry` +-/ +#guard_msgs in +example (G : Nat → Prop) (s : Std.HashSet Nat) : + ∀ x, x ∈ s → ⦃ fun _ => True ⦄ (pure x : M Nat) ⦃ fun r _ => G r ⦄ := by + vcgen + trace_state + all_goals sorry + +/-! A list variable `l` falls back to plain introduction, after the rules split off the literal +elements in front of `l`. -/ + +/-- +trace: case vc1 +G : Nat → Prop +l : List Nat +x✝ : Nat +a✝ : x✝ ∈ l +s✝ : Nat +⊢ G x✝ +--- +warning: declaration uses `sorry` +-/ +#guard_msgs in +example (G : Nat → Prop) (l : List Nat) : + ∀ x, x ∈ l → ⦃ fun _ => True ⦄ (pure x : M Nat) ⦃ fun r _ => G r ⦄ := by + vcgen + trace_state + all_goals sorry + +/-- +trace: case vc1 +G : Nat → Prop +a : Nat +l : List Nat +s✝ : Nat +⊢ G a + +case vc2 +G : Nat → Prop +a : Nat +l : List Nat +x✝ : Nat +a✝ : x✝ ∈ l +s✝ : Nat +⊢ G x✝ +--- +warning: declaration uses `sorry` +-/ +#guard_msgs in +example (G : Nat → Prop) (a : Nat) (l : List Nat) : + ∀ x, x ∈ a :: l → ⦃ fun _ => True ⦄ (pure x : M Nat) ⦃ fun r _ => G r ⦄ := by + vcgen + trace_state + all_goals sorry + +/-! Nested binders split into one goal per pair of elements. -/ + +/-- +trace: case vc1 +G : Nat → Nat → Prop +s✝ : Nat +⊢ G 1 3 + +case vc2 +G : Nat → Nat → Prop +s✝ : Nat +⊢ G 1 4 + +case vc3 +G : Nat → Nat → Prop +s✝ : Nat +⊢ G 2 3 + +case vc4 +G : Nat → Nat → Prop +s✝ : Nat +⊢ G 2 4 +--- +warning: declaration uses `sorry` +-/ +#guard_msgs in +example (G : Nat → Nat → Prop) : + ∀ x, x ∈ [1, 2] → ∀ y, y ∈ [3, 4] → + ⦃ fun _ => True ⦄ (pure x : M Nat) ⦃ fun r _ => G r y ⦄ := by + vcgen + trace_state + all_goals sorry + +/-! The binders and premises before the destructured variable are introduced. -/ + +/-- +trace: case vc1 +G : Nat → Nat → Prop +s✝¹ s✝ : Nat +⊢ G s✝¹ 1 + +case vc2 +G : Nat → Nat → Prop +s✝¹ s✝ : Nat +⊢ G s✝¹ 2 +--- +warning: declaration uses `sorry` +-/ +#guard_msgs in +example (G : Nat → Nat → Prop) : + ∀ s, ∀ x, x ∈ [1, 2] → ⦃ fun _ => True ⦄ (pure x : M Nat) ⦃ fun r _ => G s r ⦄ := by + vcgen + trace_state + all_goals sorry + +/-- +trace: case vc1 +P : Nat → Prop +G : Nat → Nat → Prop +s✝¹ : Nat +a✝ : P s✝¹ +s✝ : Nat +⊢ G s✝¹ 1 + +case vc2 +P : Nat → Prop +G : Nat → Nat → Prop +s✝¹ : Nat +a✝ : P s✝¹ +s✝ : Nat +⊢ G s✝¹ 2 +--- +warning: declaration uses `sorry` +-/ +#guard_msgs in +example (P : Nat → Prop) (G : Nat → Nat → Prop) : + ∀ s, P s → ∀ x, x ∈ [1, 2] → ⦃ fun _ => True ⦄ (pure x : M Nat) ⦃ fun r _ => G s r ⦄ := by + vcgen + trace_state + all_goals sorry + +/-! Rules for the two binders `x y` of a membership in a list of pairs. -/ + +theorem forall_pair_mem_cons_intro {α β : Type _} {G : α → β → Prop} {a : α} {b : β} + {l : List (α × β)} (hab : G a b) (hl : ∀ x y, (x, y) ∈ l → G x y) : + ∀ x y, (x, y) ∈ (a, b) :: l → G x y := by + intro x y h + cases h with + | head => exact hab + | tail _ h => exact hl x y h + +theorem forall_pair_mem_nil_intro {α β : Type _} {G : α → β → Prop} : + ∀ x y, (x, y) ∈ ([] : List (α × β)) → G x y := + fun _ _ h => nomatch h + +attribute [vcgen_rintro] forall_pair_mem_cons_intro forall_pair_mem_nil_intro + +/-! The rule `forall_pair_mem_cons_intro` destructures the binders `x y` of a membership in a list of +pairs, next to the rules for one binder. -/ + +/-- +trace: case vc1 +G : Nat → Nat → Prop +s✝ : Nat +⊢ G 1 2 + +case vc2 +G : Nat → Nat → Prop +s✝ : Nat +⊢ G 3 4 +--- +warning: declaration uses `sorry` +-/ +#guard_msgs in +example (G : Nat → Nat → Prop) : + ∀ x y, (x, y) ∈ [(1, 2), (3, 4)] → + ⦃ fun _ => True ⦄ (pure x : M Nat) ⦃ fun r _ => G r y ⦄ := by + vcgen + trace_state + all_goals sorry + +/-! The binders `y x` in the order opposite to `(x, y)` fall back to plain introduction. -/ + +/-- +trace: case vc1 +G : Nat → Nat → Prop +y✝ x✝ : Nat +a✝ : (x✝, y✝) ∈ [(1, 2)] +s✝ : Nat +⊢ G x✝ y✝ +--- +warning: declaration uses `sorry` +-/ +#guard_msgs in +example (G : Nat → Nat → Prop) : + ∀ y x, (x, y) ∈ [(1, 2)] → ⦃ fun _ => True ⦄ (pure x : M Nat) ⦃ fun r _ => G r y ⦄ := by + vcgen + trace_state + all_goals sorry + +/-! Rules keyed by `LT.lt` split the bound `n < 3` into one goal per smaller number. -/ + +theorem forall_lt_succ_intro {G : Nat → Prop} {k : Nat} (hk : G k) (hl : ∀ n, n < k → G n) : + ∀ n, n < k + 1 → G n := fun n h => by + rcases Nat.lt_succ_iff_lt_or_eq.mp h with h | rfl + · exact hl n h + · exact hk + +theorem forall_lt_zero_intro {G : Nat → Prop} : ∀ n, n < 0 → G n := + fun _ h => absurd h (Nat.not_lt_zero _) + +attribute [vcgen_rintro] forall_lt_succ_intro forall_lt_zero_intro + +/-- +trace: case vc1 +G : Nat → Prop +s✝ : Nat +⊢ G 2 + +case vc2 +G : Nat → Prop +s✝ : Nat +⊢ G 1 + +case vc3 +G : Nat → Prop +s✝ : Nat +⊢ G 0 +--- +warning: declaration uses `sorry` +-/ +#guard_msgs in +example (G : Nat → Prop) : + ∀ n, n < 3 → ⦃ fun _ => True ⦄ (pure n : M Nat) ⦃ fun r _ => G r ⦄ := by + vcgen + trace_state + all_goals sorry + +/-! The built-in rules destructure a binder over a pair, `Unit` or `True`. -/ + +/-- +trace: case vc1 +G : Nat → Nat → Prop +a✝ b✝ s✝ : Nat +⊢ G a✝ b✝ +--- +warning: declaration uses `sorry` +-/ +#guard_msgs in +example (G : Nat → Nat → Prop) : + ∀ p : Nat × Nat, ⦃ fun _ => True ⦄ (pure p : M (Nat × Nat)) ⦃ fun r _ => G r.1 r.2 ⦄ := by + vcgen + trace_state + all_goals sorry + +/-- +trace: case vc1 +G : PUnit → Prop +s✝ : Nat +⊢ G PUnit.unit +--- +warning: declaration uses `sorry` +-/ +#guard_msgs in +example (G : Unit → Prop) : + ∀ u : Unit, ⦃ fun _ => True ⦄ (pure u : M Unit) ⦃ fun r _ => G r ⦄ := by + vcgen + trace_state + all_goals sorry + +/-- +trace: case vc1 +G : True → Prop +s✝ : Nat +⊢ G trivial +--- +warning: declaration uses `sorry` +-/ +#guard_msgs in +example (G : True → Prop) : + ∀ h : True, ⦃ fun _ => True ⦄ (pure () : M Unit) ⦃ fun _ _ => G h ⦄ := by + vcgen + trace_state + all_goals sorry + +/-! A rule needs a conclusion that is a `∀`. -/ + +theorem not_forall {G : Nat → Prop} (h : G 0) : G 0 := h + +/-- +error: `@[vcgen_rintro]`: the conclusion of `not_forall` is not a `∀` +-/ +#guard_msgs in +attribute [vcgen_rintro] not_forall From 77ff45017884f2e30e46de642e0ce1a111714906 Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Fri, 6 Nov 2026 06:55:24 +0000 Subject: [PATCH 2/4] perf: keep only `Prod.forall_intro` built in, and introduce binder prefixes at once MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `vcgen` uses `Prod.forall_intro` as its only built-in `@[vcgen_rintro]` rule. `PUnit.forall_intro` and `True.forall_intro` stay available for registration. `forallIntro?` introduces the binders before the first `∀` that a rule matches in one step, and `getRIntros` computes the entries of the built-in rules once. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01QPKmiUooPkkAEYh2giBqfH --- src/Lean/Elab/Tactic/VCGen/RIntroAttr.lean | 15 ++++++++++++--- src/Lean/Elab/Tactic/VCGen/Solve.lean | 19 +++++++++++++++++-- tests/elab/vcgenJPs.lean | 12 +++++++++--- tests/elab/vcgenRIntro.lean | 5 ++++- 4 files changed, 42 insertions(+), 9 deletions(-) diff --git a/src/Lean/Elab/Tactic/VCGen/RIntroAttr.lean b/src/Lean/Elab/Tactic/VCGen/RIntroAttr.lean index 14f2499fe338..7980c004562c 100644 --- a/src/Lean/Elab/Tactic/VCGen/RIntroAttr.lean +++ b/src/Lean/Elab/Tactic/VCGen/RIntroAttr.lean @@ -28,7 +28,8 @@ conclusion, whose `∀` binders become `.arrow` keys over the binder type and th binder of the target, `vcgen` applies the first matching rule in priority order as a backward rule to the remaining target, and otherwise introduces the binder. -`vcgen` always uses the rules `Prod.forall_intro`, `PUnit.forall_intro` and `True.forall_intro`. +`vcgen` always uses the rule `Prod.forall_intro`. `Std.WP.Automation` also provides the rules +`PUnit.forall_intro` and `True.forall_intro`. -/ open Lean Meta Sym @@ -50,7 +51,7 @@ instance : BEq RIntroEntry where beq e₁ e₂ := e₁.declName == e₂.declName /-- The rules `vcgen` uses without registration. -/ -def builtinRIntros : Array Name := #[`Prod.forall_intro, `PUnit.forall_intro, `True.forall_intro] +def builtinRIntros : Array Name := #[`Prod.forall_intro] builtin_initialize rintroExt : SimpleScopedEnvExtension RIntroEntry (DiscrTree RIntroEntry) ← registerSimpleScopedEnvExtension { @@ -76,13 +77,21 @@ def mkRIntroEntry (declName : Name) (prio : Nat) : MetaM RIntroEntry := do let rule ← mkBackwardRuleFromDecl declName (some numPremises) return { declName, numPremises, keys := rule.pattern.mkDiscrTreeKeys, prio } +/-- The entries of the rules of `builtinRIntros`, computed once. -/ +builtin_initialize builtinRIntroEntries : IO.Ref (Std.HashMap Name RIntroEntry) ← IO.mkRef {} + /-- The rules registered with `@[vcgen_rintro]`, and the rules of `builtinRIntros` that exist in the environment. -/ def getRIntros : MetaM (DiscrTree RIntroEntry) := do let mut d := rintroExt.getState (← getEnv) for declName in builtinRIntros do if (← getEnv).contains declName then - let e ← mkRIntroEntry declName (eval_prio default) + let e ← match (← builtinRIntroEntries.get)[declName]? with + | some e => pure e + | none => + let e ← mkRIntroEntry declName (eval_prio default) + builtinRIntroEntries.modify (·.insert declName e) + pure e d := d.insertKeyValue e.keys e return d diff --git a/src/Lean/Elab/Tactic/VCGen/Solve.lean b/src/Lean/Elab/Tactic/VCGen/Solve.lean index c389422e2c9e..b8f237edaafe 100644 --- a/src/Lean/Elab/Tactic/VCGen/Solve.lean +++ b/src/Lean/Elab/Tactic/VCGen/Solve.lean @@ -82,6 +82,7 @@ def forallRIntro? (goal : MVarId) (target : Expr) : VCGenM (Option (List MVarId) if let some gs ← applyRIntroRule goal (← mkBackwardRuleForRIntroCached entry) then trace[Elab.Tactic.Do.vcgen] "Applied rintro rule {entry.declName}" return some gs + trace[Elab.Tactic.Do.vcgen] "Rintro rule {entry.declName} does not apply" return none /-- The number of binders `forallIntro?` introduces at once from `type`: one `∀` binder and the @@ -94,6 +95,17 @@ where | .letE _ _ _ b _, n => go b (n + 1) | _, n => n +/-- The number of leading `∀` and `let` binders of `type` before the first `∀` that a +`@[vcgen_rintro]` rule matches. -/ +def numBindersBeforeRIntro (type : Expr) : VCGenM Nat := do + let mctx ← getMCtx + let rintros := (← read).rintros + let rec go : Expr → Nat → Nat + | e@(.forallE _ _ b _), n => if (Sym.getMatch mctx rintros e).isEmpty then go b (n + 1) else n + | .letE _ _ _ b _, n => go b (n + 1) + | _, n => n + return go type 0 + /-- Strategy 1: simp the target, then introduce its binders. At each `∀` binder, a matching `@[vcgen_rintro]` rule destructures the binder instead. -/ def forallIntro? (oldGoal : MVarId) (target : Expr) : VCGenM (Option (List MVarId)) := do @@ -105,8 +117,11 @@ def forallIntro? (oldGoal : MVarId) (target : Expr) : VCGenM (Option (List MVarI | .noProgress => pure oldGoal let mut target ← goal.getType while target.isForall do - if let some gs ← forallRIntro? goal target then return some gs - let goal' ← introsHygienicN goal (numBindersToIntroOne target) + let mut n ← numBindersBeforeRIntro target + if n == 0 then + if let some gs ← forallRIntro? goal target then return some gs + n := numBindersToIntroOne target + let goal' ← introsHygienicN goal n if goal' == goal then break goal := goal' target ← goal.getType diff --git a/tests/elab/vcgenJPs.lean b/tests/elab/vcgenJPs.lean index 38b6e392604d..5ddad37263df 100644 --- a/tests/elab/vcgenJPs.lean +++ b/tests/elab/vcgenJPs.lean @@ -271,14 +271,18 @@ theorem wide_triple : ⦃ fun _ => True ⦄ wide x ⦃ fun r => ⌜r > 1⌝ ⦄ /-- trace: case vc1 b : Nat → Bool -s₀ s✝¹ s✝ : Nat +s₀ s✝¹ : Nat +x✝ : PUnit +s✝ : Nat h✝¹ : b 0 = true ∧ s✝ = s₀ + 1 ∨ ¬b 0 = true ∧ s✝ = s₀ + 2 h✝ : b 1 = true ⊢ s₀ + 2 ≤ s✝ + 1 case vc2 b : Nat → Bool -s₀ s✝¹ s✝ : Nat +s₀ s✝¹ : Nat +x✝ : PUnit +s✝ : Nat h✝¹ : b 0 = true ∧ s✝ = s₀ + 1 ∨ ¬b 0 = true ∧ s✝ = s₀ + 2 h✝ : ¬b 1 = true ⊢ s₀ + 2 ≤ s✝ + 2 @@ -336,7 +340,9 @@ def root_match (x : Nat) (b : Bool) : StateM Nat Nat := do trace: case vc1 k : Nat b : Bool -s✝ x✝ s : Nat +s✝ : Nat +x✝¹ : PUnit +x✝ s : Nat h✝ : b = true ∧ x✝ = 2 ∧ s = s✝ ∨ ¬b = true ∧ x✝ = 3 ∧ s = s✝ ⊢ 0 < x✝ + s -/ diff --git a/tests/elab/vcgenRIntro.lean b/tests/elab/vcgenRIntro.lean index bf775f1216e3..ac751a2972f1 100644 --- a/tests/elab/vcgenRIntro.lean +++ b/tests/elab/vcgenRIntro.lean @@ -360,7 +360,8 @@ example (G : Nat → Prop) : trace_state all_goals sorry -/-! The built-in rules destructure a binder over a pair, `Unit` or `True`. -/ +/-! The built-in rule `Prod.forall_intro` destructures a binder over a pair. The rules +`PUnit.forall_intro` and `True.forall_intro` destructure a binder over `Unit` or `True`. -/ /-- trace: case vc1 @@ -377,6 +378,8 @@ example (G : Nat → Nat → Prop) : trace_state all_goals sorry +attribute [vcgen_rintro] PUnit.forall_intro True.forall_intro + /-- trace: case vc1 G : PUnit → Prop From 5292c9802050378576a88ec327efddca9834a6f0 Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Fri, 6 Nov 2026 10:56:00 +0000 Subject: [PATCH 3/4] perf: `vcgen` matches each binder against `@[vcgen_rintro]` rules once MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `forallIntro?` walks the binders of the target in one pass. It matches each `∀` binder against the rule tree once, introduces the binders between two matches at once, and continues after a matched rule that does not apply without rescanning the telescope. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01D74FF61KPDjY3k6hEEbrmc --- src/Lean/Elab/Tactic/VCGen/Solve.lean | 63 +++++++++++---------------- 1 file changed, 25 insertions(+), 38 deletions(-) diff --git a/src/Lean/Elab/Tactic/VCGen/Solve.lean b/src/Lean/Elab/Tactic/VCGen/Solve.lean index b8f237edaafe..a217f59f9192 100644 --- a/src/Lean/Elab/Tactic/VCGen/Solve.lean +++ b/src/Lean/Elab/Tactic/VCGen/Solve.lean @@ -73,11 +73,10 @@ def applyRIntroRule (goal : MVarId) (rule : BackwardRule) : VCGenM (Option (List if isSameExpr ty ty' then return g g.replaceTargetDefEqFast ty' -/-- Strategy 1a: apply the first `@[vcgen_rintro]` rule, in priority order, whose conclusion matches -the target `∀ y, …`. -/ -def forallRIntro? (goal : MVarId) (target : Expr) : VCGenM (Option (List MVarId)) := do - let entries := Sym.getMatch (← getMCtx) (← read).rintros target - if entries.isEmpty then return none +/-- Strategy 1a: apply the first of the `@[vcgen_rintro]` rules `entries`, in priority order, that +applies to the target of `goal`. -/ +def applyRIntroRules (goal : MVarId) (entries : Array RIntroEntry) : + VCGenM (Option (List MVarId)) := do for entry in entries.insertionSort (·.prio > ·.prio) do if let some gs ← applyRIntroRule goal (← mkBackwardRuleForRIntroCached entry) then trace[Elab.Tactic.Do.vcgen] "Applied rintro rule {entry.declName}" @@ -85,29 +84,9 @@ def forallRIntro? (goal : MVarId) (target : Expr) : VCGenM (Option (List MVarId) trace[Elab.Tactic.Do.vcgen] "Rintro rule {entry.declName} does not apply" return none -/-- The number of binders `forallIntro?` introduces at once from `type`: one `∀` binder and the -`let` binders that follow it. -/ -def numBindersToIntroOne : Expr → Nat - | .forallE _ _ b _ => go b 1 - | _ => 0 -where - go : Expr → Nat → Nat - | .letE _ _ _ b _, n => go b (n + 1) - | _, n => n - -/-- The number of leading `∀` and `let` binders of `type` before the first `∀` that a -`@[vcgen_rintro]` rule matches. -/ -def numBindersBeforeRIntro (type : Expr) : VCGenM Nat := do - let mctx ← getMCtx - let rintros := (← read).rintros - let rec go : Expr → Nat → Nat - | e@(.forallE _ _ b _), n => if (Sym.getMatch mctx rintros e).isEmpty then go b (n + 1) else n - | .letE _ _ _ b _, n => go b (n + 1) - | _, n => n - return go type 0 - -/-- Strategy 1: simp the target, then introduce its binders. At each `∀` binder, a matching -`@[vcgen_rintro]` rule destructures the binder instead. -/ +/-- Strategy 1: simp the target, then introduce its binders. One pass over the binders matches each +`∀` binder against the `@[vcgen_rintro]` rules once. A matching rule destructures the binder, and +the binders between two matches are introduced at once. -/ def forallIntro? (oldGoal : MVarId) (target : Expr) : VCGenM (Option (List MVarId)) := do unless target.isForall do return none let oldGoal ← instantiateBinderDomains oldGoal @@ -115,16 +94,24 @@ def forallIntro? (oldGoal : MVarId) (target : Expr) : VCGenM (Option (List MVarI | .closed => return some [] | .goal goal => pure goal | .noProgress => pure oldGoal - let mut target ← goal.getType - while target.isForall do - let mut n ← numBindersBeforeRIntro target - if n == 0 then - if let some gs ← forallRIntro? goal target then return some gs - n := numBindersToIntroOne target - let goal' ← introsHygienicN goal n - if goal' == goal then break - goal := goal' - target ← goal.getType + let rintros := (← read).rintros + let mut e ← goal.getType + let mut n := 0 + repeat + match e with + | .forallE _ _ b _ => + let entries := Sym.getMatch (← getMCtx) rintros e + unless entries.isEmpty do + goal ← introsHygienicN goal n + n := 0 + if let some gs ← applyRIntroRules goal entries then return some gs + n := n + 1 + e := b + | .letE _ _ _ b _ => + n := n + 1 + e := b + | _ => break + goal ← introsHygienicN goal n if goal == oldGoal then throwError "Failed to intro forall target {goal}" return some [goal] From 29be2ab34402f596fc4781ccd40c79e78dfed0f1 Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Fri, 6 Nov 2026 11:31:35 +0000 Subject: [PATCH 4/4] test: register the `PUnit` and `True` rintro rules in the test only `PUnit.forall_intro` and `True.forall_intro` move from `Std.WP.Automation` into `tests/elab/vcgenRIntro.lean`. `vcgen` uses only `Prod.forall_intro` as a built-in rule, and `True.forall_intro` showed up in the completions of `True.` in `travellingCompletions`. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01D74FF61KPDjY3k6hEEbrmc --- src/Lean/Elab/Tactic/VCGen/RIntroAttr.lean | 3 +-- src/Std/WP/Automation.lean | 8 +------- tests/elab/vcgenRIntro.lean | 8 ++++++-- 3 files changed, 8 insertions(+), 11 deletions(-) diff --git a/src/Lean/Elab/Tactic/VCGen/RIntroAttr.lean b/src/Lean/Elab/Tactic/VCGen/RIntroAttr.lean index 7980c004562c..4a4c9c346223 100644 --- a/src/Lean/Elab/Tactic/VCGen/RIntroAttr.lean +++ b/src/Lean/Elab/Tactic/VCGen/RIntroAttr.lean @@ -28,8 +28,7 @@ conclusion, whose `∀` binders become `.arrow` keys over the binder type and th binder of the target, `vcgen` applies the first matching rule in priority order as a backward rule to the remaining target, and otherwise introduces the binder. -`vcgen` always uses the rule `Prod.forall_intro`. `Std.WP.Automation` also provides the rules -`PUnit.forall_intro` and `True.forall_intro`. +`vcgen` always uses the rule `Prod.forall_intro`. -/ open Lean Meta Sym diff --git a/src/Std/WP/Automation.lean b/src/Std/WP/Automation.lean index a524cc295598..e2d79f2464ba 100644 --- a/src/Std/WP/Automation.lean +++ b/src/Std/WP/Automation.lean @@ -32,16 +32,10 @@ attribute [simp, grind norm] Variant.evalsTo_ofMeasure Variant.evalsBelow_ofMeas end Std.WP -/-! ## The built-in `vcgen_rintro` rules -/ +/-! ## The built-in `vcgen_rintro` rule -/ theorem Prod.forall_intro {α : Type _} {β : Type _} {G : α × β → Prop} (h : ∀ a b, G (a, b)) : ∀ p, G p := fun (a, b) => h a b -theorem PUnit.forall_intro {G : PUnit → Prop} (h : G ⟨⟩) : ∀ u, G u := - fun ⟨⟩ => h - -theorem True.forall_intro {G : True → Prop} (h : G trivial) : ∀ h, G h := - fun ⟨⟩ => h - end diff --git a/tests/elab/vcgenRIntro.lean b/tests/elab/vcgenRIntro.lean index ac751a2972f1..651810a724e4 100644 --- a/tests/elab/vcgenRIntro.lean +++ b/tests/elab/vcgenRIntro.lean @@ -360,7 +360,7 @@ example (G : Nat → Prop) : trace_state all_goals sorry -/-! The built-in rule `Prod.forall_intro` destructures a binder over a pair. The rules +/-! The built-in rule `Prod.forall_intro` destructures a binder over a pair. The registered rules `PUnit.forall_intro` and `True.forall_intro` destructure a binder over `Unit` or `True`. -/ /-- @@ -378,7 +378,11 @@ example (G : Nat → Nat → Prop) : trace_state all_goals sorry -attribute [vcgen_rintro] PUnit.forall_intro True.forall_intro +@[vcgen_rintro] theorem PUnit.forall_intro {G : PUnit → Prop} (h : G ⟨⟩) : ∀ u, G u := + fun ⟨⟩ => h + +@[vcgen_rintro] theorem True.forall_intro {G : True → Prop} (h : G trivial) : ∀ h, G h := + fun ⟨⟩ => h /-- trace: case vc1