refactor: frame the lattice meet through the general gadget

Drop the meet-specific `meet_wp_imp_le_wp_skipFrame`; `vcgen` now frames every operator, the lattice meet included, through the single gadget `op_wp_upperAdjoint_le_wp_skipFrame` (renamed from `wp_imp_le_wp_skipFrame`, built on `WP.Frames.op_wp_upperAdjoint_le_wp`). The meet residual `upperAdjoint (meet F) b` is folded to `F ⇨ b` (definitionally equal: `himp` is the meet upper adjoint) by `foldUpperAdjointMeet?`, exposing the meet operand so the `himp` split decomposes it. `applyFrame` no longer branches on the operator.

Author: sgraf812

src/Lean/Elab/Tactic/Do/Internal/VCGen/Solve.lean

@@ -447,14 +447,11 @@ private def applyFrame (scope : VCGen.Scope) (goal : MVarId) (pre : Expr) (info
     | return .notFramed goal info
   -- `info.args.take 7` are the program's own `wp` arguments (program type, value, assertions, `WP`
   -- instance); `mkAppOptM` synthesizes the remaining instances against the assertion's own
-  -- `CompleteLattice` so the framing shares the structure the program's `wp` uses.
+  -- `CompleteLattice` so the framing shares the structure the program's `wp` uses. The lattice meet
+  -- is just the instance `op := (· ⊓ ·)`; its residual folds to `⇨` (see `foldUpperAdjointMeet?`).
   let specProof ←
