Email Gateway (Aug 18 2022 at 13:53): Email Gateway (Aug 18 2022 at 13:53):From: Dennis Walter <dennis.walter@gmail.com>
Dear all,
I encountered a goal which makes the simplifier hang, where by
"hanging" I mean that it does not give any response in the trace, even
though trace_simp_depth_limit is set to 10 (trace_simp enabled, ofc)
and the last message in the trace is on level 2. I could boil the goal
down to what you can see below, where the simplifier displays the same
behaviour: a partial trace, and no failure or success after one minute
(yes, I'm somewhat impatient :) ) The problem seems to be introduced
in theory Int, since simp'ing with the simpsets of Equiv_Relations,
Nat, or Wellfounded terminates.
Can somebody comment on this?
Thanks,
Dennis
=====
theory Hangs imports Main
begin
definition f :: "int => int"
where "f x = x"
lemma
"f a = M { nat j |j. 0 <= j & j < f b} ==> P"
apply simp
(* even apply (tactic {* asm_full_simp_tac (simpset_of @{theory Int})
1 *}) does not work *)
=====
PS: Isabelle 2009, polyml 5.2.1, Linux
Email Gateway (Aug 18 2022 at 13:53):From: Brian Huffman <brianh@cs.pdx.edu>
On Tue, Aug 4, 2009 at 8:36 AM, Dennis Walter<dennis.walter@gmail.com> wrote:
Dear all,
I encountered a goal which makes the simplifier hang,
I managed to simplify the example a bit more; the definition of
constant "f" has nothing to do with the problem, although the types
are important.
lemma "(a::int) = M {x::nat. EX j. x = nat j}"
apply simp (* hangs *)
lemma "(a::int) = M {z. P (nat z)}"
apply simp (* also hangs *)
The problem seems to be introduced
in theory Int, since simp'ing with the simpsets of Equiv_Relations,
Nat, or Wellfounded terminates.
The constant "nat" seems to be important here; the simplifier doesn't
hang if I replace it with another constant of the same type.
Interestingly, the same behavior is produced if I replace "a::int"
with "a::nat", "a::rat" or "a::real"; but the simplifier doesn't hang
for "a::complex", or other types like "a::int list". Only ordered
numeric types seem to cause a problem. (I also found that the
simplifier still hangs if you replace the top-level "=" with "<" or
"<=".)
My best guess is that one of the default simprocs is causing the
simplifier to hang. Looking at "Show me ... simplifier rules" in Proof
General, I don't see any simprocs that mention constant "nat"
explicitly. I suppose it must be a simproc like fast_int_arith that
matches the equality at type int. Internally, the simproc must be
doing some processing of each side that causes it to loop.
Unfortunately, it seems that the simprocs don't produce any trace
output unless they succeed, which isn't much help here. Maybe someone
else can figure out the rest of what's going on here.
Email Gateway (Aug 18 2022 at 13:55):From: Tjark Weber <webertj@in.tum.de>
Dennis,
the problem was caused by a bug in the solver for linear arithmetic,
which deals with certain expressions (e.g., "nat j") by case splitting.
If those expressions contained bound variables, the solver would (in
some cases) erroneously loop.
I have committed a fix to the Isabelle repository. Please let me know
if the problem persists.
Regards,
Tjark
Email Gateway (Aug 18 2022 at 13:55):From: Makarius <makarius@sketis.net>
Tjark's change is available here
http://isabelle.in.tum.de/repos/isabelle/rev/04af689ce721
It looks like you could apply this easily to the official Isabelle2009
sources, so you need not experiment with "unofficial undefined" repository
snapshots in your production work.
Makarius
Last updated: Apr 25 2024 at 16:19 UTC