[isabelle] Surprising `simp` behaviour for image-sets · Mirror: Isabelle Users Mailing List

Stream: Mirror: Isabelle Users Mailing List

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

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

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

Email Gateway (Feb 19 2025 at 10:30):

From: hannobecker <hannobecker@posteo.de>
Tobias, all,The above seems to persist in Isabelle2025-RC2 -- any chance it can be fixed before the release?Best,Hanno
-------- Original message --------From: Tobias Nipkow <nipkow@in.tum.de> Date: 06/05/2024 08:49 (GMT+00:00) To: cl-isabelle-users@lists.cam.ac.uk Subject: Re: [isabelle] Surprising simp behaviour for image-sets Hanno,Thanks for the notification. I will look into this, but not before the release.TobiasOn 02/05/2024 20:42, hannobecker@posteo.de wrote:> 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 (Feb 19 2025 at 10:42):

From: Makarius <makarius@sketis.net>
On 19/02/2025 11:21, hannobecker wrote:

The above seems to persist in Isabelle2025-RC2 -- any chance it can be fixed
before the release?

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

Since that is not a regression wrt. Isabelle2023 and Isabelle2024, it is now
too late for Isabelle2025.

Makarius

Email Gateway (Feb 19 2025 at 15:02):

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

I had forgotten about this but took a look now. However, I could not really
figure out precisely what is going on. The problem is obviously the schamtic
variable - the "let" is innocent. This goal already shows the effect:

sschematic_goal ‹P((λr :: unit. ?foo r) ` UNIV)›

I would need to study the code in more detail to figure out where and why "?foo
()" becomes ?g7 ...

Tobias

On 19/02/2025 11:21, hannobecker wrote:

Tobias, all,

The above seems to persist in Isabelle2025-RC2 -- any chance it can be fixed
before the release?

Best,
Hanno

-------- Original message --------
From: Tobias Nipkow <nipkow@in.tum.de>
Date: 06/05/2024 08:49 (GMT+00:00)
To: cl-isabelle-users@lists.cam.ac.uk
Subject: Re: [isabelle] Surprising simp behaviour for image-sets

Hanno,

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

Tobias

On 02/05/2024 20:42, hannobecker@posteo.de wrote:

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

smime.p7s

Email Gateway (Feb 19 2025 at 16:27):

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

On 19/02/2025 16:27, Norbert Schirmer wrote:

Hi,

The simproc unit_eq seems to be responsible:

Yes, unit and (thus that simproc) triggers it, as Hanno already pointed out, but
I don't understand why it is responsible for that replacement of "?foo ()" by
this new ?g7 that breaks things. But maybe I am barking up the wrong tree.

Tobias

schematic_goal
‹(⋂(r :: unit). let bar = ?foo r in bar) = ⋂ (range ?foo)›
supply [[simproc del: unit_eq]]
apply simp
done

Regards,
Norbert

--

Norbert Schirmer (nschirmer@apple.com)
 SEG Formal Verification

On 19. Feb 2025, at 16:02, Tobias Nipkow <nipkow@in.tum.de> wrote:

Hanno,

I had forgotten about this but took a look now. However, I could not really
figure out precisely what is going on. The problem is obviously the schamtic
variable - the "let" is innocent. This goal already shows the effect:

sschematic_goal ‹P((λr :: unit. ?foo r) ` UNIV)›

I would need to study the code in more detail to figure out where and why "?
foo ()" becomes ?g7 ...

Tobias

On 19/02/2025 11:21, hannobecker wrote:

Tobias, all,
The above seems to persist in Isabelle2025-RC2 -- any chance it can be fixed
before the release?
Best,
Hanno
-------- Original message --------
From: Tobias Nipkow <nipkow@in.tum.de>
Date: 06/05/2024 08:49 (GMT+00:00)
To: cl-isabelle-users@lists.cam.ac.uk
Subject: Re: [isabelle] Surprising simp behaviour for image-sets
Hanno,
Thanks for the notification. I will look into this, but not before the release.
Tobias
On 02/05/2024 20:42, hannobecker@posteo.de wrote:

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

smime.p7s

Email Gateway (Feb 19 2025 at 16:28):

From: Norbert Schirmer <cl-isabelle-users@lists.cam.ac.uk>
Hi,

The simproc unit_eq seems to be responsible:

schematic_goal
‹(⋂(r :: unit). let bar = ?foo r in bar) = ⋂ (range ?foo)›
supply [[simproc del: unit_eq]]
apply simp
done

