`grind`: kernel error because `abstractGroundMismatches?` passes the abstracted terms in reverse order

Closed
  • Is something wrong?
#15,700 0 comments 0 reactions 0 assignees View on GitHub

Maintainers usually reply within 1 day

A pull request for this has already been merged.

  • #15829 by @leodemoura — merged

Assessment

Difficulty
4/5
Estimated time
3-5 days
Newbie friendliness
35/100
Issue type
Bug
Clarity
Clearly specified
Activity status
Active
Domain
compilers

Research direction

Start in Lean/Meta/Tactic/Grind/ProveEq.lean, in abstractGroundMismatches? and the go helper whose (lhs, rhs) cache ignores offset. Reproduce with the headPos example, where the kernel reports an argument-order mismatch, and with the dep example. Done when both examples are accepted by the kernel, the abstracted terms are bound in the right order, and the cache key includes offset.

Written by the indexing model from the issue text.

Description

bug
Prerequisites
Description

The kernel rejects proofs produced by grind because an internal helper, abstractGroundMismatches?, passes the abstracted terms to its auxiliary function in reverse order. Ordinary code triggers it: grind [f], where f has a precondition such as "all elements are positive", stated by index.

Context

The goal is true: subst hx; rfl proves it, and so does subst hx; grind [headPos]. grind [headPos] also succeeds when the precondition mentions xs only once, for example ∀ i, i < xs.length → 0 < i + 1.

Steps to Reproduce

Run this file (no imports):

def headPos (xs : List Nat) (h : ∀ i, i < xs.length → 0 < xs[i]!) : Nat :=
  match xs with
  | a :: _ => a
  | [] => 1

example (xs : List Nat) (h : ∀ i, i < xs.length → 0 < xs[i]!) (hx : xs = [3]) : headPos xs h = 3 := by
  grind [headPos]

Expected behavior: grind proves the goal.

Actual behavior: The kernel rejects the generated proof:

error: (kernel) application type mismatch
  Lean.Grind.abstractFn (fun _x_0 _x_0_1 => ∀ (i : Nat), i < _x_0_1 → 0 < _x_0 i) xs.length
argument has type
  Nat
but function has type
  (Nat → Nat) → Nat → Prop
Versions

4.36.0-nightly-2026-10-14

Additional Information

In abstractGroundMismatches? (Lean/Meta/Tactic/Grind/ProveEq.lean), the k-th abstracted term is bound by the k-th innermost binder of the auxiliary lambda, but mkAppN f s.lhss / mkAppN f s.rhss pass the first term to the outermost one. With two or more abstracted terms (here xs.length and getElem! xs), the arguments are reversed. Suggested fix:

  return some (mkAppN f s.lhss.reverse, mkAppN f s.rhss.reverse)

Related: the (lhs, rhs) cache in go ignores offset, so a pair met again under more binders reuses a stale de Bruijn index, and grind throws an internal error. Suggested fix: add offset to the cache key.

def dep (x : Option Nat) (h : ∀ a, x = some a → ∀ b, x = some b → a = b) : Nat :=
  match x with
  | some a => a
  | none => 0

example (x : Option Nat) (hx : x = some 1) (H : ∀ a, x = some a → ∀ b, x = some b → a = b) :
    dep x H = 1 := by
  grind [dep]
Impact

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

Dominant language
Lean
Stars
9.8k
Forks
1.1k
Avg merge
14h 41m
Merged PRs (30d)
338

Getting set up

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

More from leanprover/lean4

All issues in leanprover/lean4

Similar issues

More Compilers issues

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.