Email Gateway (Aug 22 2022 at 19:09): Email Gateway (Aug 22 2022 at 19:09):From: Cezary Kaliszyk <cezarykaliszyk@gmail.com>
Dear Isabelle list,
We have run across a slowdown of Isar core commands "show", "sorry" etc on
a statement with many fixes and assumes. In the attached the show+sorry takes
about a minute, and if we add more assumptions it seems to become twice slower
with every next quantifier.
Note that "have" is immediate, but if we use "show", it becomes slow.
The original Mizar text that we try to express in Isar is a formula of this
shape with 19 assumptions.
Is there a way to express this in Isar?
Regards,
Cezary
slow_show.thy
Email Gateway (Aug 22 2022 at 19:09):From: Peter Lammich <lammich@in.tum.de>
Hi.
the problem is that, when you finish the goal, the assumptions you made
are unified with the assumptions in the actual goal, in the order of
"assume" statements ... this causes an exponential blowup to find the
correct matches of the D(x)s ... try reordering your assume statements
to avoid this blowup. The attached example works in no time!
Email Gateway (Aug 22 2022 at 19:10):From: Cezary Kaliszyk <cezarykaliszyk@gmail.com>
Thanks, this works fast indeed!
We'll try to reverse this order for all translated proofs then.
Regards
Cezary
Last updated: Nov 21 2024 at 12:39 UTC