Extremely verbose aesop panic

Stream: general

[Eric Wieser]

The following code (in mathlib master) produces 1595 panics:

import Mathlib.Data.Finset.Basic

example
    (n : List ℕ → List ℕ)
    (hn : ∀ A, n A = A.filter (fun p => true)) :
    0 ≤ 0 := by
  exact (0, not_not.1 $ by aesop)

all of which are

PANIC at Lean.MetavarContext.getLevelDepth Lean.MetavarContext:920:14: unknown metavariable

[Eric Wieser]

Waiting for an LSP message eventually gives

aesop: internal error: extracted proof has metavariables.
  Proof: Eq.mpr (id Init.Classical._auxLemma.2)
    (?m.2081 (Eq.mp (forall_congr fun A => congrArg (Eq (n A)) (List.filter_true A)) h₂'))
  Unassigned metavariables: [_uniq.6175, _uniq.6176]

[Eric Wieser]

It seems this is somehow caused by

@[simp, aesop safe apply (rule_sets := [finsetNonempty])]
theorem singleton_nonempty (a : α) : ({a} : Finset α).Nonempty :=
  ⟨a, mem_singleton_self a⟩

as the above example panics only after that lemma

[Eric Wieser]

Minimized to be mathlib-free at https://github.com/leanprover-community/aesop/issues/153

[Bhavik Mehta]

I just independently ran into the same aesop internal error, which seems to be caused by the same singleton_nonempty:

import Mathlib.Data.Finset.Card

lemma card_eq_two' {α : Type*} [DecidableEq α] {S : Finset α} (hS : S.card = 2)
    {a : α} (ha : a ∈ S) : ∃ b : α, a ≠ b ∧ S = {a, b} := by
  rw [Finset.card_eq_two] at hS
  obtain ⟨x, y, hxy, rfl⟩ := hS
  simp only [ne_eq, Finset.mem_insert, Finset.mem_singleton] at ha
  aesop

[Jannis Limperg]

This seems to be cause by a simp bug: lean4#5028

[Violeta Hernández]

Just came across a "aesop: internal error: extracted proof has metavariables." of my own.

[Violeta Hernández]

image.png
This is the goal state; doing refine fun _ ↦ ⟨n, ?_⟩ before this makes aesop work just fine.

[Violeta Hernández]

I'll try to minimize this to at least not depend on nimbers

[Violeta Hernández]

(deleted)

[Violeta Hernández]

This doesn't really break on Mathlib, though it doesn't solve the goal until you instantiate n.

import Mathlib.Algebra.Polynomial.Coeff

open Polynomial

example {R : Type*} [Semiring R] [PartialOrder R] [NeZero (1 : R)] [ZeroLEOneClass R] (p : R[X]) (n : ℕ) :
    (∀ m, n < m ∨ n = m → p.coeff m = 0) → (∀ (k : ℕ), n < k → p.coeff k = (X ^ n).coeff k) →
    ∃ n, p.coeff n < (X ^ n).coeff n := by
  aesop -- failed after exhaustive search