Lean Simp Tactics

• Bool: prove show (cond) = false from by decide then use Bool.false_eq_true, ↓reduceIte
• Prop: prove show ¬P from by omega then use ↓reduceIte

Don't use show P = false from by omega for Prop conditions — > on Nat creates a Prop, not a Bool.

Bool/Prop Bridging Quick Reference

Multiple sessions independently rediscover these patterns. This section consolidates all Bool↔Prop conversion patterns in one place.

Converting ==/!= (BEq) to =/≠ (Prop)

Pitfall: Nat.eq_of_beq_eq_true does NOT work — == produces BEq.beq, not Nat.beq. Use eq_of_beq (no namespace).

Pitfall: simp only [beq_iff_eq] rewrites ALL == in the goal, including inside lambdas/foldl. If you need targeted rewriting, use a scoped have (see "beq_iff_eq Over-Rewrites" section below).

Converting && compound guards to conjunctions

-- h : (a && decide P && decide Q) = true
simp only [Bool.and_eq_true, decide_eq_true_eq] at h
-- h : (a = true ∧ P) ∧ Q  (left-nested due to left-associative &&)
obtain ⟨⟨ha, hp⟩, hq⟩ := h

Resolving false = true in if conditions

After cases b on a Bool, if b then ... becomes if false then ... which elaborates to if (false = true) then ....

↓reduceIte does NOT work on false = true — see the ↓reduceIte Decision Guide section for the full table.

decide for concrete Bool/Prop evaluations

-- For concrete values: (1 : UInt32) &&& 1 = 1
decide

-- For implications from concrete rewrites: 0 = 0 → .raw = .raw
decide

-- For compound: htypeVal = 0 → typeVal ≠ 3
rw [htypeVal]; decide

Bool negation and or/and patterns

Cross-references

The Bool/Prop boundary appears in several other skills:

• lean-parsing-completeness: BEq to Prop bridging (for == guards)
• lean-wf-recursion: ↓reduceIte limitations with Bool-to-Prop coercion
• lean-simp-tactics: ↓reduceIte Decision Guide (this file, below)

Extracting Conditions from && Boolean Hypotheses

When a proof has hcond : (a && decide P && decide Q) = true from an if guard:

simp only [Bool.and_eq_true, decide_eq_true_eq] at hcond

This decomposes into hcond : (a = true ∧ P) ∧ Q.

Note: && is left-associative, so the result is left-nested (... ∧ ...) ∧ ..., NOT right-nested. Use obtain ⟨⟨ha, hp⟩, hq⟩ := hcond or hcond.1.2 / hcond.2 to access components.

let Bindings Are Opaque to omega

When a hypothesis hj contains an expanded expression (e.g. (List.map f xs).length) and you define let pl := List.map f xs, omega treats pl.length and (List.map f xs).length as distinct variables.

Fix with change j ≥ max 4 (pl.length - tw.length) at hj — change does definitional unfolding, making the terms syntactically identical for omega.

Don't try simp or rfl equations — they add complexity without helping omega.

simp Hypothesis Must Match Post-Rewrite Form

When using simp only [rewrite_eq, neg_hyp, ↓reduceIte], if rewrite_eq transforms the goal's condition (e.g. sym.toUInt16.toNat → sym), then neg_hyp must be stated in the post-rewrite form (e.g. ¬(sym - 257 ≥ ...), not ¬(sym.toUInt16.toNat - 257 ≥ ...)).

simp applies all rules together, so the hypothesis must match the normalized goal, not the pre-rewrite form.

letFun Linter False Positive

When unfold f at h leaves have x := e; body bindings, the letFun wrapper must be reduced before split at h can see inner if expressions.

The linter flags letFun as unused in simp only [letFun] at h because simp handles it via built-in reduction, not the named lemma. Replace with:

dsimp only at h  -- definitional reduction handles letFun

This eliminates the linter warning while performing the same reduction.

