Email Gateway (Aug 18 2022 at 13:56): Email Gateway (Aug 18 2022 at 13:56):From: Juan Antonio Navarro Pérez <juannavarroperez@gmail.com>
Hi all,
I'm rather new in the world of Isabelle, and just started doing some
of my first few interesting proofs with it.
So far, I have found myself often in the situation when I want to
apply some kind of simplification rule, but in the inverse order as
I've stated it in a previous lemma. Say I have proved something like
-- lemma name [simp]: "complex = simple" -- but, during some
particular proof, I would like to replace _some_ occurrences of
"simple" with "complex".
Now, when I am this situations, I write a second -- lemma name_inv:
"simple = complex" by (auto) -- and then selectively apply (simp only:
name_inv) whenever I need it. But I'm, wondering if there is an
easier, more clean way of doing this.
Also how can I apply the simplification rule only to _some_
occurrences of an expression and not all of them (or all in the
conclusion, or all in the premises)??
To explain things a bit more precisely, consider for example that I
have already proved the following
lemma stack_append_assoc: "stack_append a (stack_append b c) =
stack_append (stack_append a b) c"
lemma push_append_cmt [simp]: "push_updates delta (stack_append st
st') = stack_append (push_updates delta st) st'"
which prove associativity of my "stack_append" function, and some sort
of commutativity between "stack_append" and some other "push_updates"
Now I'm trying to prove a lemma that looks like
lemma "stack_append (stack_eval c x bh) (stack_eval c x bt) =
stack_eval c x (stack_append bh bt)"
apply (induct bh)
apply (simp)
after starting the proof by induction and simplifications I end up
with a subgoal like
I would like, on the left-hand side of the equation, to move
"push_updates" before the "stack_append" (using the inverse of my
push_append_cmt) and then by associativity of the "stack_append"s
(again applied in the reverse direction of my original lemma) build
the expression "stack_append (stack_eval c x bh) (stack_eval c x bt)"
found in the inductive hypothesis to finally prove this subgoal.
Indeed, after defining some "stack_append_assoc_inv" and
"push_append_cmt_inv" lemmas, the proof of this subgoal succeeds by
applying
apply (simp only: push_append_cmt_inv)
apply (simp only: stack_append_assoc_inv)
But all this looks rather ugly. Is there a better/nicer way to do this?
Cheers,
Juan
Email Gateway (Aug 18 2022 at 13:57):From: Alexander Krauss <krauss@in.tum.de>
Hi Juan,
So far, I have found myself often in the situation when I want to
apply some kind of simplification rule, but in the inverse order as
I've stated it in a previous lemma. Say I have proved something like
-- lemma name [simp]: "complex = simple" -- but, during some
particular proof, I would like to replace _some_ occurrences of
"simple" with "complex".
apply (simp only: name[symmetric])
[...]
Also how can I apply the simplification rule only to _some_
occurrences of an expression and not all of them (or all in the
conclusion, or all in the premises)??
Have a look at the "subst" method (cf. Isabelle/Isar ref manual, sect.
9.2.2). Sometimes it is also helpful to instantiate the rule manually,
such that it applies only at certain positions:
apply (simp only: name[where x="foo"]
Then, of course, if you find out that you often have to apply your rules
"backwards", you may simply have written them in the "wrong" direction.
It often takes some experimentation to find out what works best...
Hope this helps
Alex
Email Gateway (Aug 18 2022 at 13:58):From: Tobias Nipkow <nipkow@in.tum.de>
If you need to do a lot of these low level term manipulations, in most
cases something is wrong. For example, the direction
lemma "stack_append (stack_eval c x bh) (stack_eval c x bt) =
stack_eval c x (stack_append bh bt)"
looks wrong. As a programmer you would orient it the other way around.
Since your application is close to programming, you should think like a
programmer (better: term rewriter).
If you don't know how to avoid this low-level term surgery, you should
use structured proofs and especially the
also have "... = rhs"
idiom. For apply proofs the "subst" method may help because it allows
you to specify which occurrences should be replaced. But structured
proofs are less brittle.
Regards
Tobias
apply (induct bh)
apply (simp)after starting the proof by induction and simplifications I end up
with a subgoal like
- !!fun list bh.
stack_append (stack_eval c x bh) (stack_eval c x bt) =
stack_eval c x (stack_append bh bt)
==> stack_append (stack_append (push_updates list (c x fun))
(stack_eval c x bh)) (stack_eval c x bt) =
stack_append (push_updates list (c x fun)) (stack_eval c x
(stack_append bh bt))I would like, on the left-hand side of the equation, to move
"push_updates" before the "stack_append" (using the inverse of my
push_append_cmt) and then by associativity of the "stack_append"s
(again applied in the reverse direction of my original lemma) build
the expression "stack_append (stack_eval c x bh) (stack_eval c x bt)"
found in the inductive hypothesis to finally prove this subgoal.Indeed, after defining some "stack_append_assoc_inv" and
"push_append_cmt_inv" lemmas, the proof of this subgoal succeeds by
applying
apply (simp only: push_append_cmt_inv)
apply (simp only: stack_append_assoc_inv)But all this looks rather ugly. Is there a better/nicer way to do this?
Cheers,
Juan
Email Gateway (Aug 18 2022 at 13:58):From: Juan Antonio Navarro Pérez <juannavarroperez@gmail.com>
Alexander and Tobias!
Thank you very much for the hints and pointers! Indeed reversing the
order of some of my simplifications has made the proofs go much
smoother.
I'll keep an eye on the commands that you suggested me to check.
Best,
Juan
Last updated: Nov 21 2024 at 12:39 UTC