help with a metavariable issue

Stream: lean4

[Scott Morrison]

There is some code in Mathlib.Lean.Meta that tries to determine if a goal g is "independent" of a list of other goals, in the sense that assigning a value to g cannot change the solvability of those other goals.

However it is unfortunately buggy, and I'd like some help sorting it out.

Here's src#Lean.MVarId.independent?:

/--
Check if a goal is "independent" of a list of other goals.
We say a goal is independent of other goals if assigning a value to it
can not change the solvability of the other goals.

This function only calculates a conservative approximation of this condition.
-/
def independent? (L : List MVarId) (g : MVarId) : MetaM Bool := do
  let t ← instantiateMVars (← g.getType)
  if t.hasExprMVar then
    -- If the goal's type contains other meta-variables,
    -- we conservatively say that `g` is not independent.
    return false
  if t.isProp then
    -- If the goal is propositional,
    -- proof-irrelevance should ensure it is independent of any other goals.
    return true
  if ← g.subsingleton? then
    -- If the goal is a subsingleton, it should be independent of any other goals.
    return true
  -- Finally, we check if the goal `g` appears in the type of any of the goals `L`.
  let r ← L.allM fun g' => do
    let t' ← instantiateMVars (← g'.getType)
    pure <| !(← exprDependsOn' t' (.mvar g))
  return r

[Scott Morrison]

Here's an example of it working fine:

import Mathlib.Lean.Meta
import Mathlib.Tactic.RunCmd

open Lean Elab Tactic

