Zulip Chat Archive
Stream: lean4
Topic: Success is not monotone in `synthInstance.maxSize`
Eric Wieser (Jan 03 2025 at 23:07):
I'm in a situation where synthInstance.maxSize = 128
fails, but both 127 and 130 work. Wouldn't the expected behavior be that for any given problem, it succeeds until a certain limit, then fails everywhere below it?
import Mathlib
open Nat
set_option synthInstance.maxSize 128 -- the default; change to 127 and it works
abbrev broken := ∀ n : ℕ,
let bin := [1] ++ (digits 2 n) ++ [1];
Decidable <|
∀ i j : Fin bin.length, i < j → bin.get i = 1 → bin.get j = 1 →
(∀ k, i < k → k < j → bin.get k = 0) → Even ((j : ℕ) - (i : ℕ) - 1)
#synth broken
(cc @George Tsoukalas whose code this is extracted from)
Eric Wieser (Jan 03 2025 at 23:18):
Frustratingly it seemingly becomes monotone just after the default limit!
run_meta do
let fails ← (List.range 500).filterM fun x => do
withOptions (fun o => Lean.Meta.synthInstance.maxSize.set o x) do
let s ← getThe Meta.State
try
return ! (←succeeds (synthInstanceQ q(broken)))
finally
set s -- ensure the result isn't cached
Lean.logInfo m!"{fails}"
guard <| fails = List.range 22 ++ List.range' 30 6 ++ List.range' 63 4 ++ List.range' 128 2
Last updated: May 02 2025 at 03:31 UTC