Fixing bind/Option.bind/Except.bind Linter Warnings

The linter flags bind, Option.bind, and Except.bind as unused in simp only [hX, bind, Option.bind] because they contribute only via dsimp. Do NOT suppress with set_option linter.unusedSimpArgs false — use the rw + dsimp pattern from the lean-monad-proofs skill instead:

rw [hX] at h; dsimp only [bind, Option.bind] at h ⊢

have Bindings That Look Unused but Feed omega/simp

omega and simp scan the entire local context for usable hypotheses. A have binding that is never referenced by name may still be critical:

have hlen_pos_nat : 0 < lengths[i].toNat := hlen  -- "unused" but omega needs it
have hlen_le : lengths[i].toNat ≤ maxBits := ...   -- "unused" but omega needs it
...
exact foo (by rw [hls_i]; omega)  -- omega closes via hlen_pos_nat + hlen_le

Before removing a have: Check whether any downstream omega, simp, or simp_all could be relying on it. The binding won't appear in grep results but omega uses it implicitly. Build after each removal to catch breakage.

Common pattern: UInt8/UInt16/UInt32 → Nat bridge hypotheses (hlen_pos_nat : 0 < x.toNat := hlen) exist specifically because omega works on Nat, not on UIntN. These are NOT dead code.

simp Destroys Type Info Needed for Recursive Call Inference

When proving length bounds for recursive functions, simp only [List.length_cons] reduces (x :: recursive_call).length to recursive_call.length + 1. After this, have := recursive_func _ _ _ fails because Lean can no longer infer the implicit arguments from the goal — the List structure connecting them is gone.

Fix: Use a type-bridge helper lemma that takes the recursive call as an argument (not via have). This works because Lean unifies the argument's type against the goal before simp runs:

-- Helper bridges the recursive call through simp
private theorem length_cons_le {n k s pos : Nat}
    (ih : n ≤ s - (pos + k)) (hk : k ≥ 1) (hle : pos + k ≤ s) :
    n + 1 ≤ s - pos := by omega

-- Usage: recursive call is an argument, not a have
simp only [List.length_cons]
exact length_cons_le (mainLoop_length _ _ _ _ _ _) (by omega) hle

Why have before simp also fails: Even with have ih := recursive_func _ _ _ before simp, Lean still can't infer implicit arguments if the goal doesn't directly mention the recursive call's result type.

Also: all_goals (have := f _ _; tac) with semicolons inside parenthesized tactic blocks can cause parse errors. Use separate focused proofs (·) instead.

Replacing Bare simp at h in Error Branches

When split at h or cases produces a contradictory hypothesis (e.g., h : Except.error e = Except.ok x), bare simp at h closes the goal via built-in discriminator analysis (reduceCtorEq simproc).

simp only cannot do this — it lacks the discriminator simproc. Neither simp only [] at h nor contradiction (max recursion in deeply nested contexts) are reliable replacements.

Canonical replacement: exact nomatch h

-- Before (bare simp)
split at h
· simp at h  -- closes Except.error _ = Except.ok _

-- After (targeted)
split at h
· exact nomatch h  -- constructor discrimination

For simp [hrb] at h that substitutes then closes:

-- Before
| error e => simp [hrb] at h

-- After (two steps: substitute + discriminate)
| error e => simp only [hrb] at h; exact nomatch h

-- After (one step: substitute + discriminate via rewrite in match)
| error e => exact nomatch (hrb ▸ h)

The one-step exact nomatch (hrb ▸ h) form works when hrb rewrites the hypothesis into an impossible constructor equality (e.g., none = some _). It's cleaner than the two-step form and commonly used for | none => branches where a have already established the substituted value.

Why nomatch works: Eq has one constructor (rfl) requiring definitional equality. Except.error _ and Except.ok _ are different constructors, so no pattern matches — nomatch h produces the empty match, proving False.

