Stream: Beginner Questions

Topic: Why is `list_update_beyond` marked simp?

Hanno Becker (Sep 10 2023 at 06:20):

Hi. The following takes a long time on my machine:

lemma test:
  assumes ‹length x = 42›
  shows ‹x [0 := 0,  1  := 0, 2  := 0, 3  := 0, 4  := 0,
            5 := 0,  6  := 0, 7  := 0, 8  := 0, 9  := 0,
            10 := 0, 11 := 0, 12 := 0, 13 := 0, 14 := 0,
            15 := 0, 16 := 0, 17 := 0, 18 := 0, 19 := 0] = y›
  using assms apply simp

The reason is that

list_update_beyond: length ?xs ≤ ?i ⟹ ?xs[?i := ?x] = ?xs

is marked as a simp rule by default, which leads to an explosion of simplification paths explored by the simplifier for iterated list updates -- as witnessed in the example above.

Of course, one can remove list_update_beyond from the simpset, but why is it in it to begin with? As the lemma itself says, updating a list beyond its length isn't very useful, so I think it should not be considered by default.

Kevin Kappelmann (Sep 11 2023 at 13:19):

This is probably something you have to post on the mailing list to receive an answer.

Hanno Becker (Sep 13 2023 at 07:17):

Okay

Last updated: Apr 27 2024 at 12:25 UTC