Stream: General

Topic: Making proofs with inductive predicates easier


view this post on Zulip 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?

view this post on Zulip Manuel Eberl (Jul 16 2020 at 12:31):

auto/force with suitable simp/intro/dest/elim rules doesn't do it?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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: Aug 15 2022 at 04:16 UTC