refactor: drop wp canonicalization, register the WP interpretations as instances

The default-transparency instance guard alone fixes spec application for goals with a registered `WP` instance: the rule conclusion pins the goal's own instance arguments, premises keep the spec's `WPMonad.toWP` spelling, and `synthPending` assigns the spec's `WPMonad` metavariable during the guard, so goals and rules stay consistent without canonicalizing either. `Sym.canon` on the constructed rule also rewrote tuple matchers into projections, which destroyed the binder names that `binderNameHint` consumption reads and broke `tests/elab/intrinsicVerification.lean` (also on CI).

The `WP` interpretations in `Std.WP.Monad.Instances` are proper instances now, with `toWP _ := inferInstance`, so the existing tests exercise the registered-instance path and the dedicated regression test is gone. The `Id`-monad theorems in `tests/elab/vcgenFrames.lean` state their assertions at `Prop`: a hypothesis `[WPMonad Id Pred EPred]` over a generic `Pred` denotes no real instance, and instance search, which ignores `outParam` positions during selection, resolves `WP (Id β) …` to the registered `Prop` instance regardless.

Author: sgraf812

src/Lean/Elab/Tactic/VCGen/Driver.lean

@@ -10,7 +10,6 @@ public import Lean.Elab.Tactic.Meta
 public import Lean.Elab.Tactic.VCGen.Context
 public import Lean.Elab.Tactic.VCGen.Solve
 public import Lean.Meta.Sym.Grind
-import Lean.Meta.Sym.Canon
 
 open Lean Meta Elab Tactic Sym Sym.Internal Lean.Order
 open Lean.Elab.Tactic.Do.SpecAttr
@@ -94,16 +93,8 @@ private structure WorkItem where
   goal : Grind.Goal
   scope : Scope
 
-/--
-Canonicalizes the goal target with `Sym.canon`, so its instance arguments (e.g. the `WP`
-instance of a `wp` application) match the canonicalized rules from `tryMkBackwardRuleFromSpec`.
--/
-private def canonTarget (mvarId : MVarId) : SymM MVarId := do
-  mvarId.replaceTargetDefEqFast (← shareCommon (← Sym.canon (← mvarId.getType)))
-
 public def work (scope : Scope) (goal : Grind.Goal) : VCGenM Unit := do
   let mvarId ← preprocessMVar goal.mvarId
-  let mvarId ← canonTarget mvarId
   let mut worklist : Array WorkItem := #[{ goal := { goal with mvarId }, scope }]
   while let some s := worklist.back? do
     worklist := worklist.pop

src/Lean/Elab/Tactic/VCGen/RuleConstruction.lean

@@ -12,7 +12,6 @@ public import Lean.Elab.Tactic.VCGen.Reduce
 public import Lean.Elab.Tactic.VCGen.SpecDB
 public import Lean.Meta.Sym.Apply
 public import Lean.Meta.Sym.Util
-import Lean.Meta.Sym.Canon
 meta import Std.WP.Frame
 
 open Lean Meta Elab Tactic Sym
@@ -284,7 +283,7 @@ exposes in the premise program (e.g. for class projection unfold equations like
 `MonadState.modifyGet.eq_1`) are reduced by `wpHeadReduce?` before the next spec lookup.
 -/
 private def eqSpecToWp? (info : WPApp) (eqPrf eqType : Expr) :
-    OptionT SymM (Expr × Expr) := do
+    OptionT MetaM (Expr × Expr) := do
   let_expr Eq eqα _lhs _rhs := eqType
     | throwError "simp spec is not an equation: {eqType}"
   -- Unify the equation's type with the goal's program type. First-order approximation decomposes
@@ -316,7 +315,7 @@ same way.
   `info.Pred = σ1 → ... → σn → Prop`
 -/
 public def tryMkBackwardRuleFromSpec (specThm : SpecTheorem) (info : WPApp)
