mvcgen bug? "declaration has metavariables"

Stream: Program verification

[Alexander Bentkamp]

Hello, I ran into the following issue with mvcgen. Is this a bug, @Sebastian Graf?

import Std.Tactic.Do
open Std.Do

def myfun : Except String Unit := sorry

@[spec]
theorem myfun_spec (h : True) :
  ⦃ ⌜ True ⌝ ⦄
  myfun
  ⦃ ⇓ r => ⌜ True ⌝ ⦄ := by sorry

@[spec]
def anotherfun : Except String Unit :=
  if true then pure () else pure ()

def program : Except String Unit := do
  anotherfun
  myfun

@[spec]
theorem spec :
  ⦃ ⌜ True ⌝ ⦄
  program
  ⦃ ⇓ _ => ⌜ True ⌝ ⦄ := by
  mvcgen [program]

On https://live.lean-lang.org/ (Lean Nightly), I get:

(kernel) declaration has metavariables 'spec'

[Sebastian Graf]

Thanks, I think I hit this bug on and off in the last couple of months but could never quite pin it down. Fixed in https://github.com/leanprover/lean4/pull/12048.

[Alexander Bentkamp]

Is there a good workaround for released Lean versions?

[Sebastian Graf]

Hmm. Unfortunately, I don't think it's a good workaround, but writing h : True in terms of an SPred [] could help:

theorem myfun_spec (h : ⊢ₛ (⌜True⌝ : SPred [])) :
  ...

There may be less noisy ways like defining an abbreviation for (h : ⊢ₛ (⌜.⌝ : SPred [])). The point of this workaround is that SPred metavars are properly turned into synthetic opaque metavariables, which currently does not happen for metavariables of most other types. If a metavar is not opaque, then abstracting the proof will also abstract the (natural or synthetic) metavar and in doing so assign it. The bug above is that mvcgen does not track that assignment. Maybe that helps you to come up with a better fix?

[Sebastian Graf]

Similar, cleaner workaround: Embed h : True in the precondition of the hoare triple instead of having a parameter. That goes against my recommendation in the tutorial but is effectively equivalent and works around the bug for now.

@[spec]
theorem myfun_spec :
  ⦃ ⌜True⌝ ∧ ⌜True ⌝ ⦄
  myfun
  ⦃ ⇓ r => ⌜ True ⌝ ⦄ := by sorry

[Alexander Bentkamp]

Thanks, those workarounds are good enough for me, I think!