Email Gateway (Aug 19 2022 at 11:00): Email Gateway (Aug 19 2022 at 11:00):From: Makarius <makarius@sketis.net>
On Wed, 22 May 2013, Christoph LANGE wrote:
I should have said that I'm using the Isabelle2013 release version.
You shouldn't. On isabelle-users you always refer implicitly to the
latest release without saying that explicitly. Only if you use an older
(official) release you should say that.
In contrast, if you are testing Isabelle repository versions, you should
discuss your observations on the isabelle-dev mailing list (including the
all-important Mercurial changeset id), not on isabelle-users.
Is it right that as soon as I switch to Isabelle2014 or to the
development version I will be able to remove this code?
Isabelle release cycles vary between 6-10 months, but the year has
invariably 12 months. So the next one is likely to be Isabelle2013-1
before the end of 2013, not Isabelle2014.
When working profesionally and productively with Isabelle you normally use
the latest official release. Only if you have a special situation, and
some extra time to follow the ongoing development process quickly, you may
consider testing repository versions instead (see above).
Note that repository snapshots between the releases become outdated more
quickly than the stable stepping stones. It is particularly bad to "get
stuck" on some old snapshot while the official releases have moved on 1 or
2 steps already.
Makarius
Email Gateway (Aug 19 2022 at 11:11):From: Christoph LANGE <math.semantic.web@gmail.com>
Dear Isabelle community,
I am currently working with lists constructed from finite sets, and I'm
missing the following two lemmas that would really help me to get my
work done. At the moment my Isabelle experience is not sufficient for
proving them myself, plus I think it would make sense if they were part
of the library (List.thy).
lemma sorted_list_of_set_not_empty [simp] :
assumes "finite S" and "S ≠ {}"
shows "sorted_list_of_set S ≠ []"
sorry
lemma sorted_list_of_set_distinct [simp] :
shows "distinct (sorted_list_of_set S)"
sorry
Would any of the developers feel up to proving them, or alternatively
teaching me how to do it?
BTW, for my work I actually don't need these lists-from-sets to be
_sorted_. However sorted_list_of_set is the only result that
find_consts "'a set ⇒ 'a list"
gives me. Efficient computation is not yet that crucial for my work,
but would it be possible to provide a list-from-set constructor that
does not guarantee sorting? I mean something that simply rearranges the
internal data structure of a finite set (which is not guaranteed to be
sorted either) into a list.
Finally, lists-from-sets are probably not even what I need to get my
actual work done. I.e. if you think that there is no good reason for me
using them, I'm willing to abandon them. Originally I'm working with
finite sets, but I defined a custom Max-like operation on them, which
recursively folds the comparison of two elements over the whole
set/list. As I'm not yet capable of understanding the internals behind
definition (in linorder) Max :: "'a set ⇒ 'a" where
"Max = fold1 max"
in Big_Operators.thy (which seem to depend on certain idempotence laws
that max satisfies), but wanted to prove some properties of my Max-like
operation and got stuck in my initial attempt to use finite_ne_induct, I
resorted to converting my finite sets to lists and using
list_nonempty_induct – which did the job, except for the two missing
lemmas mentioned above.
Cheers, and thanks in advance for your help,
Christoph
Email Gateway (Aug 19 2022 at 11:11):From: Brian Huffman <huffman.brian.c@gmail.com>
On Wed, May 22, 2013 at 10:16 AM, Christoph LANGE
<math.semantic.web@gmail.com> wrote:
Dear Isabelle community,
I am currently working with lists constructed from finite sets, and I'm
missing the following two lemmas that would really help me to get my
work done. At the moment my Isabelle experience is not sufficient for
proving them myself, plus I think it would make sense if they were part
of the library (List.thy).lemma sorted_list_of_set_not_empty [simp] :
assumes "finite S" and "S ≠ {}"
shows "sorted_list_of_set S ≠ []"
using assms by (metis sorted_list_of_set set.simps(1))
A different formulation might make a more useful simp rule:
lemma sorted_list_of_set_empty_iff:
assumes "finite S"
shows "sorted_list_of_set S = [] ⟷ S = {}"
lemma sorted_list_of_set_distinct [simp] :
shows "distinct (sorted_list_of_set S)"
apply (cases "finite S")
apply (induct set: finite)
apply (simp_all add: distinct_insort)
done
Email Gateway (Aug 19 2022 at 11:11):From: Lars Noschinski <noschinl@in.tum.de>
On 22.05.2013 19:16, Christoph LANGE wrote:
I am currently working with lists constructed from finite sets, and I'm
missing the following two lemmas that would really help me to get my
work done. At the moment my Isabelle experience is not sufficient for
proving them myself, plus I think it would make sense if they were part
of the library (List.thy).
I first wondered why you had problems with these proofs; then I
discovered that Florians rework of Big_Operators in the development
version added some crucial lemmas ;)
lemma sorted_list_of_set_not_empty [simp] :
assumes "finite S" and "S ≠ {}"
shows "sorted_list_of_set S ≠ []"
Sledeghammer is able to find a proof after unfolding
sorted_list_of_set_def. A nicer proof however is to prove the following
first:
lemma sorted_list_of_set_remove':
assumes "finite A" "x ∈ A"
shows
"sorted_list_of_set A = insort x (sorted_list_of_set (A - {x}))"
proof -
from assms have "insert x (A - {x}) = A" by blast
then have "sorted_list_of_set A = sorted_list_of_set (insert x (A -
{x}))"
by simp
also have "... = insort x (sorted_list_of_set (A - {x}))"
using assms by simp
finally show ?thesis .
qed
then your proof goes through with
using assms by (auto simp: sorted_list_of_set_remove')
BTW, a nicer lemma would be:
lemma sorted_list_of_set_eq_Nil_iff:
assumes "finite S"
shows "sorted_list_of_set S = [] <-> S = []"
using assms by (auto simp: sorted_list_of_set_remove')
lemma sorted_list_of_set_distinct [simp] :
shows "distinct (sorted_list_of_set S)"
sorry
This property does not hold in Isabelle 2013, as Finite_Set.fold is only
defined for finite sets (i.e., we cannot prove anything about infinite
sets). So you need to district your lemma to finite sets. Then the proof
is easy:
lemma sorted_list_of_set_distinct [simp] :
assumes "finite S" shows "distinct (sorted_list_of_set S)"
using assms sorted_list_of_set by auto
(In the next version of Isabelle, Finite_Set.fold will probably return
the initial argument for infinite sets).
Finally, lists-from-sets are probably not even what I need to get my
actual work done. I.e. if you think that there is no good reason for me
using them, I'm willing to abandon them. Originally I'm working with
finite sets, but I defined a custom Max-like operation on them, which
recursively folds the comparison of two elements over the whole
set/list. As I'm not yet capable of understanding the internals behinddefinition (in linorder) Max :: "'a set ⇒ 'a" where
"Max = fold1 max"in Big_Operators.thy (which seem to depend on certain idempotence laws
that max satisfies), but wanted to prove some properties of my Max-like
operation and got stuck in my initial attempt to use finite_ne_induct, I
resorted to converting my finite sets to lists and using
list_nonempty_induct – which did the job, except for the two missing
lemmas mentioned above.
As sets have no order, fold is only well-defined if the operation you
define is commutative.
-- Lars
Email Gateway (Aug 19 2022 at 11:11):From: Lars Noschinski <noschinl@in.tum.de>
Only in the development version.
Email Gateway (Aug 19 2022 at 11:11):From: Christoph LANGE <math.semantic.web@gmail.com>
Hi Lars, hi Brian,
thanks for your quick help; let me answer all remaining points at once.
2013-05-22 19:30 Lars Noschinski:
I first wondered why you had problems with these proofs; then I
discovered that Florians rework of Big_Operators in the development
version added some crucial lemmas ;)
Oh, I see. Sorry, I should have said that I'm using the Isabelle2013
release version.
lemma sorted_list_of_set_not_empty [simp] :
assumes "finite S" and "S ≠ {}"
shows "sorted_list_of_set S ≠ []"Sledeghammer is able to find a proof after unfolding
sorted_list_of_set_def.
That's indeed a good lesson for me as a, still, relative newbie. So far
I had been doing this "unfolding some_def sledgehammer" step with
definitions of my own, whereas I had never thought of doing it with
definitions from the library.
A nicer proof however is …
then your proof goes through with …
BTW, a nicer lemma would be:lemma sorted_list_of_set_eq_Nil_iff:
assumes "finite S"
shows "sorted_list_of_set S = [] <-> S = []"
using assms by (auto simp: sorted_list_of_set_remove')
Thanks (to Brian, too)!
For now I copied these into my formalisation. Is it right that as soon
as I switch to Isabelle2014 or to the development version I will be able
to remove this code?
lemma sorted_list_of_set_distinct [simp] :
shows "distinct (sorted_list_of_set S)"
sorryThis property does not hold in Isabelle 2013, as Finite_Set.fold is only
defined for finite sets (i.e., we cannot prove anything about infinite
sets). So you need to district your lemma to finite sets. Then the proof
is easy:lemma sorted_list_of_set_distinct [simp] :
assumes "finite S" shows "distinct (sorted_list_of_set S)"
using assms sorted_list_of_set by auto(In the next version of Isabelle, Finite_Set.fold will probably return
the initial argument for infinite sets).
Thanks, and thanks for pointing out that I had forgotten to assume
"finite S".
Finally, lists-from-sets are probably not even what I need to get my
actual work done. I.e. if you think that there is no good reason for me
using them, I'm willing to abandon them. Originally I'm working with
finite sets, but I defined a custom Max-like operation on them, which
recursively folds the comparison of two elements over the whole
set/list. As I'm not yet capable of understanding the internals behinddefinition (in linorder) Max :: "'a set ⇒ 'a" where
"Max = fold1 max"in Big_Operators.thy (which seem to depend on certain idempotence laws
that max satisfies), but wanted to prove some properties of my Max-like
operation and got stuck in my initial attempt to use finite_ne_induct, I
resorted to converting my finite sets to lists and using
list_nonempty_induct – which did the job, except for the two missing
lemmas mentioned above.As sets have no order, fold is only well-defined if the operation you
define is commutative.
Indeed. Still I have no idea whether it will be _easy_ to use
finite_ne_induct in my case. Folding is actually not applicable to my
Max-like function, which is actually rather a variant of "arg max" in
that it returns the index of the maximum component of a vector, where
the index is an element of those finite "nat set"s that I'm using. –
Anyway, just some thoughts. Your solutions work fine for me, and allow
me to focus on my actual problem (proving that a certain auction
formalisation determines a unique winner – soon to become public at
http://www.cs.bham.ac.uk/research/projects/formare/code/auction-theory/).
Cheers,
Christoph
Email Gateway (Aug 19 2022 at 11:12):From: Tobias Nipkow <nipkow@in.tum.de>
Most of the time, converting from sets to lists is a cloogy workaround because
of problems defining some function directly on fnite sets. I recommend to
understand and use the appropriate fold combinator on lists instead.
tobias
Email Gateway (Aug 19 2022 at 11:12):From: Christoph LANGE <math.semantic.web@gmail.com>
2013-05-22 22:43 Tobias Nipkow:
Most of the time, converting from sets to lists is a cloogy workaround because
of problems defining some function directly on fnite sets.
Good point – that's what I tried first, but I couldn't figure out how to
make it work.
I recommend to
understand and use the appropriate fold combinator on lists instead.
You mean "on sets", right?
Here is what I tried unsuccessfully. I posted in on stackoverflow, as
it's a proper question.
Cheers,
Christoph
Email Gateway (Aug 19 2022 at 11:12):From: Tobias Nipkow <nipkow@in.tum.de>
Am 23/05/2013 01:14, schrieb Christoph LANGE:
2013-05-22 22:43 Tobias Nipkow:
Most of the time, converting from sets to lists is a cloogy workaround because
of problems defining some function directly on fnite sets.Good point – that's what I tried first, but I couldn't figure out how to
make it work.I recommend to
understand and use the appropriate fold combinator on lists instead.You mean "on sets", right?
yes
Here is what I tried unsuccessfully. I posted in on stackoverflow, as
it's a proper question.
if you are not desparate for executability, here is a two stage approach: first
get all the indices where the function has its maximum (which you can get via
Max), then select some element from it via SOME. although SOME can be a bit
tricky to reason about, this is a fairly abstract approach. something like
let M = {x. v x = Max(v ` finite domain of v)}
in SOME x. x : M & some tie breaker
where the tie breaker could be something like ALL y : M. t x y
tobias
Cheers,
Christoph
Last updated: Nov 21 2024 at 12:39 UTC