Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Problem during goal simplification

Email Gateway (Aug 22 2022 at 13:11):

From: Omar Montaño Rivas <omar.montano@upslp.edu.mx>
Hi,

Does anyone know why the following goal loops after simplification (simp)?
Is there a way to avoid non-termination, e.g. by eliminating a rewrite rule
or a congruence rule from the simpset? I have tried changing the value of
linarith_split_limit but with no success.

Thanks,
Omar.

declare [[linarith_split_limit = 0]]

lemma "∃f g. ∀(x::nat) y. f x y = (if 0 = y then if y = 0 then f 0 y else
if 0 - 1 - 1 = y then y else y else y) ∧
g x y =
(if y - 1 - 1 =
(if y - 1 - 1 =
(if 0 = y - 1 then y - 1 else (if y = (if y - 1 = y

• 1 then y - 1 else y - 1) - 1 - 1 - 1 then y else y) - 1) - 1 - 1 - 1
  then if y = (if y = y - 1 - 1 then y - 1 else y) - 1 -
  1 - 1 then y else y else y - 1) -
  1 -
  1
  then x else y)"
  using [[simp_trace]] apply simp

Email Gateway (Aug 22 2022 at 13:11):

From: Omar Montano Rivas <omarmrivas@gmail.com>
Hi,

Does anyone know why the following goal loops after simplification (simp)?
Is there a way to avoid non-termination, e.g. by eliminating a rewrite rule
or a congruence rule from the simpset? I have tried changing the value of
linarith_split_limit but with no success.

Thanks,
Omar.

declare [[linarith_split_limit = 0]]

lemma "∃f g. ∀(x::nat) y. f x y = (if 0 = y then if y = 0 then f 0 y else
if 0 - 1 - 1 = y then y else y else y) ∧
g x y =
(if y - 1 - 1 =
(if y - 1 - 1 =
(if 0 = y - 1 then y - 1 else (if y = (if y - 1 = y

• 1 then y - 1 else y - 1) - 1 - 1 - 1 then y else y) - 1) - 1 - 1 - 1
  then if y = (if y = y - 1 - 1 then y - 1 else y) - 1 -
  1 - 1 then y else y else y - 1) -
  1 -
  1
  then x else y)"
  using [[simp_trace]] apply simp

Email Gateway (Aug 22 2022 at 13:11):

From: Tobias Nipkow <nipkow@in.tum.de>
Frankly, it is hard to say. Maybe the if-splits created some premises that
constitute a nonterminating set of equations? That's heuristic proof automation
for you.

The following proof script simplifies the goal completely. Although the
resulting goal is unenlightening (for me), the script may be of use:

apply(split if_split)
apply(split if_split)
apply (simp split del: if_split)
apply(split if_split)
apply (simp split del: if_split)
apply(split if_split)
apply (simp split del: if_split)

Here is another gadget for tweaking the simplifier:

using [[simp_depth_limit = 3]] apply simp

This does the job. A second call to simp (which is not influenced by that
"using") fails, showing that the result is fully simplified.

Tobias
smime.p7s

Email Gateway (Aug 22 2022 at 13:11):

From: Omar Montaño Rivas <omar.montano@upslp.edu.mx>
Thanks!

Good to know how to control if splits during simplification.

Omar.

Last updated: Apr 26 2024 at 04:17 UTC