Hacktoberfest 2026: the issues maintainers tagged for October, open and beginner-friendly. Browse Hacktoberfest issues

`cbv` computes `List.maxOn?` as the minimum

Open
  • Is something wrong?
#15,625 0 comments 0 reactions 0 assignees View on GitHub

Maintainers usually reply within 1 day

Nobody has claimed this yet.

Assessment

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

Research direction

Start by comparing cbv and decide_cbv evaluation of [1, 3, 2].maxOn? id with decide and #eval, using the reproducer in the issue. Trace how cbv handles List.maxOn? and the proof terms for its comparisons; the issue gives no source file or test path. Done means both tactics prove the stated equality and their results agree with decide and #eval.

Written by the indexing model from the issue text.

Description

bug
Prerequisites
  • Check that your issue is not already filed (closest: #13544, see below).
  • Reduce the issue to a minimal, self-contained, reproducible test case.
  • Test your test case against the latest nightly release.
Description

cbv computes the minimum instead of the maximum for List.maxOn?: it evaluates [1, 3, 2].maxOn? id to
some 1 instead of some 3. The proof it builds is rejected by the kernel, and decide_cbv reports the
true proposition [1, 3, 2].maxOn? id = some 3 as false.

Steps to Reproduce
example : [1, 3, 2].maxOn? id = some 3 := by decide       -- ok
example : [1, 3, 2].maxOn? id = some 3 := by cbv          -- error (see below)
example : [1, 3, 2].maxOn? id = some 3 := by decide_cbv   -- error: the proposition evaluates to `false`

Expected behavior: cbv and decide_cbv prove the goal (decide, decide +kernel and #eval agree on
some 3).

Actual behavior:

error: unsolved goals
⊢ some 1 = some 3
error: (kernel) application type mismatch
  Eq.trans (congr (congrArg LE.le (id.eq_1 1)) (id.eq_1 3)) (Lean.Sym.Nat.le_eq_true 1 3 (eagerReduce (Eq.refl true)))
argument has type
  (1 ≤ 3) = True
but function has type
  (1 ≤ 3) = True → (id 1 ≤ id 3) = True
...
error: `decide_cbv` failed: the proposition evaluates to `false`
Versions

version 4.36.0-nightly-2026-10-11

Additional Information

NA

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.7k
Forks
1.1k
Avg merge
20h 22m
Merged PRs (30d)
298

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 DevTools issues

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.