IRC log for #isabelle, 2017-07-17

All times shown according to UTC.

Time Nick Message
07:28 Merv_ joined #isabelle
10:40 chindy left #isabelle
10:40 chindy joined #isabelle
10:40 chindy pruvisto: one might also add a argmin :/
10:41 pruvisto Huh? There is an arg_min.
10:43 chindy where ?
10:44 chindy wait... was that a surpise because you were wondering if that construct existet at all or wree you saying that argmin is in Isabelle
10:47 pruvisto No, there is one.
10:47 pruvisto In the development version
10:47 pruvisto in Lattices_Big
10:47 pruvisto right above arg_max
10:47 chindy ahh.. yea sry... forgot that i found argmax in the dev version... :(
11:33 silver joined #isabelle
13:03 pruvisto chindy: btw I just talked to Tobias and he said to use "{x. is_arg_min f P x}" for "Arg_min f P"
13:03 pruvisto you can make your own definition if you really need that
13:04 chindy and i guess with argmax respectively...
13:04 chindy hmm okay thanks
13:05 pruvisto He said that he considered doing a set-based thing at first, but found that the predicate-based one seemed more elegant in the end
13:13 chindy so something like this http://downthetypehole.de/paste/4O0WcRXz
13:14 pruvisto seems right, yes
13:18 chindy pruvisto: interestingly enough it seems nontrivial to prove that argmax f S is a subset of S.
13:18 pruvisto Well, that only holds if S is non-empty and a maximum actually exists
13:19 pruvisto actually
13:19 pruvisto no wait
13:19 pruvisto you mean your arg_max_set?
13:19 pruvisto that should be easy
13:19 pruvisto "arg_max f S" is only an element of S if S is non-empty and if a maximum actually exists (i.e. f is bounded on S)
13:20 pruvisto but arg_max_set should always be a subset of S
13:20 int-e . o O ( bounded? (0,1) is bounded... )
13:20 pruvisto lemma "arg_max_set f S ⊆ S" by (auto simp: arg_max_set_def is_arg_max_def)
13:21 pruvisto int-e: well, bounded by an element in f ` S
13:22 pruvisto My intuition tells me that in chindy's case, the set under consideration is always finite
13:22 pruvisto And non-empty. In which case "arg_max_set f S" will be non-empty.
13:22 int-e lemma "is_arg_max f S (arg_max f S) ==> arg_max f s : arg_max_set f S" looks a bit silly too.
13:22 chindy i am basically wondering about this http://downthetypehole.de/paste/bR3RSs3Q
13:22 int-e (sketching, there are conversions between predicates and sets missing in that)
13:23 chindy but in general for what i need argmax the sets are mostly real vectors so... uncountable (i guess)
13:23 pruvisto oh?
13:23 pruvisto okay in that case things get a bit more tricky, I guess
13:23 int-e Maybe "arg_max_set f S ~= {} <--> is_arg_max f S (arg_max f S)" is borderline interesting.
13:23 pruvisto then you probably need that S is compact and f is continuous
13:23 pruvisto or something like that
13:24 pruvisto int-e: I think that the problem is that in order to use arg_min/arg_max, you will always have to argue why such a thing should exist in the first place
13:25 int-e yes, that's kind of inescapable :)
13:25 pruvisto and that reasoning cannot be done in a general way
13:25 pruvisto you always have to make some argument specific to your use case
13:25 pruvisto one can, of course, try to provide some helpful lemmas for common cases
13:25 pruvisto like a finite domain
13:26 pruvisto or indeed a continuous f and a compact S
13:26 pruvisto that should work, unless my topology is completely failing me now
13:27 chindy pruvisto: but if i have a set of reals that is closed then it should have a meast element, right?
13:27 pruvisto only if it's compact
13:27 pruvisto the set of all real numbers is closed, but clearly does not have a least element
13:28 pruvisto or rather, what you need is closed and bounded from below
13:28 pruvisto i.e. closed and bdd_below in Isabelle
13:29 chindy yea... bounded from below for a bin and bounded from above for a max?
13:29 chindy min*
13:29 chindy but yea... i will have to have a look into that thanks!
13:29 pruvisto sounds right
13:30 pruvisto "sets of real vectors" sounds dangerously like linear algebra
13:30 pruvisto which I fear is not in a great state in Isabelle at the moment
13:30 pruvisto but people are working on it
13:31 pruvisto but, just to caution you: people aren't quite sure how to properly do linear algebra in Isabelle yet and a lot of things are still missing
13:35 pruvisto But I don't want to scare you off. Might well be that what you're trying to do is perfectly doable.
20:02 keep_learning joined #isabelle