hasLooseBVar misunderstanding?

Stream: lean4

[Sebastian Reichelt]

I'm trying to write my first Lean tactic (in Lean 4) and mostly just guessing a lot. So I'm not sure if "loose bvar" just means something different than I had guessed, or if I've stumbled upon a bug, or if I've built a term that is inconsistent in some way.

I would like to check if a lambda expression is constant in the sense that its body may reference anything except its own variable. Am I correctly assuming that I can check this with !b.hasLooseBVar 0, where b is the body? If not, what is the best way to do it?

The problem: Within my tactic, I have produced a term where hasLooseBVar 0 returns false, yet somewhere in an argument of an argument, the term contains a reference to bvar 0. When I print it, I see "#0" there as expected. The term does not itself contain any lambda abstractions, only applications, which hopefully rules out indexing issues. In case it matters, the term also contains a reference to bvar 1, and hasLooseBVar 1 does return true.

If necessary, I can try to create an MWE, but I'd like someone more knowledgeable to check whether my guesses are correct first. Thanks!

[Sebastian Ullrich]

Your intuition sounds about right, yes. Lean itself uses hasLooseBVar 0 in that manner, see e.g. Expr.eta.

[Sebastian Reichelt]

OK, I've managed to create a self-contained example. I'm sure it can still be minimized a lot.
While isolating the problem, I found that instantiateMVars fixes it. So now I'm unsure whether it is a Lean issue or not. The error message in the example below is still a bit unexpected.

import Lean

open Lean Expr Meta Elab Tactic

def swapLambdaParams (e : Expr) : MetaM Expr :=
  match e with
  | lam x X t _ => do
    let f ← mkFreshExprMVar none;
    let g ← mkFreshExprMVar none;
    if (← isDefEq t (mkApp f g)) then
      -- Uncommenting this line fixes the problem.
      --let g ← instantiateMVars g;
      let b := headBeta (mkApp2 (mkLambda x BinderInfo.default X g) (mkBVar 0) (mkBVar 1));
      unless b.hasLooseBVar 0 do
        throwError m!"{b} unexpectedly does not have any bvar 0"
      mkLambda "y" BinderInfo.default X (mkApp f (mkLambda x BinderInfo.default X b))
    else
      throwError "not defeq"
  | _ => throwError "not a lambda"

syntax (name := test) "test " term : tactic

@[tactic test] def Tactic.evalTest : Tactic := fun stx =>
  match stx with
  | `(tactic| test $e) => do
    let e' ← elabTerm e none;
    liftMetaTactic fun mvarId => do
      withMVarContext mvarId do
        checkNotAssigned mvarId `test
        let r ← swapLambdaParams e';
        assignExprMVar mvarId r;
        []
  | _ => throwUnsupportedSyntax

def f (g : Nat → Nat) := g 42
-- See error message.
def h : Nat → Nat := by test (λ x : Nat => f (λ y => x + y))

[Sebastian Ullrich]

Yes, hasLooseBVar does not see through assigned but not substituted metavariables. It cannot, as a pure function.