## Stream: General

### Topic: Making proofs with inductive predicates easier

#### 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 07 2023 at 08:19 UTC