# IRC log for #isabelle, 2017-06-08

All times shown according to UTC.

Time Nick Message
01:48 ilbot3 joined #isabelle
01:48 Topic for #isabelle is now Official channel for the Isabelle/HOL theorem prover: http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html || Now with logging: http://irclog.perlgeek.de/isabelle/
01:55 dmiles joined #isabelle
02:34 keep_learning joined #isabelle
13:45 w_ joined #isabelle
13:45 w_ hey
13:45 w_ anyone here?
13:45 w_ I'm having trouble proving a really simple lemma
13:45 w_ " ∀j<i. P j ⟹ P i ⟹  ∀j≤i. P j "
13:45 w_ can't figure out how to prove it
13:46 w_ try0 says no proof found...
13:47 w_ oh nvm
13:47 w_ try worked
13:50 silver joined #isabelle
14:00 JCaesar :)
17:35 chindy Anyone know if there are any theories specifically for correspondences/set valued functions ?
17:37 int-e I don't know. I'd consider treating such a thing as a relation.
17:46 int-e since they're isomorphic: http://downthetypehole.de/paste/BFOV9mIA
18:51 w_ does anyone know how to get min to return a nat?
18:51 w_ I've got  r = (int min {(j::nat) . A!j = m})
18:51 w_ but it fails
18:51 w_ Type unification failed: Clash of types "_ ⇒ _" and "nat"
18:51 w_ Type error in application: incompatible operand type
18:51 w_ Operator:  int :: nat ⇒ int
18:51 w_ Operand:   min :: ??'a ⇒ ??'a ⇒ ??'a
18:52 w_ in this case isabelle should know that min should return a nat, right?
18:52 w_ since I specified (j::nat)
18:57 ammbauer w_: min is for taking the minimum of two values. you want to use "Min"
18:58 w_ aha got it
18:58 w_ thank you very much
19:28 Merv_ joined #isabelle
19:33 chindy w_: also as a side node i blieve the argument of Min must be countable or foldable
20:14 larsrh we need an isabelle-bot
20:15 larsrh ! type "Min" or something
21:10 chindy +1
21:28 Merv joined #isabelle
22:04 int-e joined #isabelle
22:36 pruvisto larsrh: cool, maybe you should bring up that idea with the developer of libisabelle
22:37 pruvisto also, chindy, no it doesn't
22:37 pruvisto it just needs a linorder
22:37 pruvisto but for infinite sets, "Min" is essentially undefined
22:38 pruvisto for infinite sets, one can use "Inf", which requires some more structure on the type (semilattice probably)
22:45 chindy pruvisto: thats what i mean... i just remember wondering why max wouldnt work on an inifite set...
22:53 pruvisto Because there may not exist a maximum in an infinite set
22:54 pruvisto well, a minimum
22:55 pruvisto I guess one could have defined "Min" such that it always returns a minimum whenever there exists one
22:55 pruvisto but I think in those cases you would normally rather use "Inf" anyway