Email Gateway (Aug 22 2022 at 16:47): Email Gateway (Aug 22 2022 at 16:47):From: Lawrence Paulson <lp15@cam.ac.uk>
I've noticed that Isabelle/HOL has no syntax for the minimum/maximum of a finite set. Or rather, while one can write Max {a i| i. i ∈ I}, such a set comprehension can translate into a complicated formula involving existential quantifiers, with the reasoning similarly complicated. Or one could instead use the image operator and write Max (a ` I).
In fact (a ` I) = {a i| i. i ∈ I}, and a more general form of this result exists as the lemma setcompr_eq_image.
Arguably what's needed here isn't special syntax for Min/Max but rather an alternative syntax for image, e.g. {a i. i ∈ I}. Are there any views?
Larry Paulson
Email Gateway (Aug 22 2022 at 16:47):From: Peter Lammich <lammich@in.tum.de>
On Fr, 2018-02-16 at 16:14 +0000, Lawrence Paulson wrote:
I've noticed that Isabelle/HOL has no syntax for the minimum/maximum
of a finite set. Or rather, while one can write Max {a i| i. i ∈ I},
such a set comprehension can translate into a complicated formula
involving existential quantifiers, with the reasoning similarly
complicated. Or one could instead use the image operator and write
Max (a ` I).In fact (a ` I) = {a i| i. i ∈ I}, and a more general form of this
result exists as the lemma setcompr_eq_image.Arguably what's needed here isn't special syntax for Min/Max but
rather an alternative syntax for image, e.g. {a i. i ∈ I}. Are there
any views?
Why not use the existing Syntax for INF/SUP ?
term "SUP x:X. f x"
i.e. one could declare syntax:
MAX i:I. a i
-- Peter
Larry Paulson
Email Gateway (Aug 22 2022 at 16:48):From: Tobias Nipkow <nipkow@in.tum.de>
I agree with Peter because the SUP syntax ultimately stands for "a ` I", which
is what you want (because it avoids the quantifier). It is a very natural syntax
and avoids inventing a new syntax for image.
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 16:48):From: Joachim Breitner <joachim@cis.upenn.edu>
Hi,
I have, in the past, missed a concise quantifier-free syntax for set
image, and would have wanted (expected, even?) something like
{a i. i ∈ I}
Cheers,
Joachim
signature.asc
Email Gateway (Aug 22 2022 at 16:48):From: Julian <parsert.julian@gmail.com>
Hi,
do you mean the same as {a i |i. i ∈ I}?
Julian
Email Gateway (Aug 22 2022 at 16:48):From: Lawrence Paulson <lp15@cam.ac.uk>
This is logically equivalent to the image operator, but denotes something like {x. ∃i∈I. x = a i}, while “image” is a single constant.
The advantage of introducing something like {a i. i ∈ I} is that we would have a uniform syntax for all future situations. E.g. the current (⋃x∈A. B x) could also be written ⋃{B x. x∈A}.
Larry
Email Gateway (Aug 22 2022 at 16:49):From: Andreas Lochbihler <mail@andreas-lochbihler.de>
The map operation on multisets, image_mset, already uses the proposed syntax:
{# a i. i :# M #} = image_mset (%i. a i) M
So extending this syntax to ordinary sets would be just more uniform syntax. But how does
it interoperate with ordinary set comprehension? How do we want to distinguish the
following two cases:
{ i. i : M } = Collect (%i. i : M)
vs.
{ i. i : M } = image (%i. i) M
Andreas
Email Gateway (Aug 22 2022 at 16:49):From: Dominique Unruh <unruh@ut.ee>
I wonder why there is an existential quantifier in the translation of the
set comprehension in the first place.
If {a i | i. M} would translate to "image a (Collect M)", the awkward
existential quantifier would be gone (I suppose that the simplifier can
deal much more easily with "image a" than with the existential quantifier.)
For example, {a i |i. i ∈ I} would translate to "image a (Collect (%x.
x:I))" which the simplifier can easily rewrite to "image a I".
Of course, I also understand that changing this might introduce too many
breaking changes in proofs.
Best wishes,
Dominique.
Email Gateway (Aug 22 2022 at 16:49):From: Tobias Nipkow <nipkow@in.tum.de>
Using a standard set-comprehension syntax for image is plain misleading and will
create more confusion (even if we manage to resolve the ambiguity that Andreas
pointed out).
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 16:49):From: Lawrence Paulson <lp15@cam.ac.uk>
Well, a strong argument against any fancy syntax for image is that it would be input-only. Image is just an ordinary infix operator and the user would see something like a`i instead of {a i. i ∈ I}.
Users (especially beginners) should be aware that a general comprehension could give rise to a large formula. I frequently write expressions using nested unions instead. I don't know whether it really simplifies reasoning steps, but I find it clearer.
Larry
signature.asc
Email Gateway (Aug 22 2022 at 16:50):From: Tobias Nipkow <nipkow@in.tum.de>
I can never make up my mind.
Code generation needs Unions, but that is orthogonal.
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 16:50):From: Johannes Hölzl <johannes.hoelzl@gmx.de>
Another option is to intruduce the applicative <*>
(<*>) :: ('a => 'b) set => 'a set => 'b set
F <*> A = { f a | f a. f : F & a : A}
This allows some nice point-free style:
{(+)} <> A <> B (or (+) ` A <*> B)
But still gives nice rules, especially for finiteness, countability:
finite A ==> finite F ==> finite (F <*> A)
And it should work well with code generation.
A counter point is that it is a very CS style notation and uncommon in
mathematics.
Email Gateway (Aug 22 2022 at 17:03):From: Lawrence Paulson <lp15@cam.ac.uk>
I am returning to this old question, and thinking of doing as you suggest. But why does the HOL development (at the end of theory Main) hide part of this syntax?
no_syntax
"_INF1" :: "pttrns ⇒ 'b ⇒ 'b" ("(3⨅_./ _)" [0, 10] 10)
"_INF" :: "pttrn ⇒ 'a set ⇒ 'b ⇒ 'b" ("(3⨅_∈_./ _)" [0, 0, 10] 10)
"_SUP1" :: "pttrns ⇒ 'b ⇒ 'b" ("(3⨆_./ _)" [0, 10] 10)
"_SUP" :: "pttrn ⇒ 'a set ⇒ 'b ⇒ 'b" ("(3⨆_∈_./ _)" [0, 0, 10] 10)
Larry
Email Gateway (Aug 22 2022 at 17:03):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Dear Larry,
the lattice syntax is not a default part of HOL-Main, hence it is
manually reverted here and can included on demand importing theory
Library/Lattice_Syntax.thy.
The reason is that there has always been some reluctance to fix that
syntax with its extremely diverse applications to one particular set of
operations.
I one thought to use syntax in bundles to make this more convenient, nut
there are obstacles:
Lattice operations are introduced incrementally, but bundles are not
extensible; maybe that could be lifted by defining all syntactic
operations first, then defining the syntax bundle and then deriving the
lemmas.
There is no way yet to include bundled syntax in text of global theory
level commands like "class".
Hope this helps,
Florian
signature.asc
Last updated: Apr 27 2024 at 01:05 UTC