Email Gateway (Aug 19 2022 at 08:02): Email Gateway (Aug 19 2022 at 08:02):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Hi all again,
I have a question from part of “prog-prove.pdf”
On page 34, “prog-prove.pdf”, propose a inductive definition:
inductive star :: "('a ⇒ 'a ⇒ bool) ⇒ ('a ⇒ 'a ⇒ bool)"
for r
where
refl: "((star r) x x)"
| step: "(r x y) ⟹ ((star r) y z) ⟹ ((star r) x z)"
Then it suggest that “star r” is transitive and invite the reader to prove
it. As the transitivity looked not obvious to me, I was afraid the proof
may be not that simple, but it was.
The e‑book suggest to prove it this way:
lemma star_trans: "((star r) x y) ⟹ ((star r) y z) ⟹ ((star r) x z)"
apply (induction rule: star.induct)
apply (assumption)
apply (metis step)
done
But I did it this way:
lemma star_trans: "((star r) x y) ⟹ ((star r) y z) ⟹ ((star r) x z)"
apply (induction x y rule: star.induct)
apply (assumption)
apply (simp)
apply (simp add: step)
done
The two first steps are obvious, and the e‑books used the same. After the
first two steps, remains a single goal:
1. ⋀x y za.
r x y ⟹
star r y za ⟹
(star r za z ⟹ star r y z) ⟹ star r za z ⟹ star r x z
My first “simp” is because “star r za z” appears as a supposedly True
hypothesis, so that “(star r za z ⟹ star r y z)” can be simplified to
“star r y z” and the goal then become:
1. ⋀x y za.
r x y ⟹
star r y za ⟹
star r y z ⟹ star r za z ⟹ star r x z
Then, I noticed “r x y” and “star r y z” and “star r x z”, present in the
hypothesis covers all of “star.step”, so that “star.step” is a more
general case of the goal to prove.
As the simplifier is able to prove something like “(A⟹B⟹Z)⟹(A⟹B⟹C⟹Z)”, I
supposed it should be able to prove the less general goal by the more
general “star.step”.
Looked quite straightforward, but the simplifier trace tells me *five
times*:
simp_trace_depth_limit exceeded!
Amazingly, it was still able to prove the goal by simplification.
My question is: how to make similar simplification more simple? By the
way, should I really see it as an issue?
Thanks for any pointers and feeling on the topic.
Email Gateway (Aug 19 2022 at 08:02):From: Tobias Nipkow <nipkow@in.tum.de>
The message "simp_trace_depth_limit exceeded!" merely tells you that the trace
depth has been exceeded. The behaviour of the simplifier is not affected, merely
its tracing is stopped until it emerges from its recursive invocations. This is
a very simpled-minded way of getting a abstract view of the trace. If you want
more tracing info, you can always increase the limit - in ProofGeneral there is
a menue item Trace Simplifier Depth for it.
We expect to provide better tracing facilities in the future.
Tobias
Email Gateway (Aug 19 2022 at 08:03):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Le Tue, 31 Jul 2012 08:08:31 +0200, Tobias Nipkow
<nipkow@in.tum.de> a écrit:
The message "simp_trace_depth_limit exceeded!" merely tells you that the
trace
depth has been exceeded. The behaviour of the simplifier is not affected,
That's what I guessed too, while was still surprised a limit was exceeded
with what looked simple to me. On the other hand, I understand
simplification is the most important and tedious part of proof assistance
and that it easily requires more steps than what a human believe in his
mind.
merely
its tracing is stopped until it emerges from its recursive invocations.
This is
a very simpled-minded way of getting a abstract view of the trace. If
you want
more tracing info, you can always increase the limit - in ProofGeneral
there is
a menue item Trace Simplifier Depth for it.
I searched for a way to have the same with jEdit. That's the opportunity
of another topic.
We expect to provide better tracing facilities in the future.
Tobias
May be a simple text filter would be enough. But I did not go into these
internals for now.
Thanks for your comments and explanations.
Email Gateway (Aug 19 2022 at 08:27):From: Lars Noschinski <noschinl@in.tum.de>
You can do this by "using [[simp_trace_depth_limit=x]]"
-- Lars
Last updated: Nov 21 2024 at 12:39 UTC