Email Gateway (Aug 22 2022 at 18:00): Email Gateway (Aug 22 2022 at 18:00):From: Peter Lammich <lammich@in.tum.de>
Hi all,
During developing some Eisbach method, I recently encountered a very
inconvenient behaviour when chained facts are present.
My Eisbach method has the general shape
my_method = (rule rules | simp)+,
which seems quite natural to me. I always thought the semantics of this
is:
"Try applying a rule, and if this does not succeed, simplify the
goal. Do this as long until neither applying a rule nor simplifying the
goal changes something"
Now consider the following minimal example:
notepad begin
fix P Q assume R: "Q"
have "P (True ∧ True)"
using R
apply (simp)+
The apply step will loop forever! If I add an "apply -", i.e.,
apply - apply simp+
everything works as expected, and I get back the goal "Q ==> P True".
Also, if I remove the "using R" statement, everything works as
expected.
"apply my_method" has the same looping behaviour.
However, if I write apply (-, simp+), as I could also do inside my
Eisbach method, it still loops.
What is happening here, and how can I work around this "feature", to
get an Eisbach method that will not loop forever if chained facts are
present?
Thanks in advance for any help or comments,
Peter
Email Gateway (Aug 22 2022 at 18:01):From: Makarius <makarius@sketis.net>
As far as I can see on the spot, there is nothing special here, just
normal semantics of Isar proof methods: chained facts are always
inserted, even if there is a complex method expression.
Aside: this is the deeper reason, why proper Isar proofs should say "by
rule simp" and not "by (rule, simp)" to make clear where facts are
included and where not (even if the facts are empty).
For your Eisbach definition, you should get along with "use nothing in
simp". We specifically introduced the "use" method operator for that
situation, but it is generally useful to cleanup older tinkering with
chained facts.
Makarius
Email Gateway (Aug 22 2022 at 18:06):From: Peter Lammich <lammich@in.tum.de>
Hi Makarius,
thanks for the pointer to the "use" method combinator. I now have
use nothing in < insert method_facts, (rule rules | simp)+ >
which seems to be the intended behaviour of my method, where chained
facts make no sense. However, I still want to write things like
have ... using facts by my_method
where facts just provide additional knowledge to be used by the
simplifier, but should have no special meaning for the "rule rules".
Note that rules is just a named_theorems collection here, and it makes
little sense to chain in facts specific to these rules.
I'm not sure whether it would be better style to force the user to
inline any chained facts (and simply diverge if s*he forgets).
I.e. to write
by - my_method
and define my_method without a "use".
Email Gateway (Aug 22 2022 at 18:09):From: Makarius <makarius@sketis.net>
The last bit does not deserve the words "better style"; it looks more
like old-style facts tinkering for non-conformant proof tools.
Just abstractly, a proper proof method needs to use the primary
"method_facts" argument in a sensible way: neither ignore it, nor cause
bad behaviour when chained facts are provided.
You can also try an explicit facts argument for the Eisbach method
definition ("method test uses facts = ...") for the simp part.
I wonder how expert users of Eisbach usually do method facts handling.
Actually, I still have this TODO item left-over from some years ago:
"Eisbach: check/clarify chained facts for method expression".
Makarius
Last updated: Apr 26 2024 at 20:16 UTC