Artem Khovanov (Jul 22 2022 at 00:00): Artem Khovanov (Jul 22 2022 at 00:00):I'm trying to use "of" to limit my search space for sledgehammer. I have the assumption
∀n ≤ degree f. P (coeff f n)
and want to using the fact P (coeff g (degree g)).
I tried writing using assms[of "degree g"].
However, I get the error
More instantiations than variables in theorem.
How do I fix this?
Wenda Li (Jul 22 2022 at 01:44):I guess your assms here contains more than one theorems :-) Try assms(1), assms(2), etc.
Artem Khovanov (Jul 22 2022 at 02:02):I have a new problem.. how can I apply a fact with a variable replaced?
have ind: "∀n. coeff f n ∈ K ⟹ set f ⊆ K" <proof>
I want the fact ∀n. coeff (deri_non_norm (a # P)) n ∈ K ⟹ set (deri_non_norm (a # P)) ⊆ K.
ind[of "deri_non_norm (a # P)"] gives the error More instantiations than variables in theorem.
When I using theorem, normally the state gives me variables like ?f, but this time it just gives me f. I assume this is the problem. How can I fix it?
Wenda Li (Jul 22 2022 at 02:05):ind[rule_format, of "deri_non_norm (a # P)"] perhaps?
Mathias Fleury (Jul 22 2022 at 04:54):or did you forget a for f / ⋀f in the step ind?
Mathias Fleury (Jul 22 2022 at 04:55):Try the following with and without the for f:
notepad begin
have ind: "∀n. coeff f n ∈ K ⟹ set f ⊆ K" for f sorry
thm ind[of f]
end
Unlike theorems, have do not generalize over arbitrary variables
Last updated: Apr 18 2024 at 08:19 UTC