example : Σ α, Option α := by
  constructor
  -- Goals are `?fst : Type` and `?snd : Option ?fst`.
  -- Correctly, `independent?` claims neither is independent.
  -- (`?snd` because its type contains a metavariable, and `?fst` because `?snd`'s type depends on it)
  run_tac do
    let gs ← getGoals
    for g in gs do
      guard ! (← g.independent? gs)
  sorry

But it's easy to fool:

import Mathlib.Lean.Meta
import Mathlib.Tactic.RunCmd

open Lean Elab Tactic

example : Σ α, Option α := by
  constructor
  -- Now we introduce a hypothesis in the second goal
  rotate_left
  have := 0
  -- Now `independent?` incorrectly thinks `?fst` is independent.
  run_tac do
    let gs ← getGoals
    for g in gs do
      guard ! (← g.independent? gs) <|> throwError m!"{← g.getType} was incorrectly considered independent!"
  sorry

What's going on here? After the have, the goal state says:

case fst
this: Nat
⊢ Type ?u.8
case snd
⊢ Option
  (let_fun this := 0;
  ?m.39 this)

where ?m.39 : Nat → Type ?u.8 has "lost contact" with ?fst, and so independent? can see that actually ?fst does appear here.

[Scott Morrison]

(This problem causes the exact? bug reported earlier.)

[Damiano Testa]

Maybe I am misunderstanding, but when the target is a Type, I would have thought that "dependence" would be (also) that you are looking for a term of that type. So, maybe, replacing the last

    pure <| !(← exprDependsOn' t' (.mvar g))

with

    let defeq := ← isDefEq (← inferType t') (← g.getType'')
    pure <| !((← exprDependsOn' t' (.mvar g)) ∨ defeq)

is closer to what you want?

Sorry if this is just noise!

[Scott Morrison]

@Damiano Testa , I'm not sure what you mean. I think that situation is already being handled correctly:

import Mathlib.Lean.Meta
import Mathlib.Tactic.RunCmd

open Lean Elab Tactic

example : Σ α, α := by
  constructor
  -- Goals are `?fst : Type` and `?snd : ?fst`.
  -- Correctly, `independent?` claims neither is independent.
  -- (`?snd` because its type contains a metavariable, and `?fst` because `?snd`'s type depends on it)
  run_tac do
    let gs ← getGoals
    for g in gs do
      guard ! (← g.independent? gs)
  rotate_left
  sorry
  sorry

[Damiano Testa]

Hmm, this is strange: in the other case, the one where you expected something different, exprDependsOn' seems to give the opposite answer, though, or am I completely confused?

[Scott Morrison]

Yes, in the confusing case, that fact that I added an extra hypothesis means that exprDependsOn' can not see the dependence.

[Damiano Testa]

But the defeq check does say that the type of t' and the actual target of g are defeq.

[Damiano Testa]

So, I agree that in the latest working example exprDependsOn' is doing the right thing, but it seems to be confused by something else in the failing example from before.

[Scott Morrison]

The problem in the confusing situation is that the second goal depends on ?m.39 : Nat → Type ?u.8, rather than ?fst : Type ?u.8.

[Damiano Testa]

Ok, so you are saying that the defeq test does the right thing in this situation, because it is just telling you that the type of g' is "one-up" from the type of t' and this is because of the Nat → Type ?u.8, right?

(Btw, I have way more mvars than you do: fun (this : Nat) => ?_uniq.16536 this!)

[Scott Morrison]

I'm sorry, I don't understand.

[Damiano Testa]

While trying to answer your question, I realized that I need to think more about what I meant...

[Damiano Testa]

The fact that the question is about independence and the checks are for dependence and then the !s all conspire to confuse me.

[Damiano Testa]

In the confusing situation, exprDependsOn' t' (.mvar g) returns false, whereas we both agree that it should be true. Am I right about this?

[Scott Morrison]

Yes!

[Scott Morrison]

But the solution has to come from understanding the relationship between the ?m.X : Nat → Type ?u and ?fst : Type ?u.

[Damiano Testa]

Ok, I think that my confused message was trying to say: the defeq solution simply checks that some universes somewhere agree -- oh, this is a sign that they could be dependent on each other! I agree that it is too weak.

[Kyle Miller]

I've got one hint: ?m.39 is a delayed assignment, which is a metavariable with an entry in another table saying how it links up to another metavariable. The code for docs#Lean.Meta.getMVars will give you all metavariables, even accounting for delayed assignments.

I'm not sure if this is a bug in exprDependsOn' that it doesn't account for delayed assignments, or if it's working as intended.

[Kyle Miller]

Here's a version that uses docs#Lean.Meta.getMVars, and it seems to do the right thing.

import Mathlib.Lean.Meta
import Mathlib.Tactic.RunCmd

open Lean Elab Tactic

def Lean.MVarId.independent?' (L : List MVarId) (g : MVarId) : MetaM Bool := do
  let t ← instantiateMVars (← g.getType)
  if t.hasExprMVar then
    -- If the goal's type contains other meta-variables,
    -- we conservatively say that `g` is not independent.
    return false
  if t.isProp then
    -- If the goal is propositional,
    -- proof-irrelevance should ensure it is independent of any other goals.
    return true
  if ← g.subsingleton? then
    -- If the goal is a subsingleton, it should be independent of any other goals.
    return true
  -- Finally, we check if the goal `g` appears in the type of any of the goals `L`.
  L.allM fun g' => do
    let mvars ← Meta.getMVars (← g'.getType)
    pure <| !(mvars.contains g)

example : Σ α, Option α := by
  constructor
  -- Now we introduce a hypothesis in the second goal
  rotate_left
  have := 0
  run_tac do
    let gs ← getUnsolvedGoals
    for g in gs do
      let ty ← instantiateMVars (← g.getType)
      logInfo m!"{Expr.mvar g} : {ty} is independent = {(← g.independent?' gs)}"
  sorry
/-
?fst : Type ?u.3087 is independent = false

?snd : Option
  (let_fun this := 0;
  ?m.3118 this) is independent = false
-/

[Scott Morrison]

Thanks Kyle, this was super helpful! I think this is incorrect behaviour in exprDependsOn', I've made an issue at lean#2483 and a proposed fix at lean4#2484, and in the meantime your solution works in exact?.