Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Proposal: An update to Multiset theory

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

From: Bertram Felgenhauer via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Dear Isabelle users and maintainers,

I have been working with the multiset extension from the HOL library
recently. In the course of doing so, I proved that the multiset
extension is cancellative w.r.t. the multiset union, to wit:

lemma mult_cancel:
assumes "trans s" "irrefl s"
shows "(X + Z, Y + Z) ∈ mult s ⟷ (X, Y) ∈ mult s" (is "?L ⟷ ?R")

I believe that this lemma is generally useful and would be a good
candidate for inclusion in the Isabelle HOL library. However, it
overlaps with the decreasing_parts_disj lemma from the recent addition
of an executable version of the multiset extension (f2177f5d2aed).
I propose to eliminate the latter lemma in favor of mult_cancel.

See the attached theory for details. To summarize, I propose to

• remove lemma decreasing_parts_disj,

• add lemmas:
  mult_cancel: ... (X + Z, Y + Z) ∈ mult s ⟷ (X, Y) ∈ mult s
  mult_cancel_max: ... (X, Y) ∈ mult s ⟷ (X - X #∩ Y, Y - X #∩ Y) ∈ mult s
  multp_iff: ... multp P N M ⟷ (N, M) ∈ mult R
  (and corresponding definition of multp)

• reprove the existing lemma
  multeqp_iff: multeqp P N M ⟷ (N, M) ∈ (mult R)⇧=

• optionally add trivial lemmas:
  mono_mult1: assumes "s ⊆ s'" shows "mult1 s ⊆ mult1 s'"
  mono_mult: assumes "s ⊆ s'" shows "mult s ⊆ mult s'"

The reason for adding the multp version of multeqp is that multp_iff is
(to me) a natural intermediate result on the way towards the proof of
the existing lemma multeqp_iff.

The mult_cancel_max lemma is used in the proof of multp_iff.

What do you think? Also, are there any users of the
decreasing_parts_disj lemma?

Cheers,

Bertram

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

From: Bertram Felgenhauer via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
(Once more with an attachment)

Dear Isabelle users and maintainers,

I have been working with the multiset extension from the HOL library
recently. In the course of doing so, I proved that the multiset
extension is cancellative w.r.t. the multiset union, to wit:

lemma mult_cancel:
assumes "trans s" "irrefl s"
shows "(X + Z, Y + Z) ∈ mult s ⟷ (X, Y) ∈ mult s" (is "?L ⟷ ?R")

I believe that this lemma is generally useful and would be a good
candidate for inclusion in the Isabelle HOL library. However, it
overlaps with the decreasing_parts_disj lemma from the recent addition
of an executable version of the multiset extension (f2177f5d2aed).
I propose to eliminate the latter lemma in favor of mult_cancel.

See the attached theory for details. To summarize, I propose to

• remove lemma decreasing_parts_disj,

• add lemmas:
  mult_cancel: ... (X + Z, Y + Z) ∈ mult s ⟷ (X, Y) ∈ mult s
  mult_cancel_max: ... (X, Y) ∈ mult s ⟷ (X - X #∩ Y, Y - X #∩ Y) ∈ mult s
  multp_iff: ... multp P N M ⟷ (N, M) ∈ mult R
  (and corresponding definition of multp)

• reprove the existing lemma
  multeqp_iff: multeqp P N M ⟷ (N, M) ∈ (mult R)⇧=

• optionally add trivial lemmas:
  mono_mult1: assumes "s ⊆ s'" shows "mult1 s ⊆ mult1 s'"
  mono_mult: assumes "s ⊆ s'" shows "mult s ⊆ mult s'"

The reason for adding the multp version of multeqp is that multp_iff is
(to me) a natural intermediate result on the way towards the proof of
the existing lemma multeqp_iff.

The mult_cancel_max lemma is used in the proof of multp_iff.

What do you think? Also, are there any users of the
decreasing_parts_disj lemma?

Cheers,

Bertram
Multiset_new.thy

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

From: Bertram Felgenhauer via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Bertram Felgenhauer via Cl-isabelle-users wrote:

(Once more with an attachment)

And once more. This version works with the current development version
of Isabelle (3a0f40a6fa42). Sorry for the spam!

Cheers,

Bertram
Multiset_new.thy

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

From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Dear Bertram,

I see. I cannot find any use of "multeqp" in the repositories I mentioned in my previous email, except for some occurrences in IsaFoR. But "multeqp" can be implemented more efficiently than "multp" (and these predicates appear to be designed for code generation).

If nobody speaks up against or for one or the other predicate, I suggest you proceed with your intended change.

Cheers,

Jasmin

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

From: Christian Sternagel <c.sternagel@gmail.com>
Right, code generation was my only reason to investigate this in the
first place (since we had situations where CeTA timed out while trying
to compare "tiny" -- around 10 elements -- multisets), so that's the
only reason why I went with multeqp instead of multp.

cheers

chris

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

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi all,

I have no objection towards Bertram's proposed extension.

There is, however, one point which I don't understand:

But "multeqp" can be implemented more efficiently than "multp" (and these predicates appear to be designed for code generation).

Comparing the two definitions

definition multeqp :: "('a ⇒ 'a ⇒ bool) ⇒ 'a multiset ⇒ 'a multiset ⇒ bool" where
"multeqp P N M =
(let Z = M #∩ N; X = M - Z; Y = N - Z in
(∀y ∈ set_mset Y. ∃x ∈ set_mset X. P y x))"

definition multp :: "('a ⇒ 'a ⇒ bool) ⇒ 'a multiset ⇒ 'a multiset ⇒ bool" where
"multp P N M =
(let Z = M #∩ N; X = M - Z; Y = N - Z in
X ≠ {#} ∧ (∀y ∈ set_mset Y. ∃x ∈ set_mset X. P y x))"

it is difficult to see why this should actually be the case. The only
difference is the emptiness check for the local X, which should be
efficient to execute. Maybe the emptiness check has to be carried out
more earlier

lemma [code]:
"multp P N M ⟷ (let Z = M #∩ N; X = M - Z
in X ≠ {#} ∧ (let Y = N - Z in (∀y∈#Y. Multiset.Bex X (P y))))"
by (simp add: multp_def)

for an efficient execution.

Cheers,
Florian
signature.asc

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

From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Hi Florian,

Indeed. You can forget my comment. I misparsed the emptiness check as the disequality check "M ~= N" in the Huet-Oppen formulation of the multiset extension (cf. less_multiset\<^sub>H\<^sub>O in Multiset_Order.thy).

Jasmin

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

From: Bertram Felgenhauer via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Florian Haftmann wrote:

I have no objection towards Bertram's proposed extension.

Nice!

How shall we proceed? As I hinted at earlier I do not have (nor want, at
this point) push access, but I can prepare a patch or clone of the repo,
if that helps, or just provide a plain theory file that works with the
development version of Isabelle.

lemma [code]:
"multp P N M ⟷ (let Z = M #∩ N; X = M - Z
in X ≠ {#} ∧ (let Y = N - Z in (∀y∈#Y. Multiset.Bex X (P y))))"
by (simp add: multp_def)

for an efficient execution.

That's an easy change to make; in fact we can simply adjust the
definition of multp itself accordingly, without losing any proofs.

Does this affect the verdict on having both multp and multeqp?

Cheers,

Bertram

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

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Bertram,

How shall we proceed? As I hinted at earlier I do not have (nor want, at
this point) push access, but I can prepare a patch or clone of the repo,
if that helps, or just provide a plain theory file that works with the
development version of Isabelle.

a repo URL or a patch is indeed the best thing to proceed: there is not
»the« development version but an ongoing agile development.

lemma [code]:
"multp P N M ⟷ (let Z = M #∩ N; X = M - Z
in X ≠ {#} ∧ (let Y = N - Z in (∀y∈#Y. Multiset.Bex X (P y))))"
by (simp add: multp_def)

for an efficient execution.

That's an easy change to make; in fact we can simply adjust the
definition of multp itself accordingly, without losing any proofs.

OK.

Does this affect the verdict on having both multp and multeqp?

Both make sense: reflexive and strict order often occur as pairs in
theory Isabelle developments.

Cheers,
Florian
signature.asc

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

From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Dear Bertram,

I have been working with the multiset extension from the HOL library
recently. In the course of doing so, I proved that the multiset
extension is cancellative w.r.t. the multiset union, to wit:

lemma mult_cancel:
assumes "trans s" "irrefl s"
shows "(X + Z, Y + Z) ∈ mult s ⟷ (X, Y) ∈ mult s" (is "?L ⟷ ?R")

I believe that this lemma is generally useful and would be a good
candidate for inclusion in the Isabelle HOL library. However, it
overlaps with the decreasing_parts_disj lemma from the recent addition
of an executable version of the multiset extension (f2177f5d2aed).
I propose to eliminate the latter lemma in favor of mult_cancel.

This sounds reasonable to me.

The reason for adding the multp version of multeqp is that multp_iff is
(to me) a natural intermediate result on the way towards the proof of
the existing lemma multeqp_iff.

I was hoping Florian would comment this part, since it's related to the code setup. I'm not sure it's a gain to add yet another concept, esp. if the motivation is only a minor simplification of an existing proof. Or did I misunderstand your motivation?

What do you think? Also, are there any users of the
decreasing_parts_disj lemma?

Previous queries on the mailing list revealed that few formalizations use multisets much. The main consumers of Multisets would appear to be the Isabelle distribution, the AFP, IsaFoR, and IsaFoL [*]. A quick grep in these repositories reveals nothing. I would be in favor of that simplification.

Cheers,

Jasmin

[*] https://bitbucket.org/jasmin_blanchette/isafol/wiki/Home

Email Gateway (Aug 22 2022 at 14:02):

From: Bertram Felgenhauer via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Dear Jasmin,
I believe multp is the more fundamental of the two predicates; after
all, the rest of the theory is mostly concerned with the strict multiset
extension. But I was reluctant to drop the existing multeqp predicate in
favor of multp.

Maybe Christian Sternagel can comment on this?

Cheers,

Bertram

Last updated: Nov 21 2024 at 12:39 UTC