Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Surprising `simp` behaviour for image-sets

Email Gateway (May 02 2024 at 18:49):

From: hannobecker@posteo.de
Hi,

I observe the following unexpected behaviour of the simplifier (both in
Isabelle2023 and in Isabelle2024-RC2):

The following goal solves by simp:

schematic_goal
   ‹(⋂(r :: 'a). let bar = ?foo r in bar) = ⋂ (range ?foo)›
   by simp

However, when specializing 'a to unit, it does no longer. The simp
trace indicates that the issue may be related to the unit parameter
being elided from the schematic variable.

schematic_goal
   ‹(⋂(r :: unit). let bar = ?foo r in bar) = ⋂ (range ?foo)›
   apply simp (* No luck *)
   using [[simp_trace]]
   apply simp
   (* [1]Proved wrong theorem (bad subgoaler?)
        range (λr. let bar = ?g7 in bar) ≡ range (λa. ?g7)
      Should have proved:
        range (λr. let bar = ?foo r in bar)
      [1]Congruence proof failed.  Should not have proved
        range (λr. let bar = ?g7 in bar) ≡ range (λa. ?g7)
      [1]Applying congruence rule:
        UNIV ≡ ?N1 ⟹ (⋀x. x ∈ ?N1 =simp=> ?foo x ≡ ?g1 x) ⟹ range ?foo ≡
?g1 ` ?N1 *)
   apply (simp cong del: image_cong)
   done

The above is a minimal example derived from a real-world instance
arising in our large-scale application of Isabelle. As indicated, the
problem disappears when removing the image_cong congruence rule, but
that may cause us surprises elsewhere, so I would prefer an alternative
solution if possible.

As always, thanks for help,
Hanno

Email Gateway (May 06 2024 at 07:49):

From: Tobias Nipkow <nipkow@in.tum.de>
Hanno,

Thanks for the notification. I will look into this, but not before the release.

Tobias

smime.p7s

Last updated: May 19 2024 at 04:18 UTC