Zulip Chat Archive

Stream: general

Topic: grind? uses de Bruijn indices

Yaël Dillies (Jul 17 2025 at 17:19):

I am currently reading https://lean-lang.org/doc/reference/latest/The--grind--tactic/E___matching/#The-Lean-Language-Reference--The--grind--tactic--E___matching and finding it confusing that @[grind? ...] returns messages containing de Bruijn indices

Yaël Dillies (Jul 17 2025 at 17:19):

Taking an example from there:

axiom p : Nat → Nat
axiom q : Nat → Nat

/-- info: h₁: [q #1] -/
#guard_msgs (info) in
@[grind? →] theorem h₁ (w : 7 = p (q x)) : p (x + 1) = q x := sorry

Yaël Dillies (Jul 17 2025 at 17:20):

The corresponding example using grind_pattern would be

axiom p : Nat → Nat
axiom q : Nat → Nat

theorem h₁ (w : 7 = p (q x)) : p (x + 1) = q x := sorry

grind_pattern h₁ => q x

Yaël Dillies (Jul 17 2025 at 17:22):

q #1 is IMO very odd because:

  1. De Bruijn indices are supposed to be a Lean implementation detail
  2. grind_pattern uses the bound variable names, rather than their de Bruijn indices
  3. I can't wait to manually compute de Bruijn indices for complicated theorems with 20+ assumptions... :grinning:

Last updated: Dec 20 2025 at 21:32 UTC