fix: apply specs to goals with a registered WP instance in vcgen

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

@@ -310,7 +310,7 @@ For a spec already in `⊑ wp` form (`pre ⊑ wp prog post epost`, where the lat
 same way.
 
 - `info.Pred`: the goal's lattice type (e.g. `Nat → Prop`)
-- `info.instWP`: the `WPMonad` instance for the goal monad
+- `info.instWP`: the `WP` instance of the goal's `wp` application
 - `info.excessArgs`: free variables representing state args from
   `info.Pred = σ1 → ... → σn → Prop`
 -/
@@ -328,7 +328,9 @@ 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}"
-  guard <| ← isDefEqGuarded info.instWP instWP'
+  -- `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.
   let mut ss := #[]

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]

tests/elab/vcgenFrames.lean

@@ -60,24 +60,21 @@ theorem frames_mkFreshNat [Monad m] [Assertion Pred] [Assertion EPred]
 /-- `Id`-specialized `frames_mkFreshNat`. With the base monad ground, `grind` can derive a
 usable pattern, so registering it lets `finish` discharge the preservation VC. -/
 @[grind .]
-theorem frames_mkFreshNat_Id [Assertion Pred] [Assertion EPred]
-    [WPMonad Id Pred EPred] [∀ β (y : Id β), WPConjunctive y] {P : AppState → Pred}
+theorem frames_mkFreshNat_Id {P : AppState → Prop}
     (h : ∀ s a, P { s with fst := a } = P s) :
     WP.Frames (· ⊓ ·) (mkFreshNat : StateT AppState Id Nat) P :=
   frames_mkFreshNat h
 
 /-- The frame recovers `s.2`, which the lossy spec dropped. The `fail_if_success` confirms the frame
 is doing the work: without it, `grind` cannot close the lost `s.2 = 7`. -/
-theorem recovers_snd [Assertion Pred] [Assertion EPred] [WPMonad Id Pred EPred]
-    [∀ β (y : Id β), WPConjunctive y] [∀ a : Pred, PreservesSup (meet a)] :
+theorem recovers_snd :
     ⦃ fun s => ⌜s.1 = 0 ∧ s.2 = 7⌝ ⦄ (mkFreshNat : StateT AppState Id Nat)
     ⦃ fun r s => ⌜r = 0 ∧ s.2 = 7⌝ ⦄ := by
   fail_if_success (vcgen <;> grind)
   vcgen frames | mkFreshNat => fun s => ⌜s.2 = 7⌝ with finish
 
 /-- Two calls, two alternatives: consume-once frames each `mkFreshNat` exactly once. -/
-theorem recovers_snd_pair [Assertion Pred] [Assertion EPred] [WPMonad Id Pred EPred]
-    [∀ β (y : Id β), WPConjunctive y] [∀ a : Pred, PreservesSup (meet a)] :
+theorem recovers_snd_pair :
     ⦃ fun s => ⌜s.1 = 0 ∧ s.2 = 7⌝ ⦄ (mkFreshPair : StateT AppState Id (Nat × Nat))
     ⦃ fun p s => ⌜p.1 = 0 ∧ s.2 = 7⌝ ⦄ := by
   vcgen [mkFreshPair] frames
@@ -110,15 +107,13 @@ theorem frames_mkFreshSnd [Monad m] [Assertion Pred] [Assertion EPred]
 
 /-- `Id`-specialized `frames_mkFreshSnd`, registered so `finish` discharges the preservation VC. -/
 @[grind .]
-theorem frames_mkFreshSnd_Id [Assertion Pred] [Assertion EPred]
-    [WPMonad Id Pred EPred] [∀ β (y : Id β), WPConjunctive y] {P : AppState → Pred}
+theorem frames_mkFreshSnd_Id {P : AppState → Prop}
     (h : ∀ s a, P { s with snd := a } = P s) :
     WP.Frames (· ⊓ ·) (mkFreshSnd : StateT AppState Id Nat) P :=
   frames_mkFreshSnd h
 
 /-- Mirror of `recovers_snd`: frame the complementary (`fst`) footprint. -/
-theorem recovers_fst [Assertion Pred] [Assertion EPred] [WPMonad Id Pred EPred]
-    [∀ β (y : Id β), WPConjunctive y] [∀ a : Pred, PreservesSup (meet a)] :
+theorem recovers_fst :
     ⦃ fun s => ⌜s.1 = 5 ∧ s.2 = 0⌝ ⦄ (mkFreshSnd : StateT AppState Id Nat)
     ⦃ fun r s => ⌜r = 0 ∧ s.1 = 5⌝ ⦄ := by
   fail_if_success (vcgen <;> grind)
@@ -133,8 +128,7 @@ def mkFreshMixed [Monad m] [MonadStateOf AppState m] : m (Nat × Nat) := do
 
 /-- `mkFreshNat` (writes `fst`) and `mkFreshSnd` (writes `snd`) are framed by different alternatives:
 each recovers the component the other op's lossy spec would drop. -/
-theorem recovers_both [Assertion Pred] [Assertion EPred] [WPMonad Id Pred EPred]
-    [∀ β (y : Id β), WPConjunctive y] [∀ a : Pred, PreservesSup (meet a)] :
+theorem recovers_both :
     ⦃ fun s => ⌜s.1 = 0 ∧ s.2 = 7⌝ ⦄ (mkFreshMixed : StateT AppState Id (Nat × Nat))
     ⦃ fun p s => ⌜s.1 = 1 ∧ s.2 = 8⌝ ⦄ := by
   vcgen [mkFreshMixed] frames
@@ -168,16 +162,14 @@ theorem frames_addFst [Monad m] [Assertion Pred] [Assertion EPred]
 
 /-- `Id`-specialized `frames_addFst`, registered so `finish` discharges the preservation VC. -/
 @[grind .]
-theorem frames_addFst_Id [Assertion Pred] [Assertion EPred]
-    [WPMonad Id Pred EPred] [∀ β (y : Id β), WPConjunctive y] {P : AppState → Pred} {k : Nat}
+theorem frames_addFst_Id {P : AppState → Prop} {k : Nat}
     (h : ∀ s a, P { s with fst := a } = P s) :
     WP.Frames (· ⊓ ·) (addFst k : StateT AppState Id Nat) P :=
   frames_addFst h
 
 /-- The frame `fun s => ⌜s.2 = j⌝` references the matched argument `j`, so `elabFrame` introduces
 `let j := k` and the assignment is recovered in the postcondition. -/
-theorem recovers_with_arg [Assertion Pred] [Assertion EPred] [WPMonad Id Pred EPred]
-    [∀ β (y : Id β), WPConjunctive y] [∀ a : Pred, PreservesSup (meet a)] :
+theorem recovers_with_arg :
     ⦃ fun s => ⌜s.1 = 0 ∧ s.2 = k⌝ ⦄ (addFst k : StateT AppState Id Nat)
     ⦃ fun r s => ⌜r = 0 ∧ s.2 = k⌝ ⦄ := by
   fail_if_success (vcgen <;> grind)
@@ -211,15 +203,13 @@ theorem frames_bumpSnd {σ : Type} [Monad m] [Assertion Pred] [Assertion EPred]
 /-- `Id`-specialized `frames_bumpSnd` over an abstract state `σ`, registered so `finish`
 discharges the preservation VC. -/
 @[grind .]
-theorem frames_bumpSnd_Id {σ : Type} [Assertion Pred] [Assertion EPred]
-    [WPMonad Id Pred EPred] [∀ β (y : Id β), WPConjunctive y] {P : σ × Nat → Pred}
+theorem frames_bumpSnd_Id {σ : Type} {P : σ × Nat → Prop}
     (h : ∀ s a, P { s with snd := a } = P s) :
     WP.Frames (· ⊓ ·) (bumpSnd : StateT (σ × Nat) Id Nat) P :=
   frames_bumpSnd h
 
 /-- The frame recovers `s.1 = a` for an abstract `a : σ`, which the lossy spec dropped. -/
-theorem recovers_fst_poly {σ : Type} [Assertion Pred] [Assertion EPred]
-    [WPMonad Id Pred EPred] [∀ β (y : Id β), WPConjunctive y] [∀ a : Pred, PreservesSup (meet a)] {a : σ} :
+theorem recovers_fst_poly {σ : Type} {a : σ} :
     ⦃ fun s => ⌜s.1 = a ∧ s.2 = 0⌝ ⦄ (bumpSnd : StateT (σ × Nat) Id Nat)
     ⦃ fun r s => ⌜r = 0 ∧ s.1 = a⌝ ⦄ := by
   fail_if_success (vcgen <;> grind)
@@ -239,7 +229,7 @@ example [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred]
     ⦃ fun r s => ⌜r = 0 ∧ s.2 = 7⌝ ⦄ := by
   vcgen frames | mkFreshSnd => fun s => ⌜s.2 = 7⌝
 
-/-! ## The polymorphic frame lemmas instantiate at a concrete monad -/
+/-! ## The lemmas apply at the `StateM` alias -/
 
 example : ⦃ fun s => ⌜s.1 = 0 ∧ s.2 = 7⌝ ⦄ (mkFreshNat : StateM AppState Nat)
     ⦃ fun r s => ⌜r = 0 ∧ s.2 = 7⌝ ⦄ := recovers_snd
@@ -303,8 +293,7 @@ def selectiveFrameProc : FrameInferenceProc := fun i => do
 
 /-- `mkFreshNat_spec_guarded` is passed over; the clause still frames `s.2 = 7` when
 `mkFreshNat_spec_lossy` applies. -/
-theorem recovers_snd_second_candidate [Assertion Pred] [Assertion EPred] [WPMonad Id Pred EPred]
-    [∀ β (y : Id β), WPConjunctive y] [∀ a : Pred, PreservesSup (meet a)] :
+theorem recovers_snd_second_candidate :
     ⦃ fun s => ⌜s.1 = 0 ∧ s.2 = 7⌝ ⦄ (mkFreshNat : StateT AppState Id Nat)
     ⦃ fun r s => ⌜r = 0 ∧ s.2 = 7⌝ ⦄ := by
   vcgen frames | mkFreshNat => fun s => ⌜s.2 = 7⌝ with finish