Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] natural number arithmetic normalisation


view this post on Zulip Email Gateway (Aug 18 2022 at 18:44):

From: Michael Norrish <Michael.Norrish@nicta.com.au>
The following term arose inside a side-condition that the simplifier was attempting to discharge:

(2::nat) ^ (2 * (2 * (2 * (2 * (2 * 1)))))

The simp tactic being used included field_simps as a rewrite.

The result was an apparent "hang" as Isabelle attempted to calculate 2 ^ 32 in unary arithmetic.

You can see the behaviour by doing

lemma "(2::nat) ^ (2 * (2 * (2 * (2 * (2 * 1))))) = X"
apply (simp add: field_simps)

It seems to me that this is yet more evidence that using 1 = Suc 0 as a rewrite is a bad idea.

That aside, it would be nice if the simp technology could allow the use of an innocuous rewrite (field_simps), one that doesn't even mention Suc, alongside perfectly reasonable terms such as the one above.

Michael
signature.asc

view this post on Zulip Email Gateway (Aug 18 2022 at 18:44):

From: Brian Huffman <brianh@cs.pdx.edu>
On Mon, Nov 14, 2011 at 12:34 AM, Michael Norrish
<Michael.Norrish@nicta.com.au> wrote:

The following term arose inside a side-condition that the simplifier was attempting to discharge:

(2::nat) ^ (2 * (2 * (2 * (2 * (2 * 1)))))

The simp tactic being used included field_simps as a rewrite.

The result was an apparent "hang" as Isabelle attempted to calculate 2 ^ 32 in unary arithmetic.

You can see the behaviour by doing

lemma "(2::nat) ^ (2 * (2 * (2 * (2 * (2 * 1))))) = X"
apply (simp add: field_simps)

This is a very interesting puzzle, especially since, as you say,
field_simps doesn't even mention Suc!

After looking at the simp trace to see which rules were involved I
realized that you can get the same blowup using "simp only" with a
small set of rules, none of which are in field_simps, and all of which
are in the default simpset:

lemma "(2::nat) ^ (2 * (2 * (2 * (2 * (2 * 1))))) = X"
apply (simp only: One_nat_def mult_Suc_right mult_0_right add_2_eq_Suc)

Yet simply writing "apply simp" on the same goal reduces everything to
just a numeral.

The weirdness involves these rewrite rules:

lemma add_2_eq_Suc [simp]: "2 + n = Suc (Suc n)"
lemma add_2_eq_Suc' [simp]: "n + 2 = Suc (Suc n)"

These rules originate quite a while ago:
http://isabelle.in.tum.de/repos/isabelle/rev/9d6514fcd584

Now, what happens if we simplify a term like "2 + 0" or "0 + 2", where
more than one possible simp rule can apply? It turns out that the
simplifier will rewrite "2 + 0" to "2" (using the additive zero law),
but in the other order, "0 + 2" rewrites to "Suc (Suc 0)" (using rule
add_2_eq_Suc'). So the presence of the add_commute rule really makes a
difference here:

lemma "(2::nat) ^ (2 * (2 * (2 * (2 * (2 * 1))))) = X"
apply (simp add: add_commute) (* blows up with Suc *)

It seems to me that this is yet more evidence that using 1 = Suc 0 as a rewrite is a bad idea.

I agree. I think that a good guideline for the Isabelle simpset should
be that no simp rule should ever insert a Suc into a subgoal that
didn't already contain one.

We have discussed removing "1 = Suc 0" as a simp rule on the dev
mailing list before:
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2009-February/000484.html

My conclusion back then was that the only reason we have "1 = Suc 0"
[simp] is historical, since "1" used to be a mere abbreviation for
"Suc 0". It would be nice to finally get rid of it (along with
add_2_eq_Suc and friends).

view this post on Zulip Email Gateway (Aug 18 2022 at 18:44):

From: Tobias Nipkow <nipkow@in.tum.de>
It would certainly be nice to get rid of these rewrites, but the task is
daunting.

Tobias


Last updated: Mar 28 2024 at 16:17 UTC