Email Gateway (Aug 22 2022 at 20:14): Email Gateway (Aug 22 2022 at 20:14):From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
Hi!
I’m developing a proof method that involves applications of drule.
This proof methods doesn’t work in the presence of chained facts,
because its drule invocations fail in this situation.
Consider the following minimal example code:
lemma "P ∧ Q ⟹ R"
apply (drule conjunct1)
oops
The invocation of drule correctly turns the goal into P ⟹ R.
However, it fails in the following situation:
lemma "P ∧ Q ⟹ R"
using TrueI
apply (drule conjunct1)
oops
Why is that, and how can drule been made work also in the presence of
chained facts?
I also tried to use erule instead of drule, but the same problem
occurred with that.
In my use case, I actually want to turn all chained facts into goal
premises anyhow. I can add the chained facts to the list of goal
premises by invoking insert method_facts, but this leaves the chained
facts in place, so that the problem with drule remains. Is there
perhaps a proof method that removes all chained facts?
I know that simp turns chained facts into goal premises. Therefore, my
current workaround is to invoke simp in a way where it essentially
doesn’t rewrite anything but only moves chained facts into the goal. To
this end, I’m using (insert TrueI, simp only: True_implies_equals). This has the side effect of removing all previously existing
True premises, but this isn’t a problem in my use case. Still, I’d be
happy to use a cleaner solution.
All the best,
Wolfgang
Email Gateway (Aug 22 2022 at 20:14):From: Wenda Li <wl302@cam.ac.uk>
Hi Wolfgang,
Although there might be better solutions and deeper understandings, my usual quick and dirty ways are:
lemma "P ∧ Q ⟹ R"
using TrueI
apply -
apply (drule conjunct1)
oops
Or
lemma "P ∧ Q ⟹ R"
using TrueI
apply (drule_tac conjunct1)
oops
Wenda
Email Gateway (Aug 22 2022 at 20:14):From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
I think the trick with apply - has nothing to do with the proof
method - but only works because the second apply never sees the
chained facts from the using that comes before the first apply.
Therefore this trick doesn’t work in an Eisbach definition, where you
use the comma operator to compose several proof methods into a single
one.
The trick with drule_tac works though.
All the best,
Wolfgang
Email Gateway (Aug 22 2022 at 20:14):From: "lammich@in.tum.de" <lammich@in.tum.de>
Oops, only sent that privately
Email Gateway (Aug 22 2022 at 20:14):From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
What I had overlooked is that when using (insert TrueI, simp only:
True_implies_equals), the simp invocation can still use the chained
facts as simplification rules, which can modify the goal further.
That said, I learned from fellow mailing list members that tactics turn
chained facts into goal premises. My new proof method for moving chained
facts into the goal is (insert TrueI, erule_tac TrueE). This also
doesn’t have the disadvantage of removing True premises that might
have been there in the first place.
All the best,
Wolfgang
Email Gateway (Aug 22 2022 at 20:15):From: Gidon Ernst <gidon.ernst@lmu.de>
Hi!,
there is "elim" and "intro" which use chained facts (but apparently no
"dest") that correspond to (erule ...)+ and (rule ...)+ respectively.
Note that they might loop.
Best,
Gidon
Email Gateway (Aug 22 2022 at 20:15):From: Yakoub Nemouchi <y.nemouchi@gmail.com>
Hi,
Goal focus is another way to inline chained facts. However, I am not sure
if this is the right usage of goal focus. It might be just a hacky style
from me.
Best wishes,
Yakoub.
Email Gateway (Aug 22 2022 at 20:15):From: Andreas Lochbihler <mail@andreas-lochbihler.de>
Hi all,
IMO the cleanest way is to use the "use" method, which takes another method and overwrites
what gets chained into the proof mehod. For example,
using TrueI
apply(use nothing in \<open>drule ...\<close>)
should work as expected. Note that "nothing" is the empty list of theorems. If you want to
chain in other theorems, just use their names.
The _tac versions of (d/e)rule are considered legacy because they allow access to raw goal
parameter names (which should be made available in the proof context using "subgoal" first).
Moreoer, elim and intro try to apply the given rules as often as possible, not just once
like (d/e)rule, and they behave differently when it comes to instantiating schematic
variables in the goals.
Hope this helps,
Andreas
Last updated: Apr 19 2024 at 08:19 UTC