Preventing mvcgen from instantiating meta-variables

Stream: Program verification

[Alexander Bentkamp]

Hello! I am experimenting with using mvcgen to generate pure functions from monadic functions. Here is an example:

import Std.Tactic.Do

open Std.Do

def monadicLe (a b : UInt8) : Except String Bool := sorry

@[spec]
theorem add_spec_pre (x y : UInt8) :
    ⦃⌜True⌝⦄
      monadicLe x y
    ⦃⇓ r => ⌜r = decide (x.toNat ≤ y.toNat)⌝⦄ := sorry

def test {a : UInt8} : { f : UInt8 → Bool // ⦃ ⌜ True ⌝ ⦄ monadicLe a 1 ⦃⇓ r => ⌜ r = f a ⌝ ⦄ } := by
  constructor
  mvcgen (config := {trivial := false, leave := false, elimLets := false})

#print test

Somehow mvcgen instantiates my meta-variable ?val although I turned off all the options that I thought might be responsible. What is the mechanism that instantiates ?val here?

[Sebastian Graf]

?val is instantiated by def eq when trying to discharge a verification condition by reflexivity (see trace.Meta.isDefEq.assign). I think it's sensible behavior, after all the solution is uniquely determined. It's the same kind of behavior as in

def test2 {a : UInt8} : { f : UInt8 → Bool // ∀ a, f a = true } := by
  constructor
  intro _
  rfl

I see the UX issue here... But I'm not sure it's solvable in mvcgen. The root issue is that the contructor tactic is implemented via apply Subtype.mk, and that appears to create natural metavariables for ?val and ?property. "natural" means they are eagerly assigned by isDefEq. Any tactic that uses a definitional equality check on ?val will assign ?val. If you don't want this, you can create the metavariable ?val yourself, so that it's born as synthetic opaque. Then it won't be assigned by isDefEq:

def test {a : UInt8} : { f : UInt8 → Bool // ⦃ ⌜ True ⌝ ⦄ monadicLe a 1 ⦃⇓ r => ⌜ r = f a ⌝ ⦄ } := by
  apply Subtype.mk ?val
  mvcgen (config := {trivial := false, leave := false, elimLets := false})
  case val => exact fun a => a.toNat ≤ 1
  rfl

Still, the rfl tactic (and trivial by extension) will assign ?val even though it's synthetic opaque, so that's a gotcha to be aware of:

def test2 {a : UInt8} : { f : UInt8 → Bool // ∀ a, f a = true } := by
  apply Subtype.mk ?val
  intro _
  rfl

[Alexander Bentkamp]

Okay, that makes sense! I'll wrap this mvcgen call into a custom tactic anyway, so creating a different kind of metavariable is a good solution for me. Thanks!