Email Gateway (Aug 22 2022 at 17:30): Email Gateway (Aug 22 2022 at 17:30):From: Bertram Felgenhauer via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Hi,
I'm wondering how to best convert between the typeclass and the locale
versions of operations. For example, the ordered tree property for
red-black trees can be written as rbt_sorted or ord.rbt_sorted (op <),
and the two can be shown to be equivalent:
theory Test
imports "HOL-Library.RBT_Impl"
begin
lemma rbt_sorted_conv:
"ord.rbt_sorted (op <) = rbt_sorted"
by (auto simp: rbt_sorted_def ord.rbt_sorted_def rbt_less_prop
ord.rbt_less_prop rbt_greater_prop ord.rbt_greater_prop)
end
However, the way I'm proving this is horrible -- basically I'm unfolding
the definitions down to the elementary class operations, which does not
scale very well. Is there a better way to obtain such conversions?
Cheers,
Bertram
Email Gateway (Aug 22 2022 at 17:30):From: Bertram Felgenhauer via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
I wrote:
"ord.rbt_sorted (op <) = rbt_sorted"
On a related note, I was confused that rbt_sorted has a linorder
constraint while being defined in an ord context. This is a
consequence of the setup around
http://isabelle.in.tum.de/repos/isabelle/file/f5ca4c2157a5/src/HOL/Library/RBT_Impl.thy#l2055
Is that really necessary?
Cheers,
Bertram
Email Gateway (Aug 22 2022 at 17:30):From: Andreas Lochbihler <mail@andreas-lochbihler.de>
Dear Bertram,
The change in the sort constraint goes back to a small renovation I did a few years ago.
Originally, all the rbt_* functions were defined in the locales for the classes order and
linorder. I then moved them to the syntactic class ord such that the code generator can
generate code for the locale-based version without further ado. For backwards
compatibility, I re-installed the former sort constraints.
The problem of relaxing the sort constraints is that the rbt_* operations do not really
make sense with more general types, because they use if conditions of the form
if x < y then X else if y < x then Y else Z
If they were changed to
if x <= y then if y <= x then Z else X else Y
then they would also make sense, e.g., if the order is not antisymmetric. Changing this
would mean to change the proofs, too. Moreover, since red-black trees are mainly used for
code generation, it would be nice to change them to use a comparator, which is independent
of the logical order. René Thiemann has done some work in that direction in the AFP, but
this has not yet been propagated into the Isabelle standard library.
So, in short: No, it does not have to be this way. It is a historic relic and nobody was
sufficiently annoyed by it to put up the effort and change it.
Andreas
Email Gateway (Aug 22 2022 at 18:06):From: Bertram Felgenhauer via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
I wrote:
To answer my own question, one can exploit the automatic translation
between the locale and the typeclass with a tiny bit of obfuscation,
instead of exhaustively unfolding the definitions. For the example this
looks as follows:
theory Test
imports "HOL-Library.RBT_Impl"
begin
lemma (in ord) rbt_sorted_conv_aux:
"id ord.rbt_sorted (<) = rbt_sorted"
by simp
lemmas rbt_sorted_conv = rbt_sorted_conv_aux[unfolded id_def]
end
The downside is that this approach pollutes the locale's namespace with
useless auxiliary facts.
I still wish such identities would be accessible in a more direct way,
am I missing a way of doing that?
Cheers,
Bertram
Last updated: Nov 21 2024 at 12:39 UTC