Hi! I recently started experimenting with lean-auto, primarily to explore its support for SMT solvers. However, I frequently encounter errors ending with Higher order input?, which are not always very informative and require manual debugging.
For instance, in the artificial example below, I initially could not locate the issue, but later realized that since f2 is a function, the entire term a could be considered higher-order.
set_option auto.smt true
set_option auto.smt.trust true
structure A where
f1 : List Nat
f2 : Nat → List Nat
example : ∀ (a : A) (n : Nat),
a.f1.length < n → a.f1.length ≤ n :=
by
intros a n
-- `auto` here reports `lamSort2STermAux :: Unexpected error. Higher order input?`
-- tried on Lean 4.9.0 and 4.11.0
sorry
On the other hand, it seems that some techniques, like term substitution using generalize, could potentially address this problem.
-- attempt again
example : ∀ (a : A) (n : Nat),
a.f1.length < n → a.f1.length ≤ n :=
by
intros a n
generalize a.f1 = ff
auto -- now it works!
However I am not entirely sure if this is a reliable solution. I would like to know if there is any plan to address these types of issues.
Hi! I recently started experimenting with
lean-auto, primarily to explore its support for SMT solvers. However, I frequently encounter errors ending withHigher order input?, which are not always very informative and require manual debugging.For instance, in the artificial example below, I initially could not locate the issue, but later realized that since
f2is a function, the entire termacould be considered higher-order.On the other hand, it seems that some techniques, like term substitution using
generalize, could potentially address this problem.However I am not entirely sure if this is a reliable solution. I would like to know if there is any plan to address these types of issues.