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 setbased thing at first, but found that the predicatebased 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 nonempty 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 nonempty 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 
inte 
. 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 
inte: 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 nonempty. In which case "arg_max_set f S" will be nonempty. 
13:22 
inte 
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 
inte 
(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 
inte 
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 
inte: 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 
inte 
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 