internal `grind` error, term has not been internalized

Stream: lean4

[Aaron Liu]

This happened to me while working with docs#List.TProd (minimized):

example (n : Nat) (hn : (0 :: []).length = n)
    (ih : (List.foldr (fun i β => Fin i × β) PUnit.{1} ([] ++ [])) → False) : False := by grind

[Robin Arnez]

Huh seems like lean4#9572 was only half fixed. Yeah, probably worth opening another issue (or maybe reopening the old one)

[Edward van de Meent]

you can drop the n and hn hypotheses too

[Aaron Liu]

I thought I tried that and got "grind failed" instead of "internal grind error"

[Edward van de Meent]

oh, you're right

[Kim Morrison]

Yes, please open a new issue for this, thanks.

[Robin Carlier]

Also hitting a similar error, though in a quite different context that I have trouble minimizing.

The following is a Mathlib example. I had to redefine a few things because the live web editor is not up to date to the latest commit that turned SimplexCategory.Truncated to an abbrev, and this bug does not shows up if SimplexCategory.Truncated is a def.

import Mathlib
open CategoryTheory Simplicial SimplicialObject.Truncated
  SimplexCategory.Truncated

-- redefining some mathlib stuff as abbrev
abbrev SimplexCategory.Truncated' (n : ℕ) := ObjectProperty.FullSubcategory fun a : SimplexCategory => a.len ≤ n
abbrev δ' (m : Nat) {n} (i : Fin (n + 2)) (hn := by decide) (hn' := by decide) :
  (⟨⦋n⦌, hn⟩ : SimplexCategory.Truncated' m) ⟶ ⟨⦋n + 1⦌, hn'⟩ := SimplexCategory.δ i
abbrev σ' (m : Nat) {n} (i : Fin (n + 1)) (hn := by decide) (hn' := by decide) :
    (⟨⦋n + 1⦌, hn⟩ : SimplexCategory.Truncated' m) ⟶ ⟨⦋n⦌, hn'⟩ := SimplexCategory.σ i
abbrev δ₂' {n} (i : Fin (n + 2)) (hn := by decide) (hn' := by decide) := δ' 2 i hn hn'
abbrev σ₂' {n} (i : Fin (n + 1)) (hn := by decide) (hn' := by decide) := σ' 2 i hn hn'
lemma δ₂_zero_comp_σ₂_zero' {n} (hn := by decide) (hn' := by decide) :
    δ₂' (n := n) 0 hn hn' ≫ σ₂' 0 hn' hn = 𝟙 _ := SimplexCategory.δ_comp_σ_self

def SSet.Truncated' (n : ℕ) := (SimplexCategory.Truncated' n)ᵒᵖ ⥤ Type

