(kernel) declaration has metavariables 'test'

Stream: lean4

[Alex Nekrasov]

I have a weird kernel error while trying to prove some theorems. Here is the example that I don't know how to further minimize:

import Mathlib.ModelTheory.Syntax

open FirstOrder

structure Program (L : Language) (m n : ℕ) where
  assignments : List (L.Term ℕ)
  outputs : List.Vector ℕ n
  well_formed : ∀ (assignment_idx : ℕ),
    ∀ (hassignmentIdx : assignment_idx < assignments.length),
    ∀ var_idx ∈ assignments[assignment_idx].varFinset,
    var_idx < m + assignment_idx
  outputs_well_formed : ∀ output_idx, outputs.get output_idx < m + assignments.length

variable {L : Language} {m n : ℕ}

def variableUsedInAssignment (prog : Program L m n) (varIdx : ℕ) : Prop :=
  varIdx ∈ prog.outputs.toList ∨
  ∃ assignmentIdx : ℕ,
    ∃ hassignmentIdx : assignmentIdx < prog.assignments.length,
      ∃ hassignmentIdx2 : varIdx ∈ prog.assignments[assignmentIdx].varFinset,
      variableUsedInAssignment prog (m + assignmentIdx)
termination_by m + prog.assignments.length - varIdx
decreasing_by
  have := prog.well_formed assignmentIdx hassignmentIdx varIdx hassignmentIdx2
  omega

variable (prog : Program L m n)

instance : DecidablePred (variableUsedInAssignment prog) := by
  sorry

