Stream: Beginner Questions

Topic: Automatic reordering of current facts to apply rule


view this post on Zulip Mark Wassell (Aug 18 2020 at 08:03):

I have situations where my current facts contain facts that match some of the premises of a rule I wish to apply and may also include additional ones. Doing "then have mygoal proof(rule myrule)" doesn't work as the list of premises in myrule does not match the list of current facts.

For example, my current facts are A B C, I need to prove P and I have a rule B ⇒ A ⇒ D ⇒ P.

Is there a way of applying the rule so that the appropriate ordering of current facts is done automatically so that the rule can be applied. If not can Eisbach help?

view this post on Zulip Lukas Stevens (Aug 18 2020 at 08:06):

By using from instead of then you can reorder the facts, e.g. from this(2,3,1) have ...

view this post on Zulip Mark Wassell (Aug 18 2020 at 08:14):

Thanks, I handn't throught to use this( <list of numbers> ).

I am still interested in any automatic method of finding the ordering as the proof is not robust if the ordering of the current facts changes. The use case I have in mind is inductive predicate proofs where the 'case' introduces a number of facts and the order can change if I make a change to the rule that introduces new premises or deletes them.

view this post on Zulip Lukas Stevens (Aug 18 2020 at 08:17):

I am not sure if something like this exists. In some cases it would quite hard to discern the right ordering, for example if you have the rule x < y ==> y < z ==> x < z

view this post on Zulip Manuel Eberl (Aug 18 2020 at 08:17):

I guess you could try something like by (rule myrule; rule this; fail)

view this post on Zulip Manuel Eberl (Aug 18 2020 at 08:18):

but depending on how much ambiguity there is, that might cause a lot of backtracking

view this post on Zulip Manuel Eberl (Aug 18 2020 at 08:18):

if there is no ambiguity, it should work without problems

view this post on Zulip Manuel Eberl (Aug 18 2020 at 08:19):

as Lukas said, it is not always the case that there is a clear "correct" ordering, so I don't think there is a builtin Isar method that tries to do something like that

view this post on Zulip Peter Zeller (Aug 18 2020 at 18:40):

You might want to try my fuzzy_rule method: https://github.com/peterzeller/isabelle_fuzzy_rule
It's an attempt to get rid of the strict ordering and strict matching requirements of rule

view this post on Zulip Mark Wassell (Aug 19 2020 at 07:03):

Thanks, I will take a look. The matching requirement was another thing I was looking for some flexibility on.


Last updated: Aug 13 2022 at 06:26 UTC