example (X Y : SSet.Truncated' 2) (Δ : X.obj (Opposite.op ⟨⦋1⦌, by decide⟩)) :
    X.map (δ₂' 0).op (X.map (σ₂' 0).op Δ) = Δ := by
  grind [_=_ FunctorToTypes.map_comp_apply, _=_ op_comp, δ₂_zero_comp_σ₂_zero']

Error message is terse:

internal `grind` error, term has not been internalized
  Fin (1 + 2)

Any help minimizing this to file an issue would be appreciated, perhaps @Kim Morrison has an idea of what is happening here?

[Robin Carlier]

The conditions to hit the bug are pretty narrow: if I remove any of the three named lemmas in the grind call I get a standard "grind fail" message (which is expected) but the combination of these three has this effect.

[Kim Morrison]

Could you first check this on the nightly-testing-green branch? (You'll need to add the leanprover-community/mathlib4-nightly-testing fork as a for remote, and fetch that in order to get the branch.)

[Robin Carlier]

This is also present on nightly-testing-green.

[Robin Carlier]

(Should live.lean-lang.org also have a "nightly with Mathlib" backed by nightly-testing-green option? this would make things easier for quick checks.)

[Bhavik Mehta]

I've hit this error as well, seemingly in a different situation:

example {n m a : Nat} (ih : ∀ {a : Nat}, a ^ 2 = 4 ^ m * n → False)
    (h : a ^ 2 = 4 ^ (m + 1) * n) : False := by
  grind

[Kim Morrison]

Bhavik Mehta said:

I've hit this error as well, seemingly in a different situation:

example {n m a : Nat} (ih : ∀ {a : Nat}, a ^ 2 = 4 ^ m * n → False)
    (h : a ^ 2 = 4 ^ (m + 1) * n) : False := by
  grind

@Bhavik Mehta, your example simply fails, right? I don't see anything about "term has not been internalized".

[Bhavik Mehta]

On v4.24.0, and on current mathlib stable, the error is "internal grind error, term has not been internalized ?_mvar.617 ^ 2" I don't remember which version I used to report the one above, but I agree that on latest mathlib and current nightly, the error is different. I guess that whatever resolved Aaron's version also resolved mine.

[Kim Morrison]

Robin Carlier said:

Also hitting a similar error, though in a quite different context that I have trouble minimizing.

The following is a Mathlib example. I had to redefine a few things because the live web editor is not up to date to the latest commit that turned SimplexCategory.Truncated to an abbrev, and this bug does not shows up if SimplexCategory.Truncated is a def.

import Mathlib
open CategoryTheory Simplicial SimplicialObject.Truncated
  SimplexCategory.Truncated

-- redefining some mathlib stuff as abbrev
abbrev SimplexCategory.Truncated' (n : ℕ) := ObjectProperty.FullSubcategory fun a : SimplexCategory => a.len ≤ n
abbrev δ' (m : Nat) {n} (i : Fin (n + 2)) (hn := by decide) (hn' := by decide) :
  (⟨⦋n⦌, hn⟩ : SimplexCategory.Truncated' m) ⟶ ⟨⦋n + 1⦌, hn'⟩ := SimplexCategory.δ i
abbrev σ' (m : Nat) {n} (i : Fin (n + 1)) (hn := by decide) (hn' := by decide) :
    (⟨⦋n + 1⦌, hn⟩ : SimplexCategory.Truncated' m) ⟶ ⟨⦋n⦌, hn'⟩ := SimplexCategory.σ i
abbrev δ₂' {n} (i : Fin (n + 2)) (hn := by decide) (hn' := by decide) := δ' 2 i hn hn'
abbrev σ₂' {n} (i : Fin (n + 1)) (hn := by decide) (hn' := by decide) := σ' 2 i hn hn'
lemma δ₂_zero_comp_σ₂_zero' {n} (hn := by decide) (hn' := by decide) :
    δ₂' (n := n) 0 hn hn' ≫ σ₂' 0 hn' hn = 𝟙 _ := SimplexCategory.δ_comp_σ_self

def SSet.Truncated' (n : ℕ) := (SimplexCategory.Truncated' n)ᵒᵖ ⥤ Type

example (X Y : SSet.Truncated' 2) (Δ : X.obj (Opposite.op ⟨⦋1⦌, by decide⟩)) :
    X.map (δ₂' 0).op (X.map (σ₂' 0).op Δ) = Δ := by
  grind [_=_ FunctorToTypes.map_comp_apply, _=_ op_comp, δ₂_zero_comp_σ₂_zero']

Error message is terse:

internal `grind` error, term has not been internalized
  Fin (1 + 2)

Any help minimizing this to file an issue would be appreciated, perhaps Kim Morrison has an idea of what is happening here?

Okay, this one I've minimized as lean#11545. Not sure of the solution yet.

[Robin Carlier]

Thanks for taking the time to open the issue!

[Kim Morrison]

(This one is an example of how hard it is to write automation for dependent type theory... Leo has been performing wonders, but I'm not going to pre-empt what he thinks should be done here, and he's travelling at ItaLean at the moment.)