theorem test
    (varIdx x : ℕ)
    (hx : x < prog.assignments.length)
    (h : (fun prog assignmentIdx ↦ variableUsedInAssignment prog (m + assignmentIdx)) prog varIdx)
    (this1 : m ≤ varIdx)
    (hx2 : varIdx ∈ prog.assignments[x].varFinset)
    (hk : (fun prog assignmentIdx ↦ variableUsedInAssignment prog (m + assignmentIdx)) prog x)
    (h3 : varIdx < m + prog.assignments.length) (h2 : (∀ (a : ℕ),
      (List.range prog.assignments.length)[varIdx - m]? = some a →
        ((fun prog assignmentIdx ↦ variableUsedInAssignment prog (m + assignmentIdx)) prog a) →
          ∀ (a : ℕ),
            ¬(List.scanl (fun acc x ↦ (if x = true then 1 else 0) + acc) 0
                    (List.map (fun assignmentIdx ↦ decide (variableUsedInAssignment prog (m + assignmentIdx)))
                      (List.range prog.assignments.length)))[varIdx - m]? =
                some a))
    : False := by
  rw [List.getElem?_eq_getElem, List.getElem_range] at h2
  have : variableUsedInAssignment prog (m + (varIdx - m)) := by
    unfold variableUsedInAssignment
    right
    use x
    use by omega
    use by simp_all only [Option.some.injEq, forall_eq', add_tsub_cancel_of_le]

  have h2 := h2 (varIdx - m) rfl this ((List.scanl (fun acc x ↦ (if x = true then 1 else 0) + acc) 0
        (List.map (fun assignmentIdx ↦ decide (variableUsedInAssignment prog (m + assignmentIdx)))
          (List.range prog.assignments.length)))[varIdx - m]'(by
          rw [List.length_scanl, List.length_map, List.length_range]
          omega))

  rw [List.getElem?_eq_getElem] at h2
  simp_all only [Option.some.injEq, not_false_eq_true, implies_true, forall_eq']
  rw [List.length_scanl, List.length_map, List.length_range]
  omega

This code gives following error: (kernel) declaration has metavariables 'test'

Furthermore, if I try to swap rw and have statements at the beginning of test, rw suddenly stops working at all:

import Mathlib.ModelTheory.Syntax

open FirstOrder

structure Program (L : Language) (m n : ℕ) where
  assignments : List (L.Term ℕ)
  outputs : List.Vector ℕ n
  well_formed : ∀ (assignment_idx : ℕ),
    ∀ (hassignmentIdx : assignment_idx < assignments.length),
    ∀ var_idx ∈ assignments[assignment_idx].varFinset,
    var_idx < m + assignment_idx
  outputs_well_formed : ∀ output_idx, outputs.get output_idx < m + assignments.length

variable {L : Language} {m n : ℕ}

def variableUsedInAssignment (prog : Program L m n) (varIdx : ℕ) : Prop :=
  varIdx ∈ prog.outputs.toList ∨
  ∃ assignmentIdx : ℕ,
    ∃ hassignmentIdx : assignmentIdx < prog.assignments.length,
      ∃ hassignmentIdx2 : varIdx ∈ prog.assignments[assignmentIdx].varFinset,
      variableUsedInAssignment prog (m + assignmentIdx)
termination_by m + prog.assignments.length - varIdx
decreasing_by
  have := prog.well_formed assignmentIdx hassignmentIdx varIdx hassignmentIdx2
  omega

variable (prog : Program L m n)

instance : DecidablePred (variableUsedInAssignment prog) := by
  sorry

theorem test
    (varIdx x : ℕ)
    (hx : x < prog.assignments.length)
    (h : (fun prog assignmentIdx ↦ variableUsedInAssignment prog (m + assignmentIdx)) prog varIdx)
    (this1 : m ≤ varIdx)
    (hx2 : varIdx ∈ prog.assignments[x].varFinset)
    (hk : (fun prog assignmentIdx ↦ variableUsedInAssignment prog (m + assignmentIdx)) prog x)
    (h3 : varIdx < m + prog.assignments.length) (h2 : (∀ (a : ℕ),
      (List.range prog.assignments.length)[varIdx - m]? = some a →
        ((fun prog assignmentIdx ↦ variableUsedInAssignment prog (m + assignmentIdx)) prog a) →
          ∀ (a : ℕ),
            ¬(List.scanl (fun acc x ↦ (if x = true then 1 else 0) + acc) 0
                    (List.map (fun assignmentIdx ↦ decide (variableUsedInAssignment prog (m + assignmentIdx)))
                      (List.range prog.assignments.length)))[varIdx - m]? =
                some a))
    : False := by
  have : variableUsedInAssignment prog (m + (varIdx - m)) := by
    unfold variableUsedInAssignment
    right
    use x
    use by omega
    use by simp_all only [Option.some.injEq, forall_eq', add_tsub_cancel_of_le]
  rw [List.getElem?_eq_getElem, List.getElem_range] at h2

  have h2 := h2 (varIdx - m) rfl this ((List.scanl (fun acc x ↦ (if x = true then 1 else 0) + acc) 0
        (List.map (fun assignmentIdx ↦ decide (variableUsedInAssignment prog (m + assignmentIdx)))
          (List.range prog.assignments.length)))[varIdx - m]'(by
          rw [List.length_scanl, List.length_map, List.length_range]
          omega))

  rw [List.getElem?_eq_getElem] at h2
  simp_all only [Option.some.injEq, not_false_eq_true, implies_true, forall_eq']
  rw [List.length_scanl, List.length_map, List.length_range]
  omega

tactic 'rewrite' failed, did not find instance of the pattern in the target expression (List.range ?m.6630)[?m.6629]

Is it some bug in the compiler or why does it happen?

[Mario Carneiro]

(kernel) errors are always a bug in a tactic somewhere

[Mario Carneiro]

reduced:

example {n} (h2 : (List.range n)[0]? = sorry) : False := by
  rw [List.getElem?_eq_getElem, List.getElem_range] at h2
  have h2 := h2
  sorry

[Mario Carneiro]

the have h2 := h2 is only needed to ensure that h2 actually appears in the proof term; rw has constructed an invalid proof term for it

[Mario Carneiro]

actually I think it's dropping a goal. With this sequence of rewrites, both getElem?_eq_getElem and getElem_range leave their h : i < l.length argument free to be filled by the rewrite, which can be nice sometimes but also causes problems if it never actually gets supplied. Normally this would end up as a separate subgoal (and you can actually see it appear after the first rewrite) but it seems to get dropped here for some reason

[Mario Carneiro]

Using List.getElem?_eq_getElem ?_ instead of List.getElem?_eq_getElem prevents the goal from getting dropped

[Alex Nekrasov]

Should I create an issue for this on GitHub? Also, how did you find out where exactly this metavariable is created? I'm curious because I'd like to know how to do it myself the next time I encounter this issue. I've run into this error dozens of times while trying to fix some proofs...

[Alex Nekrasov]

And I still don't understand the second example where rw and have are swapped. Why does the compiler fail to do rw, even when I use List.getElem?_eq_getElem ?_?

[Jovan Gerbscheid]

The problem here is that rw (and similarly apply) leave their metavariables as natural metavariables instead of syntheticOpaque metavariables. @Kyle Miller suggested at #general > Why does rfl fail to instantiate metavariables? @ 💬 that there may in the future be "synthetic semiopaque metavariables" that could be used instead. Hopefully that could solve this problem.