Mark Wassell (Jul 16 2020 at 12:00): Mark Wassell (Jul 16 2020 at 12:00):Hi, I have a set of mutually recursive inductive predicates that define a well-formedness condition for a language. I often need to prove well-formedness for various forms of terms in the language. These proofs are easy if I break them down into the consituent subgoals either using apply style or Isar style but they are getting tedious to do. If I throw all of the intros at sledgehammer,sledgehammer doesn't find a proof even though it seems 'obvious' to me. If I limit the set of facts to the facts I used to prove the wf condition by hand then sledgehammer finds the proof. Any suggestions on how I can prove these wf facts easily and in a general way?
Manuel Eberl (Jul 16 2020 at 12:31):auto/force with suitable simp/intro/dest/elim rules doesn't do it?
Mark Wassell (Jul 16 2020 at 12:58):Metis with all of the intros for the wf predicates + extras sometimes works. Sometimes a more refined set of intros is needed. In cases where these don't work a few steps of apply to break it up into simpler subgoals and then the above works.
Mark Wassell (Jul 16 2020 at 13:07):I have noticed that the structure of the rules for the inductive predicate might be a problem. One of the predicate rules is not syntax directed and if I do apply(rule+) it leads me to a subgoal that is not provable. I wonder if the automatic methods are going down the same path and get stuck. I will see if I can fix the rule.
Manuel Eberl (Jul 16 2020 at 13:13):Sledgehammer is also not great with higher-order stuff, I think. In case your rules are higher-order.
Simon Wimmer (Jul 16 2020 at 14:42):auto/force/fastforce will go down a similar path with intro rules as rule+. But there will be backtracking and intermediate simplifications. If they need to go down a "deep" path, the whole thing will likely explode and they will not succeed. Also note that the search depth of auto per default is highly limited.
Mohammad Abdulaziz (Jul 17 2020 at 09:16):Also note: the search depth for auto is configurable; it could be helpful to change it for experimenting or understanding why the automation fails in your case.
Last updated: Dec 21 2024 at 16:20 UTC