unknown fvar in MetaM

Stream: lean4

[Adam Topaz]

I came across a somewhat subtle error:

import Mathlib.Algebra.Order.Ring.Defs
import Mathlib.Algebra.Order.Star.Basic

namespace StarOrderedRing

private lemma mul_le_mul_of_nonneg_left {R : Type*} [CommSemiring R] [PartialOrder R]
    [StarRing R] [StarOrderedRing R] {a b c : R} (hab : a ≤ b) (hc : 0 ≤ c) : c * a ≤ c * b := by
  rw [StarOrderedRing.nonneg_iff] at hc
  induction hc using AddSubmonoid.closure_induction with
  | mem _ h =>
    obtain ⟨x, rfl⟩ := h
    simp_rw [mul_assoc, mul_comm x, ← mul_assoc]
    exact conjugate_le_conjugate hab x
  | one => simp
  | mul x hx y hy =>
    simp only [← nonneg_iff, add_mul] at hx hy ⊢
    run_tac Lean.Elab.Tactic.withMainContext do
      let lctx ← Lean.getLCtx
      for (fvarId, decl) in lctx.fvarIdToDecl do
        let tp := decl.type
        Lean.Meta.forEachExpr tp fun e => do
          println! ← Lean.Meta.inferType e
    apply add_le_add <;> aesop

This is taken directly from Mathlib.Algebra.Order.Ring.Star. Here's what I think is going on: It seems that the fvar associated to hy is replaced in the simp only ... step, but it appears in another fvar in the local context. So when I try to traverse the expressions of the types of all fvars and infer the type, I reach the "old" hy at one point, and trying to infer the type causes an error.

I don't necessarily think there is anything to do about this, but I'm just wondering if this behavior is expected and/or known.

[Jannis Limperg]

There's definitely something fishy going on. One of the hypotheses is

a✝ : hx * a ≤ hx * b [?_uniq.1256 _uniq.2414 _uniq.2416]

where the stuff in brackets is the actual expression. _uniq.2416 is an fvar that doesn't appear in the context, but ?_uniq.1256 is a metavariable assigned to a function that throws away its second argument, so the fact that _uniq.2416 doesn't exist is 'irrelevant'. Except it isn't when we use forEachExpr because that'll happily visit _uniq.2416.

Here's a version that shows this behaviour more clearly:

import Mathlib.Algebra.Order.Ring.Defs
import Mathlib.Algebra.Order.Star.Basic

namespace StarOrderedRing

open Lean Lean.Meta in
private lemma mul_le_mul_of_nonneg_left {R : Type*} [CommSemiring R] [PartialOrder R]
    [StarRing R] [StarOrderedRing R] {a b c : R} (hab : a ≤ b) (hc : 0 ≤ c) : c * a ≤ c * b := by
  rw [StarOrderedRing.nonneg_iff] at hc
  induction hc using AddSubmonoid.closure_induction with
  | mul x hx y hy =>
    simp only [← nonneg_iff, add_mul] at hx hy ⊢
    run_tac Lean.Elab.Tactic.withMainContext do
      for decl in ← getLCtx do
        if decl.isImplementationDetail then
          continue
        logInfo m!"== {decl.userName} : {decl.type} [{toString decl.type}]"
        forEachExpr decl.type fun e => do
          logInfo $ toString $ e
          if let .mvar mvarId := e then
            logInfo m!"inst: {← instantiateMVars e}"
          discard $ inferType e
    sorry
  | _ => sorry

[Adam Topaz]

Thanks! I figured out that synthesizing synthetic mvars fixes the issue, so my explanation was probably wrong:

    run_tac Lean.Elab.Term.withSynthesize <| Lean.Elab.Tactic.withMainContext do
      let lctx ← Lean.getLCtx
      for (fvarId, decl) in lctx.fvarIdToDecl do
        let tp := decl.type
        Lean.Meta.forEachExpr tp fun e => do
          println! ← Lean.Meta.inferType e

I'm still investigating and your version of the run_tac is helpful!

[Jannis Limperg]

Now that confuses me even more... It's possible that the synthesising just happens to reduce this function application, so the unknown fvar disappears by accident.

[Adam Topaz]

I wonder if the missing fvar is in the lctx of the function mvar?

[Adam Topaz]

Well, I need to put the computer away for the rest of today. I’ll keep investigating tomorrow.