-    (stateArgNames : Array Name := #[]) : OptionT SymM BackwardRule := do
+    (stateArgNames : Array Name := #[]) : OptionT MetaM BackwardRule := do
   -- Instantiate the spec theorem, creating metavars for all universally quantified params
   let (_xs, _bs, specProof, specType) ← specThm.instantiate
   -- Equality specs (the simp side of `@[spec]`) are normalized to `⊑ wp` form, then handled like
@@ -329,6 +328,8 @@ public def tryMkBackwardRuleFromSpec (specThm : SpecTheorem) (info : WPApp)
   guard <| ← isDefEqGuarded info.Pred Pred'
   let_expr Std.WP.wp _Prog' _Value' _Pred' _EPred' _instAL' _instEAL' instWP' prog postSpec epostSpec := rhs
     | throwError "target not a wp application {rhs}"
+  -- `withDefault`: the goal can carry a registered `WP` instance (e.g. `Id.wpInst`) while the
+  -- spec spells `WPMonad.toWP ?inst`; default transparency unfolds both after `?inst` synthesis.
   guard <| ← withDefault <| isDefEqGuarded info.instWP instWP'
   -- Use local excess-state binders so explicit post premises can be re-lifted to `⊑`.
   -- Name them positionally from `stateArgNames` (else `s`) so the rule's binders carry good names.
@@ -339,8 +340,7 @@ public def tryMkBackwardRuleFromSpec (specThm : SpecTheorem) (info : WPApp)
     ssTypes := ssTypes.push ty
     ss := ss.push <| ← mkFreshExprMVar (userName := stateArgNames[i]?.getD `s) ty
   let res ← mkSpecBackwardProof pre prog postSpec epostSpec specProof info.EPred ss ssTypes stateArgNames
-  let expr ← Sym.canon res.expr
-  mkBackwardRuleFromExpr expr res.paramNames.toList
+  mkBackwardRuleFromExpr res.expr res.paramNames.toList
 
 /-! ## Split rules -/
 
@@ -446,7 +446,7 @@ condition `WP.Frames op prog F`, with the frame `F` left schematic and the weake
 frame. `analyzeFrameRule` records the positions of the schematic slots.
 -/
 public def mkFrameBackwardRule (fp : FrameProc) (info : WPApp) :
-    SymM FrameBackwardRule := do
+    MetaM FrameBackwardRule := do
   -- Pin the program and the operator, leaving everything else schematic;
   -- `tryMkBackwardRuleFromSpec` turns the unassigned metavariables into rule parameters.
   let op ← fp.mkOpAppM info

src/Std/WP/Monad/Instances.lean

@@ -41,13 +41,13 @@ namespace Std.WP
 variable {m : Type u → Type z}
 
 /-- `Id`'s `WP` interpretation: `Prop` assertions and no exceptions. -/
-@[instance_reducible] def Id.wpInst {α : Type u} : WP (Id α) α Prop EStack⟨⟩ where
+instance Id.wpInst {α : Type u} : WP (Id α) α Prop EStack⟨⟩ where
   wpTrans x := ⟨fun post _epost => post x⟩
   wp_trans_monotone x := fun _ _ _ _ _ hpost => hpost x
 
 /-- `Id` is a WPMonad with `Prop` assertions and no exceptions. -/
 instance Id.instWPMonad : WPMonad Id.{u} Prop EStack⟨⟩ where
-  toWP _ := Id.wpInst
+  toWP _ := inferInstance
   pure_le_wp_pure _ _ _ := PartialOrder.rel_refl
   bind_le_wp_bind _ _ _ _ := PartialOrder.rel_refl
 
@@ -86,7 +86,7 @@ instance {ε : Type u} {Pred : Type v} {EPred : Type w} {ε' : Type u}
 
 /-- `ExceptT`'s `WP` interpretation: lift the base interpretation by adding an exception
 postcondition layer. -/
-@[instance_reducible] def ExceptT.wpInst {Pred : Type v}
+instance ExceptT.wpInst {Pred : Type v}
   [Assertion Pred] [Assertion EPred] [WP (m (Except ε α)) (Except ε α) Pred EPred] :
     WP (ExceptT ε m α) α Pred ((ε → Pred) × EPred) where
   wpTrans x := PredTrans.pushExceptT (WP.wpTrans x.run)
@@ -103,7 +103,7 @@ postcondition layer. -/
 instance ExceptT.instWPMonad {Pred : Type v}
   [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] :
     WPMonad (ExceptT ε m) Pred ((ε → Pred) × EPred) where
-  toWP _ := ExceptT.wpInst
+  toWP _ := inferInstance
   pure_le_wp_pure x := fun post epost =>
     WPMonad.pure_le_wp_pure (m := m) (Except.ok x) (pushExcept post epost.fst) epost.snd
   bind_le_wp_bind x f := fun post epost => by
@@ -124,7 +124,7 @@ theorem ExceptT.wp_apply_eq {α ε Pred EPred}
 
 /-- `OptionT`'s `WP` interpretation: lift the base interpretation by adding a `Unit` exception
 postcondition layer. -/
-@[instance_reducible] def OptionT.wpInst {Pred : Type u}
+instance OptionT.wpInst {Pred : Type u}
   [Assertion Pred] [Assertion EPred] [WP (m (Option α)) (Option α) Pred EPred] :
     WP (OptionT m α) α Pred ((Unit → Pred) × EPred) where
   wpTrans x := PredTrans.pushOptionT (WP.wpTrans x.run)
@@ -140,7 +140,7 @@ postcondition layer. -/
 instance OptionT.instWPMonad {Pred : Type u}
   [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] :
     WPMonad (OptionT m) Pred ((Unit → Pred) × EPred) where
-  toWP _ := OptionT.wpInst
+  toWP _ := inferInstance
   pure_le_wp_pure x := fun post epost =>
     WPMonad.pure_le_wp_pure (m := m) (some x) (pushOption post epost.fst) epost.snd
   bind_le_wp_bind x f := fun post epost => by
@@ -160,7 +160,7 @@ theorem OptionT.wp_apply_eq {α : Type u} {Pred : Type u} {EPred}
     wp x post epost = wp x.run (pushOption post epost.fst) epost.snd := rfl
 
 /-- `StateT`'s `WP` interpretation: lift the base interpretation by adding a state argument. -/
-@[instance_reducible] def StateT.wpInst {EPred : Type v} {σ : Type u} {Pred : Type w}
+instance StateT.wpInst {EPred : Type v} {σ : Type u} {Pred : Type w}
   [Assertion Pred] [Assertion EPred] [WP (m (α × σ)) (α × σ) Pred EPred] :
     WP (StateT σ m α) α (σ → Pred) EPred where
   wpTrans x := pushArg (WP.wpTrans <| x.run ·)
@@ -174,7 +174,7 @@ theorem OptionT.wp_apply_eq {α : Type u} {Pred : Type u} {EPred}
 instance (priority := low) StateT.instWPMonad {EPred : Type v} {σ : Type u} {Pred : Type w}
   [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] :
     WPMonad (StateT σ m) (σ → Pred) EPred where
-  toWP _ := StateT.wpInst
+  toWP _ := inferInstance
   pure_le_wp_pure x := fun post epost s =>
     WPMonad.pure_le_wp_pure (m := m) (x, s) (fun p => post p.1 p.2) epost
   bind_le_wp_bind x f := fun post epost s => by
@@ -187,7 +187,7 @@ theorem StateT.wp_apply_eq {σ : Type u}
     wp x post epost s = wp (x.run s) (fun (a, s) => post a s) epost := rfl
 
 /-- `ReaderT`'s `WP` interpretation: lift the base interpretation by adding a reader argument. -/
-@[instance_reducible] def ReaderT.wpInst {Pred : Type v}
+instance ReaderT.wpInst {Pred : Type v}
   [Assertion Pred] [Assertion EPred] [WP (m α) α Pred EPred] :
     WP (ReaderT ρ m α) α (ρ → Pred) EPred where
   wpTrans x := ⟨fun post epost r => wp (x.run r) (fun a => post a r) epost⟩
@@ -201,7 +201,7 @@ theorem StateT.wp_apply_eq {σ : Type u}
 instance ReaderT.instWPMonad {Pred : Type v}
   [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] :
     WPMonad (ReaderT ρ m) (ρ → Pred) EPred where
-  toWP _ := ReaderT.wpInst
+  toWP _ := inferInstance
   pure_le_wp_pure x := fun post epost r =>
     WPMonad.pure_le_wp_pure (m := m) x (fun a => post a r) epost
   bind_le_wp_bind x f := fun post epost r => by
@@ -224,7 +224,7 @@ theorem ReaderT.wp_apply_eq {ρ : Type u}
 
 /-- `Option`'s `WP` interpretation: `Prop` assertions and a `Unit`-indexed exception
 postcondition. -/
-@[instance_reducible] def Option.wpInst {α : Type u} : WP (Option α) α Prop (Unit → Prop) where
+instance Option.wpInst {α : Type u} : WP (Option α) α Prop (Unit → Prop) where
   wpTrans x := ⟨fun post epost => pushOption post epost x⟩
   wp_trans_monotone x := fun post post' epost epost' hepost hpost => by
     cases x with
@@ -233,13 +233,13 @@ postcondition. -/
 
 /-- `Option` is a WPMonad with `Prop` assertions and a `Unit`-indexed exception postcondition. -/
 instance Option.instWPMonad : WPMonad Option.{u} Prop (Unit → Prop) where
-  toWP _ := Option.wpInst
+  toWP _ := inferInstance
   pure_le_wp_pure _ _ _ := PartialOrder.rel_refl
   bind_le_wp_bind x f := fun post epost => by cases x <;> exact id
 
 /-- `Except ε`'s `WP` interpretation: `Prop` assertions and an `ε`-indexed exception
 postcondition. -/
-@[instance_reducible] def Except.wpInst {α : Type u} : WP (Except ε α) α Prop (ε → Prop) where
+instance Except.wpInst {α : Type u} : WP (Except ε α) α Prop (ε → Prop) where
   wpTrans x := ⟨fun post epost => pushExcept post epost x⟩
   wp_trans_monotone x := fun post post' epost epost' hepost hpost => by
     cases x with
@@ -248,12 +248,12 @@ postcondition. -/
 
 /-- `Except ε` is a WPMonad with `Prop` assertions and an `ε`-indexed exception postcondition. -/
 instance Except.instWPMonad : WPMonad (Except ε) Prop (ε → Prop) where
-  toWP _ := Except.wpInst
+  toWP _ := inferInstance
   pure_le_wp_pure _ _ _ := PartialOrder.rel_refl
   bind_le_wp_bind x f := fun post epost => by cases x <;> exact id
 
 /-- `EStateM ε σ`'s `WP` interpretation combining state and exceptions. -/
-@[instance_reducible] def EStateM.wpInst {α : Type} : WP (EStateM ε σ α) α (σ → Prop) (ε → σ → Prop) where
+instance EStateM.wpInst {α : Type} : WP (EStateM ε σ α) α (σ → Prop) (ε → σ → Prop) where
   wpTrans x := ⟨fun post epost s => match x s with
     | .ok a s' => post a s'
     | .error el s' => epost el s'⟩
@@ -266,7 +266,7 @@ instance Except.instWPMonad : WPMonad (Except ε) Prop (ε → Prop) where
 
 /-- `EStateM ε σ` is a WPMonad combining state and exceptions. -/
 instance EStateM.instWPMonad : WPMonad (EStateM ε σ) (σ → Prop) (ε → σ → Prop) where
-  toWP _ := EStateM.wpInst
+  toWP _ := inferInstance
   pure_le_wp_pure x := fun post epost s => PartialOrder.rel_refl
   bind_le_wp_bind x f := fun post epost s => by
     simp only [WP.wp, WP.wpTrans, bind, EStateM.bind]