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?
auto/force with suitable simp/intro/dest/elim rules doesn't do it?
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.
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.
Sledgehammer is also not great with higher-order stuff, I think. In case your rules are higher-order.
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.
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 07 2023 at 08:19 UTC