Email Gateway (Aug 18 2022 at 18:10): Email Gateway (Aug 18 2022 at 18:10):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Peter, hi Brian,
In his zest to ensure all uses of numerals are algebraically
well-organised, Brian manufactured the attached theory of "saturated"
arithmetic for the naturals for me.I'm now struggling to get it to work with the code generator. The
problem is that the CARD('a) construct leans on the card function, and
for some reason the code generator wants to enumerate nat while
calculating card. I can't see why it wants to do that. Can you suggest a
way forward? (The attached theory should break at an opportune point.)
find attached an experiment of mine which hopefully turn out to be helpful.
First, it is important that we keep such discussions on the public
mailing list, since more eyes see more than less and also to make sure
the generic Isabelle knowledge stays publicly available and is able to grow.
Here now, the answers proper to your issues:
a) avoiding CARD('a) in generated code
class len_card = len +
assumes len_of_card: "len_of TYPE('a) = CARD('a)"
This connects len_of TYPE('a) to CARD('a) and allows you to generate
code for type 'a::len_card sat. Of course you have to give appropriate
instantiations, or replace CARD('a) by len_of TYPE('a) in your
specification throughout to gain full flexibility. @Brian: Did you ever
think about including such a class as len_card into the Word libraries
directly?
b) use abstract type for code generation
lemma Abs_Rep_sat' [simp, code abstype]:
"Abs_sat' (Rep_sat n) = n"
by (simp add: Abs_sat'_def min_CARD_Rep_sat Rep_sat_inverse)
(call on me again if this sounds like Bohemian villages for you)
c) prove simp rules for your "abtract" operation of the form:
lemma Rep_plus_sat [simp]:
"Rep_sat (x + y) = min (Rep_sat x + Rep_sat y) CARD('a)"
by (simp add: plus_sat_def)
Together with extensionality on sat values, this will greatly simplify
your proofs and make them less cumbersome. Look at the theory to get
more ideas.
I humbly suggest that a working version of this theory make its way
into HOL/Library. I'd be happy to round out the theory with some guidance.
Yes, indeed. I'd first suggest to round up the proofs a little, and
maybe others want to comment also on that.
Hope this helps,
Florian
Saturated.thy
signature.asc
Email Gateway (Aug 18 2022 at 18:10):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Btw. theory src/HOL/Library/Dlist.thy is a very nice example how to
establish what you could call »abstract types with invariants« and
corresponding code generation in Isabelle/HOL.
I suggest to follow the patterns which can be found there wrt.
to which auxiliary lemmas about Rep/Abs/Abs' to prove, which simp rules
to prove
and how to setup code generation.
Maybe your Abs_sat' can just be called Sat.
Florian
signature.asc
Email Gateway (Aug 18 2022 at 18:11):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Maybe your Abs_sat' can just be called Sat.
When going through Dlist a further suggestion came to my mind:
I have modified the theory further: Abs_sat' is called Sat, and Rep_sat
nat_of. Both are operations to be expected to be used in »user space«
and should therefore carry readable names.
Hope this helps,
Florian
Saturated.thy
signature.asc
Email Gateway (Aug 18 2022 at 18:12):From: Peter Gammie <peteg42@gmail.com>
Florian,
Thanks for this. I've tidied it up a bit. See the attached.
cheers
peter
Saturated.thy
Email Gateway (Aug 18 2022 at 18:13):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Peter,
Thanks for this. I've tidied it up a bit. See the attached.
Thanks a lot.
One further remark: the lemmas nat_mult_min_left etc. are quite generic.
These should go into a separate prelude section at the beginning of the
theory, from where, after becoming part of the library, they should be
move to appropriate theories in the HOL distribution.
What also comes to my mind is that saturated numbers seem to be a nice
example for complete lattices (with inf = min etc.). Maybe you still
want to add those instances.
Cheers,
Florian
signature.asc
Email Gateway (Aug 18 2022 at 18:20):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Peter,
the theory is in regression:
http://isabelle.in.tum.de/testboard/Isabelle/rev/fe33d6655186
I did this - see the attached. Thanks very much to sledgehammer for doing the most boring bits!
Well, the first one(s) did not really perform well, but it was not very
difficult to get along without it.
I'm not speaking against sledgehammer, but when you prove fundamental
things it is often better to try with less erratic methods like simp,
auto etc – this will both increase your understanding of the matter as
well as give hints which fundamental rules are still missing. In
application with more rather technical lemmas, sledgehammer is very fine.
After the next Isabelle release you might want to add also
instantiation sat :: (len) complete_lattice
but AFAIS this will require more lemmas about fold.
Thanks a lot for your contribution.
Florian
signature.asc
Email Gateway (Aug 18 2022 at 18:20):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Still one further remark:
I guess with lemmas like
"nat_of (min x y) = min (nat_of x) (nat_of y)"
"nat_of (max x y) = max (nat_of x) (nat_of y)"
"nat_of (Inf A) = Min_fin (insert 0 (nat_of A))"
"nat_of (Sup A) = Sup_fin (insert (len_of TYPE('a)) (nat_of A))"
life in the instances proofs can even be easier.
Florian
signature.asc
Email Gateway (Aug 18 2022 at 18:20):From: Peter Gammie <peteg42@gmail.com>
Florian,
On 08/09/2011, at 8:00 AM, Florian Haftmann wrote:
the theory is in regression:
http://isabelle.in.tum.de/testboard/Isabelle/rev/fe33d6655186
Great, thanks.
I did this - see the attached. Thanks very much to sledgehammer for doing the most boring bits!
Well, the first one(s) did not really perform well, but it was not very
difficult to get along without it.
What do you mean by "the first one(s)"? Lemmas, sledgehammers, ... ?
I'm not speaking against sledgehammer, but when you prove fundamental
things it is often better to try with less erratic methods like simp,
auto etc – this will both increase your understanding of the matter as
well as give hints which fundamental rules are still missing. In
application with more rather technical lemmas, sledgehammer is very fine.
I found sledgehammer very useful for discovering the lemmas needed for the proofs. I agree that the final proofs could be presented better.
After the next Isabelle release you might want to add also
instantiation sat :: (len) complete_lattice
but AFAIS this will require more lemmas about fold.
You've lost me here - the final instantiation in the theory is precisely this one.
Thanks a lot for your contribution.
Thanks to you and Brian for developing the theory!
cheers
peter
Email Gateway (Aug 18 2022 at 18:20):From: Tobias Nipkow <nipkow@in.tum.de>
Am 08/09/2011 00:12, schrieb Peter Gammie:
I did this - see the attached. Thanks very much to sledgehammer for doing the most boring bits!
Well, the first one(s) did not really perform well, but it was not very
difficult to get along without it.What do you mean by "the first one(s)"? Lemmas, sledgehammers, ... ?
I'm not speaking against sledgehammer, but when you prove fundamental
things it is often better to try with less erratic methods like simp,
auto etc – this will both increase your understanding of the matter as
well as give hints which fundamental rules are still missing. In
application with more rather technical lemmas, sledgehammer is very fine.I found sledgehammer very useful for discovering the lemmas needed for the proofs. I agree that the final proofs could be presented better.
I agree with both Florian and Peter: s/h is great for discovering useful
lemmas, and it can be beneficial both for performance and legibility to
transform the generated metis proofs into auto. (But one can easily
waste time on unsuccessful attempts to do so.)
Tobias
After the next Isabelle release you might want to add also
instantiation sat :: (len) complete_lattice
but AFAIS this will require more lemmas about fold.
You've lost me here - the final instantiation in the theory is precisely this one.
Thanks a lot for your contribution.
Thanks to you and Brian for developing the theory!
cheers
peter
Email Gateway (Aug 18 2022 at 18:20):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Peter,
Well, the first one(s) did not really perform well, but it was not very
difficult to get along without it.What do you mean by "the first one(s)"? Lemmas, sledgehammers, ... ?
Well, the first metis class was very slow, I did not check the others
explicitly.
instantiation sat :: (len) complete_lattice
You've lost me here - the final instantiation in the theory is precisely this one.
This was a slip, it should read
instantiation sat :: (len) complete_distrib_lattice
which is still left as an exercise to prove.
Cheers,
Florian
signature.asc
Email Gateway (Aug 18 2022 at 18:21):From: Lukas Bulwahn <bulwahn@in.tum.de>
It seems as if this saturated naturals library is still causing some
trouble with the code generator. I am looking into this and will
probably solve it within the next hours.
Lukas
Email Gateway (Aug 18 2022 at 18:21):From: Lukas Bulwahn <bulwahn@in.tum.de>
The issue was related to my misunderstanding of the code generator
handling abstract (code) types.
After some enlightment, code generation for saturated naturals in
Haskell does not pose a problem any longer.
Lukas
Email Gateway (Aug 18 2022 at 18:21):From: Brian Huffman <brianh@cs.pdx.edu>
I haven't added this instance proof yet, but I did add another one:
Type 'a sat is now an instance of the number_semiring class. Proving
this instance involved showing that the function "Sat :: nat => 'a
sat" is identical to the polymorphic function "of_nat" at the same
type.
This brings up another issue: It is generally undesirable to have two
different copies of the same function around if they are both in
common use, since this means that we would have to maintain two
similar-looking but separate sets of simp rules. This was the
motivation for making "int :: nat => int" into an abbreviation for
"of_nat :: nat => int" a few years ago; it let us remove a lot of
duplication and simpset inconsistencies from the standard library.
So here's what I propose for the saturated arithmetic library: Rename
the current constant "Sat :: nat => 'a sat" to something like
Abs_sat', and reintroduce the user-friendly name "Sat" as a
type-constrained abbreviation for "of_nat".
The only reason I'm hesitant to make this change myself is that I
don't know how it might affect code generation -- currently "Sat" has
some special status because it appears in the [code abstype]
declaration.
Email Gateway (Aug 18 2022 at 18:21):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Brian,
And according to the type discipline of the code generator it must
remain so. But we need the "old" Sat anyway for bootstrap reasons. So
I would suggest:
I remember a similar issue concerning of_nat can be found in
Code_Numeral, which also contains such duplication due to bootstrap reasons.
Florian
signature.asc
Email Gateway (Aug 18 2022 at 18:26):From: Peter Gammie <peteg42@gmail.com>
Florian,
On 18/08/2011, at 4:29 PM, Florian Haftmann wrote:
One further remark: the lemmas nat_mult_min_left etc. are quite generic.
These should go into a separate prelude section at the beginning of the
theory, from where, after becoming part of the library, they should be
move to appropriate theories in the HOL distribution.
OK.
What also comes to my mind is that saturated numbers seem to be a nice
example for complete lattices (with inf = min etc.). Maybe you still
want to add those instances.
I did this - see the attached. Thanks very much to sledgehammer for doing the most boring bits!
cheers
peter
Saturated.thy
Last updated: Apr 26 2024 at 08:19 UTC