Currently, LamTerm.betaBounded may not fully beta reduce an expression regardless of how large an n it is given. This interacts poorly with LamTerm.betaReduceHacky and LamTerm.betaReduceHackyIdx, making it possible for auto's preprocessing to run into an infinite loop.
One example of this occurring can be seen in this theorem:
set_option auto.smt false in
set_option auto.tptp true in
set_option auto.native true in
theorem test {f : α → β} (P : (α → γ) → Prop)
(symbol1 : β → γ) (symbol2 : β → β)
(h : P ((symbol1 ∘ symbol2) ∘ f)) : False := by
auto [h, Function.comp_def] -- This should fail quickly rather than infinitely loop
There are presumably multiple ways to resolve this issue, but one simple way that I believe should work would be to change the last line of LamTerm.betaBounded from LamTerm.mkAppN fn argsb to (LamTerm.mkAppN fn argsb).betaBounded n' (and update the theorems LamTerm.maxEVarSucc_betaBounded and LamEquiv.ofBetaBounded accordingly).
Currently,
LamTerm.betaBounded
may not fully beta reduce an expression regardless of how large ann
it is given. This interacts poorly withLamTerm.betaReduceHacky
andLamTerm.betaReduceHackyIdx
, making it possible forauto
's preprocessing to run into an infinite loop.One example of this occurring can be seen in this theorem:
There are presumably multiple ways to resolve this issue, but one simple way that I believe should work would be to change the last line of
LamTerm.betaBounded
fromLamTerm.mkAppN fn argsb
to(LamTerm.mkAppN fn argsb).betaBounded n'
(and update the theoremsLamTerm.maxEVarSucc_betaBounded
andLamEquiv.ofBetaBounded
accordingly).