fix: apply specs stated via reducible abbreviations (#14089)

This PR lets `mvcgen` and `mvcgen'` apply `@[spec]` theorems whose
statement is a reducible abbreviation wrapping a Hoare triple, such as
`abbrev foo.spec := ⦃P⦄ foo ⦃Q⦄`. Previously the program stayed stuck
because the spec, although registered, was discarded at lookup time.

The spec database recovers the triple from the proof's type via
`SpecProof.instantiate`, which performs no whnf, and then matches the
`Triple` head syntactically. For an abbreviation-typed spec the head is
the abbreviation constant, so the match failed: `mvcgen` rejected the
candidate in `findSpec`, while `mvcgen'` first failed to migrate the
entry and then failed to build the backward rule. Reduce the
instantiated type with `whnfR` at these three sites before matching
`Triple`.

Author: sgraf812

src/Lean/Elab/Tactic/Do/Attr.lean

@@ -452,6 +452,9 @@ private def mkSpecTheorem (type : Expr) (proof : SpecProof) (prio : Nat) : MetaM
   let (levelParams, expr) ← proof.getProof
   let type ← instantiateMVars type
   let (_, _, type) ← forallMetaTelescope type
+  -- Reduce reducible abbreviations so a proof whose type is an abbreviation like
+  -- `abbrev s := ⦃P⦄ prog ⦃Q⦄` is recognized as a triple spec.
+  let type ← whnfR type
   let some _ ← selectProg type | return none
   let pattern ← mkSpecPatternFromExpr expr levelParams
   return some { pattern, proof, priority := prio }

src/Lean/Elab/Tactic/Do/Spec.lean

@@ -30,6 +30,9 @@ public def findSpec (database : SpecTheorems) (wp : Expr) : MetaM SpecTheorem :=
   trace[Elab.Tactic.Do.spec] "Candidates for {prog}: {candidates.map (·.proof)}"
   let specs ← candidates.filterM fun spec => do
     let (_, _, _, type) ← spec.proof.instantiate
+    -- Reduce reducible abbreviations so a proof whose type is an abbreviation like
+    -- `abbrev s := ⦃P⦄ prog ⦃Q⦄` is recognized as a triple spec.
+    let type ← whnfR type
     trace[Elab.Tactic.Do.spec] "{spec.proof} instantiates to {type}"
     let_expr c@Triple m ps instWP α specProg _P _Q := type | throwError "Not a triple: {type}"
     let check := isDefEqGuarded wp (mkApp5 (mkConst ``WP.wp c.constLevels!) m ps instWP α specProg)
@@ -177,6 +180,9 @@ public def mSpec (goal : MGoal) (elabSpecAtWP : Expr → n SpecTheorem) (goalTag
 
   -- Fully instantiate the specThm without instantiating its MVars to `wp` yet
   let (mvars, _, spec, specTy) ← specThm.proof.instantiate
+  -- Reduce reducible abbreviations so a proof whose type is an abbreviation like
+  -- `abbrev s := ⦃P⦄ prog ⦃Q⦄` is recognized as a triple spec.
+  let specTy ← whnfR specTy
 
   -- Instantiation creates `.natural` MVars, which possibly get instantiated by the def eq checks
   -- below when they occur in `P` or `Q`.

tests/elab/mvcgenSpecAbbrev.lean

@@ -0,0 +1,48 @@
+import Std.Internal.Do
+import Std.Tactic.Do
+
+/-!
+Tests that `mvcgen` and `mvcgen'` apply a `@[spec]` theorem whose *type* is a
+reducible abbreviation wrapping a Hoare triple, e.g. `abbrev foo.spec := ⦃P⦄ foo ⦃Q⦄`.
+The triple is recovered from the proof's type and must be reduced through the
+abbreviation before it is recognized as a `Triple`.
+-/
+
+set_option mvcgen.warning false
+
+/-! `mvcgen` over a legacy `Std.Do` triple. `foo` is `irreducible`, so the
+postcondition `r = 1` can only be discharged via the registered spec (`r = 0`). -/
+section
+open Std.Do
+
+@[irreducible] def foo : Id Nat := pure 0
+
+abbrev foo.spec := ⦃⌜True⌝⦄ foo ⦃⇓r => ⌜r = 0⌝⦄
+
+@[spec] theorem foo.spec.proof : foo.spec := by
+  unfold foo.spec foo; mvcgen <;> grind
+
+example :
+    ⦃⌜True⌝⦄
+    do let x ← foo; pure (x + 1)
+    ⦃⇓r => ⌜r = 1⌝⦄ := by
+  mvcgen <;> grind
+
+end
+
+/-! `mvcgen'` over a new-metatheory `Std.Internal.Do` triple. `G` is an `axiom`,
+so discharging `wp⟦G⟧` requires the registered spec. -/
+section
+open Std.Internal.Do Lean.Order
+set_option warn.sorry false
+
+axiom G : StateM Nat Unit
+
+abbrev G.spec := ⦃fun (_ : Nat) => True⦄ G ⦃fun _ n => n = n⦄
+
+@[spec] axiom G.spec.proof : G.spec
+
+example : ⦃fun (_ : Nat) => True⦄ G ⦃fun _ n => n = n⦄ := by
+  mvcgen'
+
+end