fix: More consistent transparency when calling mspec from mvcgen (#9097)

This PR ensures that `mspec` uses the configured transparency setting
and makes `mvcgen` use default transparency when calling `mspec`.

Co-authored-by: Sebastian Graf <sg@lean-fro.org>

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

@@ -114,8 +114,11 @@ partial def dischargeFailEntails (ps : Expr) (Q : Expr) (Q' : Expr) (goalTag : N
 end
 
 def dischargeMGoal (goal : MGoal) (goalTag : Name) : n Expr := do
-  -- controlAt MetaM (fun map => do trace[Elab.Tactic.Do.spec] "dischargeMGoal: {(← reduceProj? goal.target).getD goal.target}"; map (pure ()))
+  liftMetaM <| do trace[Elab.Tactic.Do.spec] "dischargeMGoal: {(← reduceProj? goal.target).getD goal.target}"
   -- simply try one of the assumptions for now. Later on we might want to decompose conjunctions etc; full xsimpl
+  -- The `withDefault` ensures that a hyp `⌜s = 4⌝` can be used to discharge `⌜s = 4⌝ s`.
+  -- (Recall that `⌜s = 4⌝ s` is `SVal.curry (σs:=[Nat]) (fun _ => s = 4) s` and `SVal.curry` is
+  -- semi-reducible.)
   let some prf ← liftMetaM goal.assumption | mkFreshExprSyntheticOpaqueMVar goal.toExpr goalTag
   return prf
 
@@ -176,7 +179,7 @@ def mSpec (goal : MGoal) (elabSpecAtWP : Expr → n SpecTheorem) (goalTag : Name
     -- Often P or Q are schematic (i.e. an MVar app). Try to solve by rfl.
     -- We do `fullApproxDefEq` here so that `constApprox` is active; this is useful in
     -- `need_const_approx` of `doLogicTests.lean`.
-    let (HPRfl, QQ'Rfl) ← withDefault <| withAssignableSyntheticOpaque <| fullApproxDefEq <| do
+    let (HPRfl, QQ'Rfl) ← withAssignableSyntheticOpaque <| fullApproxDefEq <| do
       return (← isDefEqGuarded P goal.hyps, ← isDefEqGuarded Q Q')
 
     -- Discharge the validity proof for the spec if not rfl

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

@@ -350,7 +350,7 @@ where
         try
           let specThm ← findSpec ctx.specThms wp
           trace[Elab.Tactic.Do.vcgen] "Candidate spec for {f.constName!}: {specThm.proof}"
-          let (prf, specHoles) ← mSpec goal (fun _wp  => return specThm) name
+          let (prf, specHoles) ← withDefault <| mSpec goal (fun _wp  => return specThm) name
           assignMVars specHoles
           return prf
         catch ex =>

tests/lean/run/doLogicTests.lean

@@ -574,13 +574,7 @@ theorem unfold_to_expose_match_spec :
   ⦃⇓ r => ⌜r = 4⌝⦄ := by
   -- should unfold `Option.getD`, reduce the `match (some get) with | some e => e`
   -- and then apply the spec for `get`.
-  set_option pp.rawOnError true in
   mvcgen [unfold_to_expose_match, Option.getD]
-  -- TODO: This is weird, we should not need .rfl below.
-  -- `mspec` should be able to solve this,
-  -- but isDefEq seems to fail for `⌜s = 4⌝ = ⌜s = 4⌝ s`, whereas
-  -- it succeeds below. It must be some Config setting, but I don't know which.
-  exact .rfl
 
 theorem test_match_splitting {m : Option Nat} (h : m = some 4) :
   ⦃⌜True⌝⦄