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

vcgen: "Failed to apply split rule" for an over-applied `ite`, `(if c then f else g) x`

Open
  • Is something wrong?
#15,730 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
25/100
Issue type
Bug
Clarity
Clearly specified
Activity status
Active
Domain
devtools

Research direction

Start from the standalone reproducer in the issue: prog_spec fails with "Failed to apply split rule" on (if c then f else g) x, while prog_spec' succeeds on the pushed-in form. Find where vcgen's split rule matches ite and check why it does not handle an ite in function position with extra arguments. Done when prog_spec closes with vcgen [f_spec, g_spec] with finish and the existing Std.Tactic.Do tests still pass.

Written by the indexing model from the issue text.

Description

This issue was written by Claude (an AI assistant) on behalf of @nomeata.

Found while moving con-leche's cached-to-pure simulation proofs (a few thousand lines) to vcgen + grind (sym … => vcgen … <;> finish). Each case has a workaround in con-leche; the reproducer below is standalone.

vcgen cannot split an ite whose branches are functions applied to
further arguments ((if c then f else g) x), the shape a record field
fun c => if c then … else … has once the record is unfolded and the
field applied.

Expected: vcgen [f_spec, g_spec] splits (if c then f else g) x into
the two branches (as it does for if c then f x else g x).
Observed (v4.35.0 and nightly-2026-10-15): "Failed to apply split rule for (if c = true then f else g) x".
(con-leche task #359: simp only [coreKnotI] on the knot's whnfCore
field, ConLeche/Verify/Cached/KnotC.lean.)
Workaround: cases c first, or a restatement lemma
(coreKnotI_whnfCore_succ).

import Std.WP
import Std.Tactic.Do
open Std.WP
open scoped Lean.Order
set_option experimental.vcgen true

abbrev M := StateT Nat (Except String)

def f (x : Nat) : M Nat := modifyGet fun s => (x, s + 1)
def g (x : Nat) : M Nat := modifyGet fun s => (x, s + 2)

theorem f_spec (x s₀ : Nat) : ⦃fun s => s = s₀⦄ f x ⦃fun r s => r = x ∧ s = s₀ + 1; ⊤⦄ := by
  vcgen [f] with finish
theorem g_spec (x s₀ : Nat) : ⦃fun s => s = s₀⦄ g x ⦃fun r s => r = x ∧ s = s₀ + 2; ⊤⦄ := by
  vcgen [g] with finish

/-- Fails: "Failed to apply split rule". -/
theorem prog_spec (c : Bool) (x s₀ : Nat) :
    ⦃fun s => s = s₀⦄ (if c then f else g) x ⦃fun r _ => r = x; ⊤⦄ := by
  vcgen [f_spec, g_spec] with finish

/-- Works: the `ite` applied inside. -/
theorem prog_spec' (c : Bool) (x s₀ : Nat) :
    ⦃fun s => s = s₀⦄ (if c then f x else g x) ⦃fun r _ => r = x; ⊤⦄ := by
  vcgen [f_spec, g_spec] with finish
Dominant language
Lean
Stars
9.6k
Forks
1.1k
Avg merge
1d 4h
Merged PRs (30d)
290

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.