-    if op.eta.getAppFn.isConstOf ``Lean.Order.meet then
-      Meta.mkAppOptM ``Std.Internal.Do.Gadget.meet_wp_imp_le_wp_skipFrame
-        ((info.args.take 7).map some ++ #[none, some F])
-    else
-      Meta.mkAppOptM ``Std.Internal.Do.Gadget.wp_imp_le_wp_skipFrame
-        ((info.args.take 7).map some ++ #[none, some op, none, some F])
+    Meta.mkAppOptM ``Std.Internal.Do.Gadget.op_wp_upperAdjoint_le_wp_skipFrame
+      ((info.args.take 7).map some ++ #[none, some op, none, some F])
   let some specThm ← mkSpecTheoremFromStx (← getRef) specProof
     | throwError "frame: could not build spec from the frame gadget for{indentExpr info.prog}"
   let some rule ← (tryMkBackwardRuleFromSpec specThm info).run
@@ -463,6 +460,21 @@ private def applyFrame (scope : VCGen.Scope) (goal : MVarId) (pre : Expr) (info
     | throwError "frame: failed to apply rule for{indentExpr info.prog}"
   return .framed scope subgoals
 
+/-- Fold a frame residual `upperAdjoint (meet F) b` on the RHS to Heyting `F ⇨ b` (definitionally
+equal: `himp` *is* the meet upper adjoint), exposing the meet operand `F` so the `himp` split can
+decompose it. This lets the lattice meet be framed by the general gadget like any operator, with no
+meet-specific spec; a non-meet operator's residual is left for its registered `impSplit`. -/
+private def foldUpperAdjointMeet? (goal : MVarId) (target rhs : Expr) : VCGenM (Option MVarId) := do
+  unless rhs.isAppOf ``Lean.Order.PreservesSup.upperAdjoint do return none
+  let args := rhs.getAppArgs
+  let some slice := args[2]? | return none
+  unless slice.isAppOf ``Lean.Order.meet && slice.getAppNumArgs == 3 do return none
+  let himpExpr ← Meta.mkAppM ``Lean.Order.himp #[slice.appArg!, args[3]!]
+  let newRhs ← mkAppNS himpExpr (args.extract 4 args.size)
+  let relArgs := target.getAppArgs
+  let newTarget ← mkAppNS target.getAppFn (relArgs.set! (relArgs.size - 1) newRhs)
+  return some (← goal.replaceTargetDefEq newTarget)
+
 /--
 The main VC generation step. Operates on a plain `MVarId` with no knowledge of grind.
 Returns `.goals subgoals` when the goal was decomposed, or a classification result
@@ -522,6 +534,7 @@ public def solve (scope : VCGen.Scope) (goal : MVarId) : VCGenM SolveResult := g
   -- Phase 3: shape the `rhs` (reduce an EPost projection, decompose a lattice connective), then
   -- discharge a residual entailment against the lifted hypothesis.
   if let some g ← reduceEPostHead? goal target α inst pre rhs then return .goals scope [g]
+  if let some g ← foldUpperAdjointMeet? goal target rhs then return .goals scope [g]
   if let some gs ← splitLatticeOp? goal rhs then return .goals scope gs
   if let some gs ← liftedHyp? scope goal α pre rhs then return .goals scope gs
 

src/Std/Internal/Do/WP/Frame.lean

@@ -35,8 +35,8 @@ structure WP.Frames {R : Type t} (op : R → Pred → Pred) (x : Prog) (F : R) :
 
 /-- The framed spec `vcgen` applies for `x`, when each `op r` preserves `Sup`: framing `x` by `F`
 makes `op F (wp x (fun a => PreservesSup.upperAdjoint (op F) (Q a)))` a precondition for `wp x Q`. -/
-theorem WP.Frames.conj_wp_imp_le_wp {R : Type t} (op : R → Pred → Pred) [∀ r, PreservesSup (op r)]
-    {x : Prog} {F : R} (hframes : WP.Frames op x F) :
+theorem WP.Frames.op_wp_upperAdjoint_le_wp {R : Type t} (op : R → Pred → Pred)
+    [∀ r, PreservesSup (op r)] {x : Prog} {F : R} (hframes : WP.Frames op x F) :
     ∀ Q E, op F (wp x (fun a => PreservesSup.upperAdjoint (op F) (Q a)) E) ⊑ wp x Q E := by
   intros
   apply PartialOrder.rel_trans

src/Std/Internal/Do/WP/FrameGadget.lean

@@ -23,27 +23,15 @@ variable {Prog : Type u} {Value : Type v} {Pred : Type w} {EPred : Type z}
 Stripped by `vcgen` before the real spec applies. -/
 def skipFrame {α : Sort u} (a : α) : α := a
 
-/-- `meet_wp_imp_le_wp` with the program wrapped in `skipFrame`, the per-call spec `vcgen`
-applies for a framed program. The frame `F` is the first explicit argument so that `vcgen` can
-partially apply it (pinning `F`) and feed the result through the ordinary spec machinery, leaving
-`x`, `epost`, `Q`, and `hframe` schematic. -/
-theorem meet_wp_imp_le_wp_skipFrame [∀ a : Pred, PreservesSup (meet a)] (F : Pred) (x : Prog)
-  (E : EPred) (Q : Value → Pred)
-    (hframes : WP.Frames meet x F) :
-    F ⊓ wp (skipFrame x) (fun a => F ⇨ Q a) E ⊑ wp x Q E := by
-  refine PartialOrder.rel_trans (hframes.conj_wp_le_wp_conj (fun a => F ⇨ Q a) E) ?_
-  apply WP.wp_consequence
-  intro a
-  exact meet_himp_le
-
-/-- `meet_wp_imp_le_wp_skipFrame` for an arbitrary frame operator `conj` whose slices preserve `Sup`,
-the per-call spec `vcgen` applies for a program framed with a non-meet operator. `conj` is the first
-explicit argument so that `vcgen` can pin it (to the inferred frame operator) while leaving `F`, `x`,
-`E`, `Q`, and `hframes` schematic. -/
-theorem wp_imp_le_wp_skipFrame {R : Type r} (conj : R → Pred → Pred) [∀ r, PreservesSup (conj r)]
-  (F : R) (x : Prog) (E : EPred) (Q : Value → Pred)
+/-- The per-call spec `vcgen` applies for a framed program: for a frame operator `conj` whose slices
+preserve `Sup`, framing by `F` runs the program under the upper adjoint of `conj F` and re-applies
+`conj F`. `conj` is the first explicit argument so that `vcgen` can pin it (to the inferred frame
+operator) while leaving `F`, `x`, `E`, `Q`, and `hframes` schematic. The lattice meet is the instance
+`conj := (· ⊓ ·)`, whose residual `vcgen` folds to Heyting `⇨`. -/
+theorem op_wp_upperAdjoint_le_wp_skipFrame {R : Type r} (conj : R → Pred → Pred)
+  [∀ r, PreservesSup (conj r)] (F : R) (x : Prog) (E : EPred) (Q : Value → Pred)
     (hframes : WP.Frames conj x F) :
     conj F (wp (skipFrame x) (fun a => PreservesSup.upperAdjoint (conj F) (Q a)) E) ⊑ wp x Q E :=
-  hframes.conj_wp_imp_le_wp _ _ _
+  hframes.op_wp_upperAdjoint_le_wp _ _ _
 
 end Std.Internal.Do.Gadget

tests/elab/vcgenTickFrames.lean

@@ -243,7 +243,7 @@ theorem tickFrames {α : Type} (x : TickM α) (F : Nat) (Q : α → Nat → Prop
     F ⋆ TickM.wp x Q EPost.Nil.mk ⊑ TickM.wp x (fun a => F ⋆ Q a) EPost.Nil.mk :=
   (frames_costConj x F).conj_wp_le_wp_conj Q EPost.Nil.mk
 
-/-- The framed-spec corollary, mirroring `WP.Frames.conj_wp_imp_le_wp`: running `x` under the magic
+/-- The framed-spec corollary, mirroring `WP.Frames.op_wp_upperAdjoint_le_wp`: running `x` under the magic
 wand `F -⋆ Q` and re-conjoining the budget `F` is a precondition for running `x` under `Q`. -/
 theorem tickFrames_imp {α : Type} (x : TickM α) (F : Nat) (Q : α → Nat → Prop) :
     F ⋆ TickM.wp x (fun a => F -⋆ Q a) EPost.Nil.mk ⊑ TickM.wp x Q EPost.Nil.mk := by