Email Gateway (Aug 22 2022 at 10:41): Email Gateway (Aug 22 2022 at 10:41):From: Lars Hupel <hupel@in.tum.de>
Dear list,
I have a proof state which can be solved by the subsequent application
of two methods, i.e.
have "P x"
apply (induct x)
apply auto
done
If I rewrite this to
have "P x"
by (induct x) auto
the proof fails. Unfortunately I haven't been able to distill a small
example exhibiting this behaviour. Now, I know that "by x y" is
equivalent to "proof x qed y", but I always thought that is in turn
equivalent to "apply x apply y". Funnily enough, "by (x, y)" works. The
chained facts appear not to be significant here (I tried some variations).
Cheers
Lars
Email Gateway (Aug 22 2022 at 10:41):From: Lars Noschinski <noschinl@in.tum.de>
It is not. I am not sure about proof, but qed usually does a bit more
than apply (e.g., solve things by assumption).
Email Gateway (Aug 22 2022 at 10:41):From: Lars Hupel <hupel@in.tum.de>
It is not. I am not sure about proof, but qed usually does a bit more
than apply (e.g., solve things by assumption).
True, but shouldn't that mean that "by xy" solves more than "apply x apply
y done", instead of the other way round?
Email Gateway (Aug 22 2022 at 10:42):From: Lars Noschinski <noschinl@in.tum.de>
I would have expected that, yes. Does "proof x" create the same subgoals
as "apply x"? Does "proof x apply_end y qed" solve the goal?
-- Lars
Email Gateway (Aug 22 2022 at 11:14):From: Makarius <makarius@sketis.net>
(Back to this old thread.)
The above situation is indeed a bit odd. Too bad that there is not an
isolated experimental setup to test theories what is going on.
In principle the following equivalences of proof snippets hold:
by method1 method2
==
apply method1
apply method2
.
==
apply method1
apply method2
apply assumption*
done
But there are various fine points, notably backtracking: "by" composes all
possibilities with the Seq.THEN / Seq.EVERY combinator, while the "apply"
script takes each step separately and uses only the first result.
In PIDE interaction, there is also a difference in forked proofs: the
proof state for "by" looks technically a bit different. Well-behaved
proof methods should not be able to discern that, but who know what really
happens here. Note that in batch mode, both the "by" and "apply" proofs
are forked uniformly.
If you still happen to have that situation at hand, we could try to
explore it further.
Makarius
Last updated: Apr 20 2024 at 01:05 UTC