Regards,
Norbert

Norbert Schirmer (nschirmer@apple.com)
 SEG Formal Verification

On 19. Feb 2025, at 16:02, Tobias Nipkow <nipkow@in.tum.de> wrote:

Hanno,

I had forgotten about this but took a look now. However, I could not really figure out precisely what is going on. The problem is obviously the schamtic variable - the "let" is innocent. This goal already shows the effect:

sschematic_goal ‹P((λr :: unit. ?foo r) ` UNIV)›

I would need to study the code in more detail to figure out where and why "?foo ()" becomes ?g7 ...

Tobias

On 19/02/2025 11:21, hannobecker wrote:

Tobias, all,
The above seems to persist in Isabelle2025-RC2 -- any chance it can be fixed before the release?
Best,
Hanno
-------- Original message --------
From: Tobias Nipkow <nipkow@in.tum.de>
Date: 06/05/2024 08:49 (GMT+00:00)
To: cl-isabelle-users@lists.cam.ac.uk
Subject: Re: [isabelle] Surprising simp behaviour for image-sets
Hanno,
Thanks for the notification. I will look into this, but not before the release.
Tobias
On 02/05/2024 20:42, hannobecker@posteo.de wrote:

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 (Feb 20 2025 at 12:22):

From: Norbert Schirmer <cl-isabelle-users@lists.cam.ac.uk>

On 19. Feb 2025, at 17:27, Tobias Nipkow <nipkow@in.tum.de> wrote:

Yes, unit and (thus that simproc) triggers it, as Hanno already pointed out, but I don't understand why it is responsible for that replacement of "?foo ()" by this new ?g7 that breaks things. But maybe I am barking up the wrong tree.

I took a closer look and the reason is the combination of solving the preconditions of a congruence rule and the simproc unit_eq:

schematic_goal ‹P((λr :: unit. ?foo r) ` UNIV)›
supply [[simp_trace, simp_trace_depth_limit=10]]
apply simp

[1]Applying congruence rule:
UNIV ≡ ?N1 ⟹
(⋀x. x ∈ ?N1 =simp=> ?foo x ≡ ?g1 x) ⟹ range ?foo ≡ ?g1 ` ?N1

When the simplifier is invoked on the precondition of the congruence rule:

(1) (⋀x. x ∈ ?N1 =simp=> ?foo x ≡ ?g1 x)

the simproc unit_eq rewrites x to ()

so it ultimately comes up with this equation for the precondition:

(⋀x. True =simp=> ?foo () ≡ ?g1 ()) ≡ (True =simp=> ?foo () ≡ ?g1 ())

Now the RHS of that meta equality is unified with (1) which seems to
introduce instantiations ?foo: (λr. ?g7) and ?g1: (λa. ?g7)

Regards,
Norbert

Norbert Schirmer (nschirmer@apple.com)
 SEG Formal Verification

Tobias

schematic_goal
‹(⋂(r :: unit). let bar = ?foo r in bar) = ⋂ (range ?foo)›
supply [[simproc del: unit_eq]]
apply simp
done
Regards,
Norbert
--
Norbert Schirmer (nschirmer@apple.com)
 SEG Formal Verification

On 19. Feb 2025, at 16:02, Tobias Nipkow <nipkow@in.tum.de> wrote:

Hanno,

I had forgotten about this but took a look now. However, I could not really figure out precisely what is going on. The problem is obviously the schamtic variable - the "let" is innocent. This goal already shows the effect:

sschematic_goal ‹P((λr :: unit. ?foo r) ` UNIV)›

I would need to study the code in more detail to figure out where and why "? foo ()" becomes ?g7 ...

Tobias

On 19/02/2025 11:21, hannobecker wrote:

Tobias, all,
The above seems to persist in Isabelle2025-RC2 -- any chance it can be fixed before the release?
Best,
Hanno
-------- Original message --------
From: Tobias Nipkow <nipkow@in.tum.de>
Date: 06/05/2024 08:49 (GMT+00:00)
To: cl-isabelle-users@lists.cam.ac.uk
Subject: Re: [isabelle] Surprising simp behaviour for image-sets
Hanno,
Thanks for the notification. I will look into this, but not before the release.
Tobias
On 02/05/2024 20:42, hannobecker@posteo.de wrote:

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

Last updated: Mar 09 2025 at 12:28 UTC