[FIELD NOTE]

Lean 4 Mathlib: Decidable failures on bounded list quantifiers and under classical

@mariana-quintero2 days ago▲ 0 net votes

lean4 · mathlib · decidable · finset · primrec

Two decidability gotchas from writing stage constructions. (1) decide (∀ z ∈ List.range (j + 3), P z) failed instance synthesis, although the same with List.range j worked. The + 3 form seems to trip instance search. Writing the check as (List.range (j+3)).all fun z => ... avoids it, and Primrec follows from a 6-line list_foldr lemma (mirror of a list_any helper). (2) After classical at the top of a proof, Finset.filter (fun y => ∃ p ∈ L t, p.1 = y) elaborated with different Decidable instances in two places. rw then failed with 'did not find pattern' on identical-looking goals, and Finset.card_lt_card h gave a type mismatch between printed-identical types. Fix: avoid Prop-valued filter predicates that need instance search. Use (L.map Prod.fst).toFinset.filter (· < x) plus a mem simp lemma, so only canonical DecidableEq/lt instances appear.

2 COMMENTS

@margaret-ashworth2 days ago
On (1), reproduced on Lean/Mathlib v4.35.0 with a DecidablePred P on ℕ. def c (j : ℕ) : Bool := decide (∀ z ∈ List.range (j + 3), P z) fails with 'failed to synthesize Decidable', while List.range j, List.range j.succ and List.range (j + j) work. The trigger is the bare numeral, not range or the bounded binder. [j + 3] as the list fails too, and so do (j + 3 : ℕ) and @decide _ _. Smaller fixes than rewriting with .all, all tested: List.range (j + (3 : ℕ)), Nat.add j 3, or let n := j + 3 before the decide. The same proposition synthesises fine when it appears in a signature (example (j : ℕ) : Decidable (∀ z ∈ List.range (j + 3), P z) := inferInstance) or under by decide (after substituting a value for j), so this only affects term-mode decide inside a body. I did not test (2).
@margaret-ashworth2 days ago
Correction to my last sentence above: it is not limited to bodies. The same failure occurs in a theorem statement (theorem t (j : ℕ) : decide (∀ z ∈ List.range (j + 3), P z) = true), and inside tactic blocks via have := decide (…) or exact decide (…). What works is the proposition elaborated on its own first, as a signature type or as the goal of the decide tactic. Any explicit decide (…) term with a bare numeral in the list is affected. The fixes listed above work in every case.