Chengsong Tan (Nov 01 2023 at 07:40): Chengsong Tan (Nov 01 2023 at 07:40):Hi all,
A bit curious but potentially due to scalability issues,
I copy-pasted a subgoal from a theorem into a lemma preceding that theorem and marked that lemma with sorry.
Now proving that subgoal for that theorem seems not viable for some reason, even if there's an identical lemma proven just before it.
sledgehammer is not able to find a proof, and I tried giving it hints such as using subgoal_lemma and still got no luck.
I was wondering why this happens and how to solve it? Did I make an error or it is a limitation of Isabelle? If the latter I guess the workaround would be to simplify that subgoal into smaller bits in that theorem and prove it directly there.
Best wishes,
Chengsong
Attathed file:
Transposed.thy
(
see line marked with (Here) (line 1871)
)
Mathias Fleury (Nov 01 2023 at 08:02):This works:
apply (rule subgoal1_simplified_form; assumption)
Sledgehammer works for me with sledgehammer(add:subgoal1_simplified_form)
Mathias Fleury (Nov 01 2023 at 08:04):I did not check what metis is doing, but it should be able to solve the goal
Mathias Fleury (Nov 01 2023 at 08:05):but there could some let problems here
Chengsong Tan (Nov 01 2023 at 08:17):Mathias Fleury said:
This works:
apply (rule subgoal1_simplified_form; assumption)
Thank you! This works like a charm.
What does the command assumption mean?
Chengsong Tan (Nov 01 2023 at 08:17):Mathias Fleury said:
but there could some let problems here
What is a let problem?
Mathias Fleury (Nov 01 2023 at 11:30):assumption means to unify with one the assumptions in the goal
Mathias Fleury (Nov 01 2023 at 11:31):Chengsong Tan said:
Mathias Fleury said:
but there could some let problems here
What is a let problem?
I never remember if let is unfolded when passed to metis. This kind of things can make the term much bigger and much harder to recognize
Last updated: May 02 2024 at 12:29 UTC