Tactic is never executed

Stream: new members

[Vasily Ilin]

Why does Lean not want my proof that p \leq 1 in this variable definition?

import Mathlib.Probability.ProbabilityMassFunction.Constructions
import Mathlib.Data.Real.Basic

variable (f : PMF Bool) (p : NNReal) (hp : p ≤ 1) (hf: f = PMF.bernoulli p (by simp [hp])) -- tactic is never executed

image.png

[Eric Wieser]

I think it wants you to write a theorem that uses hf

[Mario Carneiro]

that's probably a bug in the linter that it doesn't ignore that location, although it is arguably also a bug in variable that it doesn't actually run the tactic

[Mario Carneiro]

because it means that you don't get any error if you write something bogus there, leading to lean4#2226

[Vasily Ilin]

@Eric Wieser , I have lemmas in this file that use hf but the linter still complains.

[Kyle Miller]

This leads to no errors, which shouldn't be right because _ can't be inferred from the rest:

variable (f : PMF Bool) (p : NNReal) (hp : p ≤ 1) (hf: f = PMF.bernoulli p _)

[Kyle Miller]

I wonder if it's that the runTermElabM block in the variable definition isn't doing synthesizeSyntheticMVars

[Vasily Ilin]

I tried that, Kyle, and I noticed that once I used hf in a proof, I got a red underline under the _. But only after using hf in a proof.

[Kyle Miller]

Synthesizing synthetic mvars doesn't solve the _ problem, but it does cause by simp [hp] to evaluate at least.

import Mathlib.Probability.ProbabilityMassFunction.Constructions
import Mathlib.Data.Real.Basic

-- A new `variable` command based on the old one, but synthesize synthetic mvars
open private replaceBinderAnnotation in Lean.Elab.Command.elabVariable in
open Lean Elab Command in
elab "variable'" binders:(bracketedBinder)+ : command => do
  -- Try to elaborate `binders` for sanity checking
  runTermElabM fun _ => Term.withAutoBoundImplicit <|
    Term.elabBinders binders fun _ => Term.synthesizeSyntheticMVarsNoPostponing
  for binder in binders do
    let binders ← replaceBinderAnnotation binder
    -- Remark: if we want to produce error messages when variables shadow existing ones, here is the place to do it.
    for binder in binders do
      let varUIds ← getBracketedBinderIds binder |>.mapM (withFreshMacroScope ∘ MonadQuotation.addMacroScope)
      modifyScope fun scope => { scope with varDecls := scope.varDecls.push binder, varUIds := scope.varUIds ++ varUIds }

variable' (f : PMF Bool) (p : NNReal) (hp : p ≤ 1) (hf: f = PMF.bernoulli p (by simp [hp]))