Batching error cases: To compress repeated split at h / · exact nomatch h patterns, use split at h; next => exact nomatch h (one line). Do NOT use split at h <;> try exact nomatch h — nomatch emits elaboration-level "Missing cases" errors that try does not catch.

repeat split at h Only Processes the First Goal

repeat tac in Lean 4 only retries tac on the first unsolved goal. After split at h creates goals A and B, repeat retries on A (which may have nothing to split), fails, and stops — leaving B unsplit.

For chained if-then-else splitting (e.g., highBitPos with 8 branches), use the flat pattern:

split at h
· handle_true_case  -- closes this goal
split at h           -- now operates on the remaining false case
· handle_true_case
...
handle_last_case     -- no more splits needed

Each split at h operates on whatever is the current goal after the · block closes the previous case. This correctly walks through all branches.

Evaluating if false = true then X else Y: Use if_neg Bool.false_ne_true since simp only [ite_false] requires the condition to already be False, not false = true (a decidable-but-not-reduced Prop).

simp only [] for Match Reduction

simp only [] (empty argument list) can reduce match expressions where the scrutinee is already a constructor:

-- After cases/split has resolved the scrutinee:
simp only []  -- reduces match (LZ77Token.literal b) with ...

This replaces patterns like simp only [htok] where the named hypothesis was unused by simp — the match reduction happens without it.

Limitation: simp only [] does NOT reduce Option.bind none f to none or other monadic chain reductions. These require the full @[simp] database. For deeply nested do-notation / Option.bind chains, bare simp [hyps] is often the only practical approach — converting to simp only would require explicitly listing every @[simp] lemma used in the bind reduction chain.

simp at h vs dsimp at h for if P then a else none = some b

When h : (if P then a else none) = some b, simp at h deduces that P must be true (since the else branch is none ≠ some b) and simplifies to h : a = some b. dsimp at h cannot do this — it only performs definitional reduction (iota, beta), not propositional reasoning about if.

This commonly arises in WF-recursive functions where the guard condition (e.g., if bits₁.length < br.toBits.length then ...) is embedded in the hypothesis. Replacing simp at h with dsimp at h will leave the guard unresolved, causing downstream proofs to fail because they lose the length bound that simp implicitly derived.

Rule: Use dsimp at h only for pure constructor/match reduction (e.g., reducing match LZ77Symbol.literal b with | .literal b => ...). Use simp at h when the hypothesis contains if P then ... else none patterns that need propositional resolution.

simp [hf] vs rw [if_pos/neg hf] in Monadic Proofs

In suffix/roundtrip proofs where the goal's condition differs syntactically from the hypothesis (e.g., goal has (bits ++ suffix).length but hypothesis proves about bits.length), simp [hf] can bridge the gap via List.length_append + arithmetic, while rw [if_pos/neg hf] and rw [dif_pos/neg hf] require exact syntactic match. Don't try to replace simp [hf] at hgo ⊢ with rw in these cases — it will fail.

↓reduceIte Decision Guide

After cases b on Bool: if b then 1 else 0 becomes if false then 1 else 0, which elaborates to @ite _ (false = true) (instDecidableEqBool false true) 1 0. ↓reduceIte does NOT reduce this because false = true is not literally False. Use dsimp instead — it performs definitional reduction through instDecidableEqBool.

Why dsimp works here: instDecidableEqBool computes definitionally to isFalse or isTrue, which dsimp can reduce via iota reduction. simp only [↓reduceIte] only handles the case where the decidable instance is already isTrue/isFalse at the syntax level. This distinction was independently discovered by two separate review sessions (PRs #764, #787).

After WF unfolding (rw [f.eq_1]), function bodies often contain if branches. The standard pattern: rw [f.eq_1]; simp only [h, ↓reduceIte] where h resolves the guard. See the lean-wf-recursion skill for details.

decide vs Structural Proofs for Large Finite Types

decide on large finite types (e.g., ∀ i : Fin 288, ...) requires high maxRecDepth. Replace with structural proofs that case-split on array