Zixuan Fan (Apr 10 2023 at 13:21): Zixuan Fan (Apr 10 2023 at 13:21):Hi, in my proof, I want to show an inequality relation like
B + B * B + d * B ≤ C + C * C + d * C
Apparently, if I have the the relation , I can apply this rule for quite a few times to show the goal, but it is tedious and repetitive to do so in Isar.
Additionaly, it seems like that no automatic method maybe helpful here. I thought linarith maybe efficient in this context, but it seems to only be able to apply the rule once. So I wonder if there is a better solution or any approach that I did not know.
Wolfgang Jeltsch (Apr 10 2023 at 13:24):What type do your variables have? If you just state the goal as it is, they will probably be of a type variable that is only guaranteed to be of the most general class providing + and *, which will probably give you no axioms about + and *. Well, given that linarith was at least partly successful, this is maybe not what happened, but it would still be good to first clarify what the types are.
Zixuan Fan (Apr 10 2023 at 13:25):I am showing some property about the cardinality, so the type has to be the nature number.
Wolfgang Jeltsch (Apr 10 2023 at 13:25):Have you tried proof-finding tools like try0, sledgehammer, or try (which involves the former two)?
Wolfgang Jeltsch (Apr 10 2023 at 13:25):Zixuan Fan said:
I am showing some property about the cardinality, so the type has to be the nature number.
And is it guaranteed to be of type natfrom the context?
Zixuan Fan (Apr 10 2023 at 13:26):Yes, that's where I found linarith is typically more efficient than other methods.
Zixuan Fan (Apr 10 2023 at 13:26):Wolfgang Jeltsch schrieb:
Zixuan Fan said:
I am showing some property about the cardinality, so the type has to be the nature number.
And is it guaranteed to be of type
natfrom the context?
Yes.
Wolfgang Jeltsch (Apr 10 2023 at 13:27):Doesn’t simp help then?
Wolfgang Jeltsch (Apr 10 2023 at 13:28):After all, it’s just application of ≤-congruence.
Zixuan Fan (Apr 10 2023 at 13:28):No, only sledgehammer yields a non-terminating proof.
Zixuan Fan (Apr 10 2023 at 13:30):Wolfgang Jeltsch schrieb:
After all, it’s just application of
≤-congruence.
That is just what I don't understand about. It seems that all the methods fails to find the intermiediate steps fo the relation. So I wonder if there is any method that is more helpful, or if Eisbach methods can be useful here.
Wolfgang Jeltsch (Apr 10 2023 at 13:46):On my machine, which runs Isabelle2022, sledgehammer finds the proof by (simp add: add_mono mult_le_mono). Here’s a complete working code snippet:
lemma
fixes B C d :: nat
assumes "B ≤ C"
shows "B + B * B + d * B ≤ C + C * C + d * C"
using assms by (simp add: add_mono mult_le_mono)
Maybe older Sledgehammer versions aren’t capable of finding this proof (I think they don’t find simp proofs), and try0 doesn’t search for additional rewrite rules to pass from what I know. In such situations, it can help to think about what lemmas would be needed, search for them using find_theorems, and then pass them to the proof method.
Zixuan Fan (Apr 10 2023 at 13:58):I see, my goal is a bit more complicated than my example, maybe that is why the sledgehammer does not work. But I guess I can figure out a way by looking for useful lemmas in this way. Thanks a lot!
Last updated: Apr 28 2024 at 08:19 UTC