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

vcgen: an equation in the spec list whose left-hand side is an `ite` program is not used; the `ite` is split first

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

Research direction

Start by running the standalone reproducer with set_option experimental.vcgen true, focusing on prog_spec, which fails, and prog_spec', which works. The issue points to the Std.WP and Std.Tactic.Do modules, where vcgen's handling of equational arguments is implemented. Done means prog_spec closes with guard_eq used to rewrite the ite before splitting, without a manual rw.

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.

An equational vcgen argument whose left-hand side is an ite program
is not used: vcgen splits the ite first.

Expected: vcgen [guard_eq, …] rewrites (if ok n then g n else pure 0)
to g n (as it rewrites any other program by an equation in its list),
leaving one verification condition about g.
Observed (v4.35.0 and nightly-2026-10-15): the ite is split; the else branch's condition
¬ ok n = true is a separate VC with pure 0, which here is unprovable
(the post needs g's answer), so finish fails on it.
Workaround: fold the equation into the caller's own unfolding equation
(con-leche: whnfAppI_cons states the loop with the ι arity guard
already discharged by iotaArityOk_guard).

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

def ok (n : Nat) : Bool := n % 2 == 0
/-- An answer only `g_spec` knows (as a walk's pure side is known only
through its callee specs). -/
@[irreducible] def spec (n : Nat) : Nat := if ok n then 1 else 0
def g (n : Nat) : StateT Nat (Except String) Nat := pure (spec n)

/-- The guard changes nothing: `g` answers `0` itself where `ok` fails. -/
theorem guard_eq (n : Nat) : (if ok n then g n else pure 0) = g n := by
  by_cases h : ok n = true
  · simp [h]
  · simp only [h, g]; unfold spec; simp [h]

theorem g_spec (n : Nat) (s₀ : Nat) :
    ⦃fun s => s = s₀⦄ g n ⦃fun r s => s = s₀ ∧ r = spec n; ⊤⦄ := by
  vcgen [g] with finish

def prog (n : Nat) : StateT Nat (Except String) Nat := do
  let r ← (if ok n then g n else pure 0)
  pure (r + 1)

/-- Fails: the `ite` is split, `guard_eq` unused. -/
theorem prog_spec (n : Nat) (s₀ : Nat) :
    ⦃fun s => s = s₀⦄ prog n ⦃fun r _ => r = spec n + 1; ⊤⦄ := by
  vcgen [prog, guard_eq, g_spec] with finish

/-- Works: the same rewrite done by hand first. -/
theorem prog_spec' (n : Nat) (s₀ : Nat) :
    ⦃fun s => s = s₀⦄ prog n ⦃fun r _ => r = spec n + 1; ⊤⦄ := by
  unfold prog; rw [guard_eq]
  vcgen [g_spec] with finish
Dominant language
Lean
Stars
9.6k
Forks
1.1k
Avg merge
1d 1h
Merged PRs (30d)
279

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.