Email Gateway (Aug 18 2022 at 14:49): Email Gateway (Aug 18 2022 at 14:49):From: Peter Gammie <peteg42@gmail.com>
Hello,
I am curious to know what the code generator can do with finite sets.
For proof re-use reasons I use this idiom to fudge them into lists (in a definition context):
xs_list = (SOME xs. set xs = { my finite set })
The only substantial reason I have is that I can make use of the equivalence relation partition operator '_ // _' on these sets.
Is there a way (does someone have some code) to partition lists? Is there a more-complete treatment of finite sets for the code generator somewhere?
cheers
peter
Email Gateway (Aug 18 2022 at 14:50):From: Peter Lammich <peter.lammich@uni-muenster.de>
Peter Gammie wrote:
Hello,
I am curious to know what the code generator can do with finite sets.
For proof re-use reasons I use this idiom to fudge them into lists (in a definition context):
xs_list = (SOME xs. set xs = { my finite set })
The only substantial reason I have is that I can make use of the equivalence relation partition operator '_ // _' on these sets.
When using SOME, you run into a fundamental problem: SOME makes a choice
that the
executable code cannot follow (as you can't tell anything about the
choice made).
One workaround is to parameterize over the SOME-operator, i.e. work
under the assumption that you have an operator that
behaves like SOME, but having the possibility to replace it by a
concrete one later.
However, I'm think this will not work without some manual refinement
steps from sets to lists (?)
Best,
Peter
Is there a way (does someone have some code) to partition lists? Is there a more-complete treatment of finite sets for the code generator somewhere?
cheers
peter
Email Gateway (Aug 18 2022 at 14:50):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Peter,
For proof re-use reasons I use this idiom to fudge them into lists (in =
a definition context):
=20
xs_list =3D (SOME xs. set xs =3D { my finite set })
=20
The only substantial reason I have is that I can make use of the equiva=
lence relation partition operator '_ // _' on these sets.
If this is indeed the only reason, you should perhaps define an
alternative equivalence relation partition operator on lists and then
proof some lemmas which allow you to transfer theorems from the set to
the list representation (at least to some extent).
Sorry for being that vague, but we are still exploring how a systematic
transfer principle for such situations should look like.
Hope this helps,
Florian
--=20
Home:
http://www.in.tum.de/~haftmann
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_in=
formatik_tu_muenchen_de
signature.asc
Email Gateway (Aug 18 2022 at 14:51):From: Peter Gammie <peteg42@gmail.com>
Daniel:
Thanks for this! I am embarrassed that I didn't consult the AFP before sending that email
(Co)Incidentally this will at least solve another problem I was facing, viz dealing with functions over finite subsets of some arbitrary type, which may or may not coincide on the rest of the type... a problem I didn't expect to be so neatly treated as it is here.
Rene: thanks for your kind offer. I will see how Andreas's FinFuns work out.
cheers
peter
Last updated: Apr 19 2024 at 16:20 UTC