Incrementality causes a weird error

[BrunoDutertre]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

In VScode, the kernel complains of an invalid proof term in the example below (I couldn't reduce it more).

(kernel) declaration has metavariables 'PFormula.nnf_of_pos_produces_nnf'

The error disappears on "Restart File" or after any small edit to the file. It reappears when the proof is modified.

inductive PFormula (α: Type): Type where
  | And: Array (PFormula α) → PFormula α
  | Or: Array (PFormula α) → PFormula α
  | Not: (PFormula α) → PFormula α
  | Atom: α → PFormula α

namespace PFormula

/-
Negative normal form
-/
def is_atom (f: PFormula α): Prop :=
  match f with
  | .Atom _ => True
  | _ => False

def is_nnf (f: PFormula α): Prop :=
  match f with
  | .And a | .Or a => all_nnf a
  | .Not g => g.is_atom
  | .Atom _ => True
where
  all_nnf (a: Array (PFormula α)): Prop := ∀ i, (k: i < a.size) → a[i].is_nnf

mutual
-- convert f to negative normal form
def nnf_of_pos (f: PFormula α): PFormula α :=
  match f with
  | .And a => And (a.mapIdx (fun i _ => nnf_of_pos a[i]))
  | .Or a => Or (a.mapIdx (fun i _ => nnf_of_pos a[i]))
  | .Not g => nnf_of_neg g
  | .Atom x => Atom x

-- convert (not f) to negative normal form
def nnf_of_neg (f: PFormula α): PFormula α :=
  match f with
  | .And a => Or (a.mapIdx (fun i _ => nnf_of_neg a[i]))
  | .Or a => And (a.mapIdx (fun i _ => nnf_of_neg a[i]))
  | .Not g => nnf_of_pos g
  | .Atom x => Not (Atom x)
end

theorem nnf_of_pos_produces_nnf {f: PFormula α}: is_nnf (nnf_of_pos f) := by
  induction f using nnf_of_pos.induct (motive2 := fun g => is_nnf (nnf_of_neg g))
  case case1 a ih | case2 a ih =>
    simp [nnf_of_pos, is_nnf, is_nnf.all_nnf]
    intro i h
    exact ih ⟨i, h⟩
  case case3 g ih =>
    simp only [nnf_of_pos]
    exact ih
  case case4 =>
    simp [nnf_of_pos, is_nnf]
  case case5 a ih | case6 a ih =>
    simp [nnf_of_neg, is_nnf, is_nnf.all_nnf]
    intro i h
    exact ih ⟨i, h⟩
  case case7 g  ih =>
    simp only [nnf_of_neg]
    exact ih
  case case8 =>
    simp [nnf_of_neg, is_nnf, is_atom]

end PFormula

Context

Talked with @leodemoura about this and he suspects that this is caused by incrementality.

Steps to Reproduce

It's a bit finicky but this might work

1. Load the example in vscode
2. If the error is not there. Comment out the case7 in the proof then put it back in.
3. Restarting lean on the file should make the error disappear.

Versions

4.10.0

Additional Information

[Additional information, configuration or data that might be necessary to reproduce the issue]

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.