Kevin Kappelmann (Mar 17 2021 at 17:19): Kevin Kappelmann (Mar 17 2021 at 17:19):Hey IRC people (#isabelle on freenode) and Zulip community (https://isabelle.zulipchat.com)! :)
I tinkered with matterbridge (https://github.com/42wim/matterbridge) and it seems like we could now communicate with each other.
Do you like this idea? Do you have any concerns? Let me know! I would love to see the Isabelle community to get closer together :)
IRC Bot (Mar 17 2021 at 17:20):@pruvisto[m]: The main concern is that we have to maybe rein in the trash talk a bit now. :P
IRC Bot (Mar 17 2021 at 17:20):@pruvisto[m]: In any case, the channel hasn't been terribly active lately, so who knows when you'll get a reply to those question. :)
Kevin Kappelmann (Mar 17 2021 at 17:21):haha, maybe I should put the IRC channel on Zulip on a different stream than "General" so people can choose whether they are interested in the IRC chat? :)
IRC Bot (Mar 17 2021 at 17:35):@int-e: Uh, no more talk about bugs?
IRC Bot (Mar 17 2021 at 17:36):@int-e: Bugs in Isabelle, I mean. ducks
IRC Bot (Mar 17 2021 at 17:37):@pruvisto[m]: I think that's okay. As of yet, Makarius still boycotts Zulip, I think?
IRC Bot (Mar 17 2021 at 17:39):@int-e: it's hard to tell who's lurking behind the isabelle_zulip nick
IRC Bot (Mar 17 2021 at 17:40):@pruvisto[m]: Yeah also Zulip is archived semi-publicly.
Kevin Kappelmann (Mar 17 2021 at 17:41):That's indeed true!
So I think the IRC community should decide if that's a big no-no.
the isabelle_zulip user is just a bot run by me
IRC Bot (Mar 17 2021 at 17:42):@pruvisto[m]: I don't even know who made this channel in the first place.
IRC Bot (Mar 17 2021 at 17:43):@int-e: so hmm logging... that should be noted in the topic then (out of politeness and per Freenode policy... https://freenode.net/policies#public-logging "Ensure that you notify users (by way of channel topic, channel entry message or similar) that the channel is being publicly logged")
IRC Bot (Mar 17 2021 at 17:43):@pruvisto[m]: But it is fairly common for IRC to be logged, and for parts of these logs surfacing on the web somewhere. So it's not like this channel was "off the record" before, strictly speaking.
IRC Bot (Mar 17 2021 at 17:44):@int-e: (even if it requires registration it still is public to my mind)
IRC Bot (Mar 17 2021 at 17:45):@int-e: Oh I'm an op here? I forgot...
IRC Bot (Mar 17 2021 at 17:47):@pruvisto[m]: Yes, absolutely.
IRC Bot (Mar 17 2021 at 17:51):@int-e: isabelle_zulip [Kevin]: Can isabelle_zulip tell us which users are online on the Zulip side? A command for private chat would be perfect, I think. But I have no clue how the thing works, obviously.
IRC Bot (Mar 17 2021 at 17:53):@int-e: Uh. I mean, a command an IRC user could send to isabelle_zulip privately to get the current list of users on the IRC... topic?... on the Zulip server.
IRC Bot (Mar 17 2021 at 17:53):@pruvisto[m]: You mean the people who are currently actively online there or the ones that are subscribed to the IRC stream?
IRC Bot (Mar 17 2021 at 17:54):@int-e: In any case, personally I think we can try this out and see where it goes.
IRC Bot (Mar 17 2021 at 17:54):@pruvisto[m]: (i.e. who see what is going on there?)
IRC Bot (Mar 17 2021 at 17:54):@int-e: the latter I think
IRC Bot (Mar 17 2021 at 17:54):@pruvisto[m]: but of course, if you subscribe to the stream at a later point, you are still able to see everything that was said before
IRC Bot (Mar 17 2021 at 17:54):@int-e: people we might actually talk to if we catch there interest in the moment
IRC Bot (Mar 17 2021 at 17:54):@int-e: *their
IRC Bot (Mar 17 2021 at 17:54):@pruvisto[m]: in any case, Zulip is probably a better venue for any concrete questions
IRC Bot (Mar 17 2021 at 17:54):@pruvisto[m]: because it is threaded and more searchable
IRC Bot (Mar 17 2021 at 17:55):@pruvisto[m]: so if people have concrete questions, it would be better to ask on there
IRC Bot (Mar 17 2021 at 17:55):@int-e: browser windows take up too much space
IRC Bot (Mar 17 2021 at 17:55):@int-e: :P
IRC Bot (Mar 17 2021 at 17:55):@pruvisto[m]: I usually have it as a pinned tab in Firefox
IRC Bot (Mar 17 2021 at 17:56):@pruvisto[m]: (with Tree Style Tabs)
IRC Bot (Mar 17 2021 at 17:56):@int-e: For IRC, I can have a terminal in a corner of the screen (with irssi) and see whether there's activity. The browser lives on a different virtual screen :P
Kevin Kappelmann (Mar 17 2021 at 17:56):Seems like you cannot query for online users as of now. There was an issue about this https://github.com/42wim/matterbridge/issues/361 but it got closed in favour of another issue, which is still open
IRC Bot (Mar 17 2021 at 17:56):@pruvisto[m]: Private messages are probably difficult because there is only one user on the Zulip side (Kevin's bot).
IRC Bot (Mar 17 2021 at 17:57):@pruvisto[m]: The bot could easily forward private messages from IRC users to Zulip users, but the other direction, well, you would have to specify which IRC user it is supposed to go to on the Zulip side
IRC Bot (Mar 17 2021 at 17:57):@pruvisto[m]: So it would probably be a bit awkward to use.
IRC Bot (Mar 17 2021 at 17:58):@pruvisto[m]: actually even from the IRC side it would be awkward
IRC Bot (Mar 17 2021 at 17:58):@pruvisto[m]: the same problem, you'd have to tell the bot which user the message is supposed to go to
IRC Bot (Mar 17 2021 at 17:58):@pruvisto[m]: This is probably difficult to do with the current bridge.
IRC Bot (Mar 17 2021 at 17:58):@int-e: pruvisto[m]: Yeah I realized that "private chat" was ambiguous... messaging Zulip users privately is different from what I asked.
Kevin Kappelmann (Mar 17 2021 at 17:59):Here's the relevant thread about direct messaging containing some thoughts https://github.com/42wim/matterbridge/issues/191
IRC Bot (Mar 17 2021 at 17:59):@pruvisto[m]: Then what did you mean?
IRC Bot (Mar 17 2021 at 18:01):@int-e: I really wanted #361 only (see who's listening on the other side), not all the other things that are included in #191 (communicating directly with users across the bridge).
IRC Bot (Mar 17 2021 at 18:02):@int-e: Anyway it's not a huge deal... as far as I can see right now.
IRC Bot (Mar 17 2021 at 18:05):@int-e: As to this channel, it was founded by Ian Lynagh (possibly with some other Haskell folks?)... I assume back when he was working on formalizing a darcs-like theory of patches.
IRC Bot (Mar 17 2021 at 18:08):@int-e: But I'm not sure... I joined much later.
Kevin Kappelmann (Mar 17 2021 at 19:22):The archive lives here btw: https://isabelle.systems/zulip-archive/
IRC Bot (Mar 18 2021 at 16:10):@int-e: Odd. I thought I had extended that ban.
IRC Bot (Mar 18 2021 at 16:24):@pruvisto[m]: hm?
IRC Bot (Mar 18 2021 at 16:24):@int-e: wrong channel, my bad.
Ricardo Correia (Apr 11 2021 at 15:36):I'm using Isabelle/jedit and it's working fine except that every few minutes, the cursor switches from red to brown and then I can't type anymore, I can only use the arrow keys, tab and backspace (perhaps others as well, not sure).
Ricardo Correia (Apr 11 2021 at 15:37):The only way I know how to go back to normal is to click with the mouse in the text edit area... is there any other known workaround? This is a bit disruptive.
IRC Bot (Apr 11 2021 at 15:41):@int-e: I know this effect from interacting with the find theorems/sledgehammer/etc. panels, but I don't think I've had it happen all by itself. But I'm not actively using Isabelle at the moment; maybe it got worse. And unfortunately clicking is the only way I know to get back to normal.
Ricardo Correia (Apr 11 2021 at 15:44):Oh, I think you're right... it seems this happens when I focus another panel, I'm not entirely sure if it also happens by itself, but anyway... I just created a keyboard shortcut for the "Go to text area" action and it seems to fix the issue for me, i.e. I don't need to use the mouse anymore. Thanks!
IRC Bot (Apr 11 2021 at 15:44):@int-e: I often thought that the experience would be less awful if the cursor keys would not work in that mode.
IRC Bot (Apr 15 2021 at 08:22):@JCaesar: Hm, there was a way to do a computable fold on a set, if isabelle understands that that set is finite, right? Does anybody know how to pull that off from the top of their head?
IRC Bot (Apr 15 2021 at 09:25):@pruvisto[m]: The operation also has to be commutative and associative
IRC Bot (Apr 15 2021 at 09:25):@pruvisto[m]: then you can use Finite_Set.fold
IRC Bot (Apr 15 2021 at 09:51):@pruvisto[m]: Take a look at the comp_fun_commute and comp_fun_idem locales, and how e.g. the sum function does it.
IRC Bot (Apr 15 2021 at 09:52):@pruvisto[m]: (I think Lukas Stevens also recently made a relativised version that works when the operation is only commutative/associative on the set, but not the entire type)
IRC Bot (Apr 15 2021 at 10:26):@JCaesar: ty.
IRC Bot (Apr 17 2021 at 01:38):@aindilis: Is there a user group, mailing list or some such thing for people wanting to get started writing proofs using Isabelle, where remedial questions might be asked and answered?
IRC Bot (Apr 17 2021 at 10:06):@pruvisto[m]: You should try the zulip
IRC Bot (Apr 17 2021 at 10:07):@pruvisto[m]: isabelle.zulipchat.com
IRC Bot (Apr 17 2021 at 12:12):@JCaesar: pruvisto: I tried Finite_Set.fold and others a bit, remembered the pain from a previous attempt, and ended up just doing everything with lists. (There was one slightly difficult set x = set y ==> ?P x = ?P y proof I had to do, but overall, it's just easier...)
IRC Bot (Apr 18 2021 at 17:00):@aindilis: pruvisto[m]: ty!
IRC Bot (Apr 25 2021 at 15:58):@NieDzejkob: will the new EU regulations apply to proof assistants? (: https://statmodeling.stat.columbia.edu/2021/04/22/eu-proposing-to-regulate-the-use-of-bayesian-estimation/
Manuel Eberl (Apr 25 2021 at 18:25):Hm, somehow I can't post anything on this channel anymore through Matrix. >_>
Manuel Eberl (Apr 25 2021 at 18:25):I was going to reply to what you said with "You have got to be joking"
Manuel Eberl (Apr 25 2021 at 18:25):Hm, the messages also don't show up in my Matrix. Maybe the bridge is broken?
IRC Bot (Apr 26 2021 at 07:59):@pruvisto[m]: Ah, I think I got it working again. :)
IRC Bot (Apr 26 2021 at 08:00):@pruvisto[m]: Something was broken with my Matrix bridge and so I couldn't talk on #isabelle anymore
IRC Bot (Apr 26 2021 at 21:24):@kit_ty_kate: hi, does anyone know where i can report issues/bugs by any chance?
IRC Bot (Apr 26 2021 at 21:25):@kit_ty_kate: I haven't seen any mention of a bug tracker for Isabelle anywhere
IRC Bot (Apr 26 2021 at 21:38):@NieDzejkob: you could send a mail to the isabelle-users mailing list
IRC Bot (Apr 26 2021 at 21:38):@int-e: The isabelle-users mailing list is the usual place for odd behaviors.
IRC Bot (Apr 26 2021 at 21:39):@int-e: (Makarius (the main Isabelle maintainer) likes to explain that there are no "bugs", or rather, that the term "bug" is meaningless. Call it "odd behavior" and you should avoid that trigger.)
IRC Bot (Apr 26 2021 at 21:47):@kit_ty_kate: :D
IRC Bot (Apr 27 2021 at 08:32):@pruvisto[m]: Of course, the IRC here or the Zulip (isabelle.zulipchat.com) also works.
IRC Bot (Apr 27 2021 at 08:32):@pruvisto[m]: As a first place to get some input on it (possibly more timely input than on the mailing list).
IRC Bot (Apr 27 2021 at 08:33):@pruvisto[m]: Most of the "bugs" people find are indeed really only misunderstandings and both on IRC and Zulip, there are enough advanced users to explain what is going on in such cases.
IRC Bot (Apr 27 2021 at 08:33):@pruvisto[m]: ("should Isabelle have a bug tracker" is also a long-standing point of contention with Makarius >_>)
IRC Bot (Apr 29 2021 at 12:22):@pie_: ....wat. <pruvisto[m]> ("should Isabelle have a bug tracker" is also a long-standing point of contention with Makarius >_>)
IRC Bot (Apr 30 2021 at 11:43):@NieDzejkob: hmm, looks like isabelle.in.tum.de and concrete-semantics.org are down
IRC Bot (Apr 30 2021 at 11:51):@pruvisto[m]: sigh yes
IRC Bot (Apr 30 2021 at 11:51):@pruvisto[m]: The Isabelle website at least is mirrored in a few places: https://www.cl.cam.ac.uk/research/hvg/Isabelle/
IRC Bot (Apr 30 2021 at 11:51):@pruvisto[m]: I'd hoped those instability problems were resolved now that everything was moved to a new server
IRC Bot (May 03 2021 at 21:22):@aindilis: are there any free online courses that teach mechanization at the same time as the subject itself?
Jakub Kądziołka (May 04 2021 at 11:38):Nipkow's Concrete Semantics could fit that description.
IRC Bot (May 04 2021 at 11:53):@pruvisto[m]: It's a book though, not a course as such.
IRC Bot (May 04 2021 at 20:35):@Gurkenglas: Can I tell Isabelle to, like, poke something in order to do the obvious thing to it? If I poke that i know "A /\ B", it should turn that into knowing A and B; If I poke that I need "A -> B", it should turn that into knowing A and needing B; If I poke that I have "A -> B", it should turn that into needing A and having B; etc.
IRC Bot (May 04 2021 at 20:37):@pruvisto[m]: resolution with the right rule, e.g. conjI for "and", impI for implication
IRC Bot (May 04 2021 at 20:37):@pruvisto[m]: i.e. "rule conjI"
IRC Bot (May 04 2021 at 20:37):@pruvisto[m]: there's also "safe", which applies a number of sensible intro/elim rules
IRC Bot (May 04 2021 at 20:37):@pruvisto[m]: in particular all the ones that you probably think about, but sometimes it does a bit too much for my taste
IRC Bot (May 04 2021 at 20:37):@int-e: there's also apply standard, the thing that proof does by default
IRC Bot (May 04 2021 at 20:38):@pruvisto[m]: and you can use "intro" to apply resolution with some rules exhaustively
IRC Bot (May 04 2021 at 20:38):@int-e: (but it really doesn't come up in practice)
IRC Bot (May 04 2021 at 20:38):@pruvisto[m]: I often write things like "apply (intro conjI impI allI)
IRC Bot (May 04 2021 at 20:38):@pruvisto[m]: to get basically a more "controlled" version of "apply safe"
IRC Bot (May 04 2021 at 20:39):@int-e: Yeah I do (or did, not formalizing atm) that a lot as well.
IRC Bot (May 04 2021 at 20:41):@int-e: I've done a good deal of proof (intro conjI impI allI, goal_cases)
IRC Bot (May 04 2021 at 20:41):@int-e: (usually assigning names to the cases when there were more than a couple)
IRC Bot (May 04 2021 at 20:47):@Gurkenglas: I'm looking at https://github.com/seL4/isabelle/blob/master/src/HOL/Examples/Drinker.thy#L49. I don't see how Isabelle follows that, can I make it show its work?
Jakub Kądziołka (May 04 2021 at 20:48):it's just rule exI
IRC Bot (May 04 2021 at 20:49):@int-e: Right, it just goes from drunk a ⟶ (∀x. drunk x) to ∃x. drunk x ⟶ (∀x. drunk x).
IRC Bot (May 04 2021 at 20:50):@pruvisto[m]: .. is roughly equivalent to "by standard"
IRC Bot (May 04 2021 at 20:50):@pruvisto[m]: Which in this case just picks a suitable rule
IRC Bot (May 04 2021 at 20:50):@pruvisto[m]: Which is indeed exI
IRC Bot (May 04 2021 at 20:50):@pruvisto[m]: The introduction rule for the existential quantifier in HOL
IRC Bot (May 04 2021 at 20:51):@int-e: (You can see the thing it shows in the proof state if your cursor is somewhere in the "show ?thesis " part)
IRC Bot (May 04 2021 at 20:51):@int-e: the thing it shows = the relevant proof goal
IRC Bot (May 04 2021 at 20:54):@Gurkenglas: int-e, right, that's the step I don't understand. How does it go from f(A)->B to ∃x.f(x)->B ?
IRC Bot (May 04 2021 at 20:54):@int-e: A is a witness for the existential
IRC Bot (May 04 2021 at 20:55):@int-e: exI is P(a) -> ∃ x. P(x)
IRC Bot (May 04 2021 at 20:55):@Gurkenglas: yea but P->R and P->Q don't combine into Q->R
IRC Bot (May 04 2021 at 20:55):@int-e: ?
IRC Bot (May 04 2021 at 20:56):@int-e: P(x) is an implication here.
IRC Bot (May 04 2021 at 20:56):@int-e: ∃x. drunk x ⟶ (∀x. drunk x) is ∃x. (drunk x ⟶ (∀x. drunk x))
IRC Bot (May 04 2021 at 20:56):@Gurkenglas: Oh darn I tried to introduce P Q and R to distinguish it from previous terms
IRC Bot (May 04 2021 at 20:56):@Gurkenglas: ohh i thought it was trying to prove (∃x. drunk x) -> (∀x. drunk x)
IRC Bot (May 04 2021 at 20:57):@int-e: but that would be false
IRC Bot (May 04 2021 at 20:57):@Gurkenglas: indeed
IRC Bot (May 04 2021 at 20:57):@Gurkenglas: I thought Isabelle was showing off some sort of pitfall that everybody needs to know about to not accidentally prove falsities which is apparently possible.
IRC Bot (May 04 2021 at 20:57):@Gurkenglas: Haskell has that.
Jakub Kądziołka (May 04 2021 at 20:58):well, haskell is not a very good proof assistant :P
IRC Bot (May 04 2021 at 20:59):@pruvisto[m]: If you can prove falsity in Isabelle without introducing new axioms or using oracles, we'll all be very interested to hear about it ;)
IRC Bot (May 04 2021 at 21:00):@pruvisto[m]: Should be worth one paper at least
Jakub Kądziołka (May 04 2021 at 21:00):(it has happened before, can't recall whether it was 1 or 2 papers in the end)
IRC Bot (May 05 2021 at 21:24):@gr0n: i have a quick question about fetching components from isabelle, specifically isabelle2021. when i run ./bin/isabelle components -a on that version of isabelle, it fails to fetch anything (there's a permission denied error on sketis)
IRC Bot (May 05 2021 at 21:25):@gr0n: is there any way that one could bootstrap isabelle from the hg repository rather than downloading the pre-built binary for linux?
IRC Bot (May 05 2021 at 21:33):@pruvisto[m]: Yes
IRC Bot (May 05 2021 at 21:34):@pruvisto[m]: isabelle components -I
IRC Bot (May 05 2021 at 21:34):@pruvisto[m]: isabelle components -a
IRC Bot (May 05 2021 at 21:34):@gr0n: pruvisto[m]: yeah, but the URL that 2021 gets aren't accessible anymore
IRC Bot (May 05 2021 at 21:34):@pruvisto[m]: Run that on the development version and you're set
IRC Bot (May 05 2021 at 21:34):@pruvisto[m]: Ah
IRC Bot (May 05 2021 at 21:34):@pruvisto[m]: No that's probably not possible
IRC Bot (May 05 2021 at 21:34):@pruvisto[m]: Although
IRC Bot (May 05 2021 at 21:35):@pruvisto[m]: I'm actually surprised
IRC Bot (May 05 2021 at 21:35):@pruvisto[m]: Which component is the problem?
IRC Bot (May 05 2021 at 21:35):@pruvisto[m]: But why can't you run the regular Isabelle2021 release?
IRC Bot (May 05 2021 at 21:35):@pruvisto[m]: You shouldn't have to fetch any components for that
IRC Bot (May 05 2021 at 21:35):@pruvisto[m]: They're all bundled with it
IRC Bot (May 05 2021 at 21:36):@pruvisto[m]: The component fetching is only for the development version on mercurial
IRC Bot (May 05 2021 at 21:36):@gr0n: pruvisto[m]: i'm trying to package isabelle into a linux distro that prefers building as much as possible due to supporting different libc versions and a lot of architectures
IRC Bot (May 05 2021 at 21:36):@gr0n: so i'm just trying to take the most barebones thing and bootstrap as much of isabelle as possible manually
IRC Bot (May 05 2021 at 21:37):@pruvisto[m]: Oof
Jakub Kądziołka (May 05 2021 at 21:37):you might be interested in https://github.com/nspin/nix-isabelle
IRC Bot (May 05 2021 at 21:37):@pruvisto[m]: Yeah Makarius isn't a big fan of people don't that because it tends to cause weird problems (e.g. when the versions of the components are slightly wrong)
IRC Bot (May 05 2021 at 21:38):@pruvisto[m]: People then want support for that on the mailing list and it takes time to figure out what the problem is
IRC Bot (May 05 2021 at 21:38):@gr0n: pruvisto[m]: oh i'm keeping the isabelle contrib/ versions rather than using the system versions, i'm just trying to bootstrap it from within the isabelle repo itself (hence components -a)
IRC Bot (May 05 2021 at 21:38):@pruvisto[m]: But of course I understand there are reasons for doing this
IRC Bot (May 05 2021 at 21:39):@pruvisto[m]: I don't know how long Makarius keeps the components on the server
IRC Bot (May 05 2021 at 21:39):@gr0n: also... it seems to be working now? i'm not sure why it wasn't a few minutes ago.
IRC Bot (May 05 2021 at 21:39):@gr0n: maybe i hit a weird timing
IRC Bot (May 05 2021 at 21:39):@pruvisto[m]: But I was under the impression that he does so pretty much indefinitely
IRC Bot (May 05 2021 at 21:39):@pruvisto[m]: For one, we sometimes like to go back to old versions to figure out regressions
IRC Bot (May 05 2021 at 21:40):@pruvisto[m]: However, even if you take the exact right commit in the development branch and fetch all the components, you will not end up with issbelle2021
IRC Bot (May 05 2021 at 21:41):@pruvisto[m]: For one, it will keeps its files in .isabelle
IRC Bot (May 05 2021 at 21:41):@pruvisto[m]: Not in .isabelle/Isabelle2021
IRC Bot (May 05 2021 at 21:41):@gr0n: hmm, so the preferred approach would be just to fetch the -linux tar.gz and distribute that?
IRC Bot (May 05 2021 at 21:41):@pruvisto[m]: And it will not display its name as Isabelle 2021 but as "unspecified repository version"
IRC Bot (May 05 2021 at 21:42):@gr0n: right, that sounds pretty... unacceptable to say the least :)
IRC Bot (May 05 2021 at 21:42):@pruvisto[m]: <gr0n "hmm, so the preferred approach w"> I would indeed recommend that if it is an option
IRC Bot (May 05 2021 at 21:42):@gr0n: pruvisto[m]: i think given a good enough a reason, it is.
IRC Bot (May 05 2021 at 21:42):@gr0n: and this seems like one
IRC Bot (May 05 2021 at 21:42):@pruvisto[m]: But Jakub seems to know a thing or two about packaging Isabelle
IRC Bot (May 05 2021 at 21:43):@pruvisto[m]: So if you prefer to look into alternatives, maybe have a look at the thing he linked
IRC Bot (May 05 2021 at 21:43):@gr0n: oh i totally missed that link... the @** caught me off guard and i thought it was another conversation :)
IRC Bot (May 05 2021 at 21:43):@gr0n: thnaks
IRC Bot (May 05 2021 at 21:43):@pruvisto[m]: No it's just the zulip bridge
IRC Bot (May 05 2021 at 21:44):@pruvisto[m]: That's what it looks like when someone writes on zulip
IRC Bot (May 05 2021 at 21:44):@gr0n: yeah, i see it now but completely glossed over it before :D
IRC Bot (May 05 2021 at 21:44):@pruvisto[m]: This big bundle is Makarius's solution to our very own dependency hell
IRC Bot (May 05 2021 at 21:44):@pruvisto[m]: It's not perfect, but it works very well for almost everyone
IRC Bot (May 05 2021 at 21:49):@gr0n: alright, that nix-isabelle thing is quite helpful. thanks for all the advice and information
IRC Bot (May 22 2021 at 16:41):@int-e: any opinions on the libera/freenode split?
IRC Bot (May 22 2021 at 16:59):@pruvisto[m]: Ugh
IRC Bot (May 22 2021 at 16:59):@pruvisto[m]: Yeah we should probably switch to libera
IRC Bot (May 22 2021 at 17:02):@int-e: ugh covers it well :-/
IRC Bot (May 22 2021 at 17:04):@int-e: I honestly don't know. We'd almost inevitably split up an already small and very low traffic channel. And there's a good chance that Andrew Lee and his consorts will leave it well enough alone. It's all very unpleasant.
IRC Bot (May 22 2021 at 17:07):@int-e: And of course there are other options... like OFTC, or giving up the IRC presence entirely (sniff)
Jakub Kądziołka (May 22 2021 at 17:21):I wouldn't have found the zulip without IRC, so...
IRC Bot (May 22 2021 at 20:51):@aweinstock: #haskell seems to be around halfway moved (~770 vs ~370 at the moment)
IRC Bot (May 22 2021 at 20:51):@aweinstock: well, existent in both places, so not exactly moved
IRC Bot (May 26 2021 at 03:18):@int-e: Note: It is now against Freenode policy to advertise libera.chat in the topic for project channels, and this is being enforced.
IRC Bot (May 26 2021 at 03:18):@int-e: #isabelle exists on irc.libera.chat does exist though in case anyone wants to meet up there.
IRC Bot (May 26 2021 at 03:19):@int-e: details (as of now, policies seem to be chaning every few hours): https://freenode.net/policies#channel-ownership
IRC Bot (May 26 2021 at 03:20):@int-e: this obviously doesn't mention Libera anywhere, but it's considered spam.
IRC Bot (May 26 2021 at 08:04):@pruvisto[m]: Libera does not have a Matrix bridge. :/
IRC Bot (May 26 2021 at 08:04):@pruvisto[m]: otherwise I'd happily vote for switching to that.
IRC Bot (May 26 2021 at 08:04):@pruvisto[m]: We are just moving another channel to oftc
IRC Bot (May 26 2021 at 08:15):@pruvisto[m]: A Matrix–Libera bridge is in progress, according to official information.
IRC Bot (May 26 2021 at 08:15):@pruvisto[m]: So I guess we should just move this thing to Libera and be done with it.
IRC Bot (May 26 2021 at 08:15):@pruvisto[m]: It's a damn shame Freenode had to go out like this.
Kevin Kappelmann (May 26 2021 at 09:01):Isn't libera using the same IRC protocol as is used on freenode and thus the same matrix bridge should work if you change the URL and port number?
IRC Bot (May 26 2021 at 09:02):@pruvisto[m]: I don't know, but if it were that easy, they would already have done it.
IRC Bot (May 26 2021 at 09:02):@pruvisto[m]: There's a Twitter post from two days ago saying that the matrix.org people and the Libera people are working on it.
IRC Bot (May 26 2021 at 09:03):@pruvisto[m]: The problem, I think, is that the big Matrix bridges need some form of collaboration from the IRC side to work.
IRC Bot (May 26 2021 at 09:03):@pruvisto[m]: If you just host your own small Matrix bridge, you can set it up to act just like a regular IRC client and everything's fine. But I haven't done that in the past. Because I'm lazy.
Jakub Kądziołka (May 26 2021 at 10:52):The 'impersonation' feature where the bridge posts as many users with the [m] prefix might require collaboration
IRC Bot (May 26 2021 at 10:53):@pruvisto[m]: Yes, that definitely. But there's normally also a limit on how many IRC connections can come from the same IRC address, which is not ideal for bigger bridges.
IRC Bot (May 26 2021 at 10:54):@pruvisto[m]: So I guess the big Matrix bridges usually bundle these somehow, in circumvention of the "normal" IRC protocol
IRC Bot (May 26 2021 at 10:54):@pruvisto[m]: at least that's what I gather from half-overheard remarks
IRC Bot (May 26 2021 at 10:54):@pruvisto[m]: I'm still not sure why my name appears as "pruvisto[m]" and not as "pruvisto", seeing as I'm pretty sure I enabled puppeting on the bridge
IRC Bot (May 26 2021 at 10:54):@pruvisto[m]: sigh
IRC Bot (May 26 2021 at 20:34):@pruvisto[m]: They're hoping to get the Matrix bridge on Libera up tomorrow
IRC Bot (May 29 2021 at 13:03):@pie_: -> libera
Kevin Kappelmann (May 30 2021 at 07:03):Just a test if the bridge to zulip works.
IRC Bot (May 30 2021 at 07:03):@Guest8864: works here.
IRC Bot (May 30 2021 at 09:58):@int-e: hi zulip
IRC Bot (May 30 2021 at 10:57):@pruvisto: Test?
IRC Bot (May 30 2021 at 10:57):@pruvisto: Ah okay it still works.
IRC Bot (May 30 2021 at 10:58):@pruvisto: And my name even appears as "pruvisto", not as "pruvisto[m]". Yay!
IRC Bot (May 30 2021 at 10:58):@pruvisto: int-e: Well I could take over the channel if you want me to.
IRC Bot (May 30 2021 at 10:58):@pruvisto: I haven't been op of an IRC channel since, uh, I don't know. Many years ago. :D
IRC Bot (May 30 2021 at 10:58):@pruvisto: But I could probably figure it out.
IRC Bot (May 30 2021 at 10:59):@pruvisto: I'm not terribly eager to do it, but if you're even less eager I'd happily do it.
IRC Bot (May 30 2021 at 12:16):@int-e: pruvisto: added you on chanserv. so /msg chanserv op #isabelle will work, for example.
IRC Bot (May 30 2021 at 12:20):@pruvisto: thanks
IRC Bot (May 31 2021 at 01:39):@wagle: Topic for #isabelle is "Sorry, but because of spam, only registered users can talk; see https://freenode.net/kb/answer/registration || Official channel for the Isabelle/HOL theorem prover: http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html || isabelle_zulip bridges to https://isabelle.zulipchat.com/ which keeps logs."
IRC Bot (May 31 2021 at 03:50):@int-e: What was that about? Anyway I guess neither channel is official in any capacity... is the Isabelle website doesn't know any IRC channel at all. It does know about Zulip though.
IRC Bot (May 31 2021 at 07:35):@pruvisto: I have no idea
IRC Bot (May 31 2021 at 07:35):@pruvisto: Perhaps they thought we don't know about the other one?
IRC Bot (May 31 2021 at 07:36):@pruvisto: We should put the information that this channel is bridged to zulip in the topic
IRC Bot (May 31 2021 at 07:37):@int-e: right, I took that out because it was false at the time
IRC Bot (Jun 01 2021 at 07:21):@pruvisto: fyi the word is "unofficial"
IRC Bot (Jun 01 2021 at 07:22):@pruvisto: "inofficial", if it exists at all, is very rare
IRC Bot (Jun 01 2021 at 07:22):@pruvisto: so you just outed yourself as a German speaker. ;)
IRC Bot (Jun 01 2021 at 07:22):@int-e: just giving you an incentife to try out those op powers ;)
IRC Bot (Jun 01 2021 at 07:22):@int-e: wow
IRC Bot (Jun 01 2021 at 07:22):@int-e: incentive.
IRC Bot (Jun 01 2021 at 07:23):@int-e: I need to wake up.
IRC Bot (Jun 01 2021 at 07:23):@pruvisto: incentife sounds like something a French person might write. :D
IRC Bot (Jun 01 2021 at 07:23):@pruvisto: In paper reviews you can often tell what country a person is from by the mistakes they make
IRC Bot (Jun 01 2021 at 07:24):@pruvisto: I once had a reviewer tell me "I was deceived by the presentation", presumable French because "décevoir" = "disappoint"
IRC Bot (Jun 01 2021 at 07:25):@int-e: that's an almost sinister shift in meaning
IRC Bot (Jun 01 2021 at 07:26):@pruvisto: There, I did it
IRC Bot (Jun 01 2021 at 07:26):@int-e: wee
IRC Bot (Jun 01 2021 at 08:48):@pruvisto: Who was op of the old Freenode channel anyway?
IRC Bot (Jun 01 2021 at 08:49):@pruvisto: Not sure how many regulars we lost in the move. And how many newbies.
IRC Bot (Jun 01 2021 at 08:49):@pruvisto: I guess I can advertise the channel on Twitter
IRC Bot (Jun 01 2021 at 08:49):@pruvisto: From the Isabelle account
IRC Bot (Jun 01 2021 at 08:54):@pruvisto: I wonder if we can somehow plumb a Matrix room to this one…
IRC Bot (Jun 01 2021 at 11:01):@int-e: pruvisto: larsh, Igloo, lispy, you, and I
IRC Bot (Jun 01 2021 at 11:01):@pruvisto: Me? Huh.
IRC Bot (Jun 01 2021 at 11:02):@int-e: Igloo founded it, I suspect because he wanted to formalize a darcs-like theory of patches.
IRC Bot (Jun 01 2021 at 11:03):@int-e: then I got ops from lispy one day and I looked for more active people actually involved in Isabelle :P
IRC Bot (Jun 01 2021 at 11:03):@int-e: And ended up picking larsh and you :P
IRC Bot (Jul 11 2021 at 16:17):@aweinstock: win move 12
IRC Bot (Jul 11 2021 at 16:17):@aweinstock: oops
IRC Bot (Jul 11 2021 at 16:17):@int-e: /lose :-)
IRC Bot (Aug 05 2021 at 23:38):@safinaskar: how to prove this? (case f a of True ⇒ Some (a # b) | False ⇒ None) = Some s ⟹ a # b = s
IRC Bot (Aug 06 2021 at 00:21):@pruvisto1: I would try `apply (auto split: option.splits)
IRC Bot (Aug 06 2021 at 00:21):@pruvisto1: If you have a case expression over a datatype in a proof obligation, you pretty much always want to use the splits rules of the corresponding datatype
IRC Bot (Aug 06 2021 at 00:21):@pruvisto1: uh, wait, in this case it's bool.splits
IRC Bot (Aug 06 2021 at 00:22):@pruvisto1: why are you using a case expression on booleans anyway, instead of just an "if"?
IRC Bot (Aug 06 2021 at 00:22):@pruvisto1: It's not wrong of course, but somewhat unusual
IRC Bot (Aug 06 2021 at 00:22):@pruvisto1: the splitting rule for "if" is called if_splits
IRC Bot (Aug 06 2021 at 00:28):@safinaskar: pruvisto1: thanks for answer
IRC Bot (Aug 06 2021 at 00:28):@safinaskar: pruvisto1: i simply used "try" and then copied suggested proof to source
IRC Bot (Aug 06 2021 at 00:28):@safinaskar: pruvisto1: is there a way to avoid copy? i. e. i want proof method which simply does same thing as "try"
IRC Bot (Aug 06 2021 at 00:29):@pruvisto1: I don't know what you mean by that
IRC Bot (Aug 06 2021 at 00:29):@pruvisto1: When "try" suggests something you can normally just click on it and it will copy it over
IRC Bot (Aug 06 2021 at 00:31):@safinaskar: pruvisto1: yes, but then my source will contain this unreadable proof
IRC Bot (Aug 06 2021 at 00:32):@safinaskar: pruvisto1: is there a way just to write something like "try" in my source? i don't want to have actual generated proof in my source
IRC Bot (Aug 06 2021 at 00:36):@pruvisto1: uh, no
IRC Bot (Aug 06 2021 at 00:36):@pruvisto1: that's probably a sledgehammer proof
IRC Bot (Aug 06 2021 at 00:36):@pruvisto1: they tend to be something like "apply (metis …)" or "apply (smt …)" where the … is a list of facts
IRC Bot (Aug 06 2021 at 00:37):@pruvisto1: they can get pretty big and ugly, that's why I try to avoid them
IRC Bot (Aug 06 2021 at 00:39):@safinaskar: pruvisto1: ok, thanks a lot
IRC Bot (Aug 06 2021 at 16:26):@safinaskar: is there a way to run two proof methods truly in parallel?
IRC Bot (Aug 06 2021 at 16:27):@safinaskar: i can write "by (auto|blast)"
IRC Bot (Aug 06 2021 at 16:27):@safinaskar: but it seems that this will run "auto" and if it fails, then blast
IRC Bot (Aug 06 2021 at 16:27):@safinaskar: how to run them actually in parallel?
IRC Bot (Aug 06 2021 at 16:29):@safinaskar: okey, maybe there is a way to run a proof method with a timeout?
IRC Bot (Aug 06 2021 at 16:30):@safinaskar: i. e. is there a way to write "by (auto|blast)" such that "auto" is given 5 secs to terminate, and if it fails then "blast" starts?
IRC Bot (Aug 06 2021 at 16:31):@pruvisto1: There's no such thing because that would ruin any chance of a reproducible build
IRC Bot (Aug 06 2021 at 16:33):@pruvisto1: There is the stuff by Yutaka Nagashima: https://github.com/data61/PSL
IRC Bot (Aug 06 2021 at 16:33):@pruvisto1: not sure if this runs in parallel but I think it does
IRC Bot (Aug 06 2021 at 16:34):@pruvisto1: but I think this is intended more as a more advanced version of running "try", i.e. it finds a proof that you can then copypaste into your document
IRC Bot (Aug 06 2021 at 16:34):@pruvisto1: I've never used it myself
IRC Bot (Aug 06 2021 at 17:28):@safinaskar: pruvisto1: thanks
IRC Bot (Sep 05 2021 at 05:01):@sthaan: hello :)
IRC Bot (Sep 05 2021 at 05:01):@sthaan: is there a lexicographical order over finite sets in Isabelle?
IRC Bot (Sep 05 2021 at 05:01):@sthaan: if no, how I can define an alternative "≤" order over "nat set" instead of the default subset relation "⊆"?
IRC Bot (Sep 05 2021 at 16:03):@pruvisto: You can either to a clone of the set type and instantiate the "order" type class there, or you can interpret the "order_class" locale (I think that's what it's called) for your "≤" relation.
IRC Bot (Sep 05 2021 at 16:03):@pruvisto: The former is always a bit annoying to do.
IRC Bot (Sep 05 2021 at 16:03):@pruvisto: The latter is nice but does not allow you to actually write "≤" (you'll have to come up with some notation of your own, e.g. ≤' or ≤ with something in the index
IRC Bot (Sep 05 2021 at 16:04):@pruvisto: It also doesn't work with constants that require the "order" sort, since these will still take the "≤" from the type class (which is the subset relation)
IRC Bot (Sep 05 2021 at 16:04):@pruvisto: But usually the "locale interpretation" approach works pretty well for orderings
IRC Bot (Sep 05 2021 at 16:06):@pruvisto: Something like that is e.g. done for multisets, see ~~/src/HOL/Library/Multiset.thy, search for "global_interpretation subset_mset"
IRC Bot (Sep 05 2021 at 16:07):@pruvisto: Or also here, where I define a lexicographic ordering on the complex numbers: https://www.isa-afp.org/browser_info/current/AFP/Hermite_Lindemann/Complex_Lexorder.html
IRC Bot (Sep 07 2021 at 04:08):@sthaan: pruvisto, thank you very much for your detailed answer
IRC Bot (Sep 08 2021 at 01:30):@zfnmxt: Is there any way to reverse an equality in Isabelle? That is, if I have some lemma foo: "left = right" can I get a lemma blah: "right = left" for free?
IRC Bot (Sep 08 2021 at 05:39):@sthaan: zfnmxt: foo[symmetric]
IRC Bot (Sep 08 2021 at 10:04):@zfnmxt: sthaan: Thanks. :)
IRC Bot (Sep 08 2021 at 14:52):@zfnmxt: I'm trying to prove https://gist.github.com/zfnmxt/86e90b4b310703f72158d164d33bf0c4 , is there any simplification rule that lets you move a function inside the bodies of an f? I.e. f (if b then e1 else e2) = if b then f e1 else f e2? And I tried searching for such a rule, but I just got syntax errors trying things like "if _ then _ else _".
IRC Bot (Sep 08 2021 at 14:52):@zfnmxt: s/of an f/of an if-then-else expression
IRC Bot (Sep 08 2021 at 15:03):@zfnmxt: Oh, looks like if_distrib is what I was looking for, but I was only able to find it in a bit of a roundabout way. How can I more effectively search for this sort of thing?
IRC Bot (Sep 08 2021 at 15:19):@sthaan: zfnmxt, you just forgot a bracket:
IRC Bot (Sep 08 2021 at 15:19):@sthaan: https://upload.wiuwiu.de/share.php/1ec724eb-621c-497b-9636-c42c1a9292bd/20210909_00h19m31s_grim.png
IRC Bot (Sep 08 2021 at 15:20):@zfnmxt: sthaan: Ah, I see, thank you. :)
IRC Bot (Sep 08 2021 at 15:25):@zfnmxt: One more question! I find myself constantly writing simp only: _some_rule. Is there any sort of shorthand for this thing where you're doing a rewrite with exactly one rule?
Simon Roßkopf (Sep 08 2021 at 15:26):subst _some_rule_ might help
IRC Bot (Sep 08 2021 at 15:28):@pruvisto: That does exactly one step
IRC Bot (Sep 08 2021 at 15:28):@zfnmxt: Perfect, that's what I wanted. Thanks.
IRC Bot (Sep 08 2021 at 15:29):@pruvisto: And it simply adds the preconditions as new goals
IRC Bot (Sep 08 2021 at 15:29):@pruvisto: Whereas simp tries to solve them and fails if it can't
IRC Bot (Sep 08 2021 at 15:29):@zfnmxt: Is there a good reference for everything you can do in an apply script/Isar proof? I've been reading "Programming and Proving in Isabelle/HOL" but all the information is a bit scattered through the prose.
IRC Bot (Sep 08 2021 at 15:30):@pruvisto: Now that you need to supply additional parameters to subst if you want to rewrite in the assumptions or control precisely where in the term the rewrite happens
IRC Bot (Sep 08 2021 at 15:31):@pruvisto: there's also the "rewrite" method somewhere in the library that allows for more sophisticated things
IRC Bot (Sep 08 2021 at 15:31):@pruvisto: and there's "unfolding" which acts something like a "simp only: "
IRC Bot (Sep 08 2021 at 15:31):@pruvisto: (mostly used for unfolding definitions)
IRC Bot (Sep 08 2021 at 15:31):@pruvisto: zfnmxt: There's the Isabelle/Isar reference manual in the Isabelle documentation
IRC Bot (Sep 08 2021 at 15:31):@pruvisto: There's also https://tips.isabelle.systems
IRC Bot (Sep 08 2021 at 15:32):@pruvisto: e.g. https://isabelle.systems/cookbook/src/proofs/methods/
IRC Bot (Sep 08 2021 at 15:33):@zfnmxt: Aha, that's also helpful, thanks.
IRC Bot (Sep 08 2021 at 15:52):@zfnmxt: One more question! https://gist.github.com/zfnmxt/d668599b6dd870499b59dd0653ea4654 Why does the goal try to move the equality into the bodies of the if-then-else expression?
IRC Bot (Sep 08 2021 at 15:56):@sthaan: zfnmxt, try rule if_distrib instead of simp only: if_distrib
IRC Bot (Sep 08 2021 at 15:59):@zfnmxt: sthaan: What exactly does rule do here?
IRC Bot (Sep 08 2021 at 16:03):@sthaan: sadly, I do not know why it works, I'm just a beginner myself
IRC Bot (Sep 13 2021 at 13:45):@zfnmxt: Is there any theorem that says something like A <===> B => A = B? I'm trying to prove something similar to A U B = B U A using only rules, but it's unclear to me how to manipulate the equality to do so. refl and subst don't seem particularly useful here.
IRC Bot (Sep 13 2021 at 13:46):@zfnmxt: Err, I realize now that A <===> B => A = B? is nonsensical. But my question of how to prove equalities with just rules remains :)
IRC Bot (Sep 13 2021 at 13:48):@int-e: zfnmxt: what is <===>? There's <--> or ⟷, but that's an abbreviation for =.
IRC Bot (Sep 13 2021 at 13:50):@zfnmxt: int-e: Just ignore that bit of my question entirely, I confused myself. I just want to understand how to prove equalities like A U B = B U A via rules alone.
IRC Bot (Sep 13 2021 at 13:54):@zfnmxt: Oh, I guess maybe I should just use set_eq.
IRC Bot (Sep 13 2021 at 13:55):@zfnmxt: set_eqI, sorry.
IRC Bot (Sep 13 2021 at 13:56):@int-e: yep
IRC Bot (Sep 13 2021 at 13:57):@zfnmxt: Why is <--> an abbreviation for =?
IRC Bot (Sep 13 2021 at 13:58):@int-e: Because it is equality on bools. Distinguishing between those notions would hinder rewriting.
IRC Bot (Sep 13 2021 at 13:58):@zfnmxt: Is there a rule that says [A -> B; B -> A] => (A <-> B)?
IRC Bot (Sep 13 2021 at 13:59):@int-e: Maybe? iffI is more useful, beecause it gives you meta implications directly
IRC Bot (Sep 13 2021 at 14:00):@zfnmxt: Ah! iffI is exactly what I want, I think :)
IRC Bot (Sep 13 2021 at 14:01):@int-e: There's also iff_conv_conj_imp for rewriting. Which I found by putting "_ ⟶ _" "(_ ⟷ _) = (_ ∧ _)" into the "find theorems" panel
IRC Bot (Sep 13 2021 at 14:02):@zfnmxt: Is it possible to search for "substrings" via the query panel. E.g., "⟷" doesn't work and requires the addition of wildcards and such.
IRC Bot (Sep 13 2021 at 14:03):@zfnmxt: Oh, what you wrote is a union of queries. I didn't know you could do that. Neat.
IRC Bot (Sep 13 2021 at 18:06):@zfnmxt: How can you explicitly extend the set of intro (or elim) rules used by proof (when no arguments are supplied)?
IRC Bot (Sep 13 2021 at 18:11):@sthaan: zfnmxt, I think by declaring your facts [intro] or [elim]
IRC Bot (Sep 13 2021 at 18:14):@zfnmxt: Is it not possible to add them afterwards? (And also remove them after?) I saw the ability to do so with simplification rules in one of the tutorials/manuals somewhere, so I figured it'd extend to intro/elim rules.
IRC Bot (Sep 13 2021 at 18:19):@sthaan: declare your_fact[intro]
IRC Bot (Sep 13 2021 at 18:20):@zfnmxt: sthaan: Ah, I misunderstood. I see. Thank you. :)
IRC Bot (Sep 13 2021 at 18:25):@zfnmxt: Looks like declare your_face[rule del] removes it.
IRC Bot (Sep 13 2021 at 18:26):@zfnmxt: s/face/fact
IRC Bot (Sep 22 2021 at 06:18):@sthaan: Let's say I have a record type and some restrictions on it, like this:
IRC Bot (Sep 22 2021 at 06:18):@sthaan: ```
IRC Bot (Sep 22 2021 at 06:18):@sthaan: I now want to extend the record and add additional assumptions as well:
IRC Bot (Sep 22 2021 at 06:18):@sthaan: locale wf_point =
IRC Bot (Sep 22 2021 at 06:18):@sthaan: fixes pt :: point (structure)
IRC Bot (Sep 22 2021 at 06:18):@sthaan: assumes "x pt ≤ 100" "y pt ≤ 100"
IRC Bot (Sep 22 2021 at 06:18):@sthaan: ```
IRC Bot (Sep 22 2021 at 06:18):@sthaan: record point = x :: nat y ::nat
IRC Bot (Sep 22 2021 at 06:18):@sthaan: ```
IRC Bot (Sep 22 2021 at 06:18):@sthaan: datatype color = Brown | Blue | Violet | Purple | Green
IRC Bot (Sep 22 2021 at 06:18):@sthaan: record cpoint = point + col :: color
IRC Bot (Sep 22 2021 at 06:18):@sthaan: locale wf_cpoint =
IRC Bot (Oct 14 2021 at 09:02):@pruvisto: sthaan: Bit of a late response, but did you sort out your problem?
IRC Bot (Oct 14 2021 at 09:02):@pruvisto: I don't even see what your problem is – did your message perhaps get cut off?
IRC Bot (Oct 14 2021 at 09:10):@sthaan: pruvisto, looking at the logs it seems my message indeed was cut off after 11 lines.
IRC Bot (Oct 14 2021 at 09:10):@sthaan: here is the full question:
IRC Bot (Oct 14 2021 at 09:10):@sthaan: https://upload.wiuwiu.de/share.php/40b68d9a-a37f-4bae-b59f-4e9d44b16b29/message.txt
IRC Bot (Oct 14 2021 at 09:11):@pruvisto: Isabelle/HOL does not have subtyping
IRC Bot (Oct 14 2021 at 09:11):@pruvisto: So if you have something that wants a point, you can't give it a cpoint. That's a type error.
IRC Bot (Oct 14 2021 at 09:12):@pruvisto: Well, it does have… what is that called… parametric subtyping?
IRC Bot (Oct 14 2021 at 09:12):@pruvisto: So e.g. nat list is a subtype of 'a list
IRC Bot (Oct 14 2021 at 09:12):@pruvisto: and this is how record extension works in Isabelle/HOL
IRC Bot (Oct 14 2021 at 09:13):@pruvisto: When you define your point record, it actually defines a record 'a :: point_scheme which has all the fields of your record plus an additional field more :: 'a
IRC Bot (Oct 14 2021 at 09:14):@pruvisto: And then when you extend it tocpoint, it puts the new stuff (and another more field) into the more of the point
IRC Bot (Oct 14 2021 at 09:14):@pruvisto: So with this knowledge, I think the way to fix your locales is to do fixes pt :: "'a point_scheme"
IRC Bot (Oct 14 2021 at 09:14):@pruvisto: Where the 'a has to be a fresh type variable (the name doesn't matter, Isabelle will normalise it anyway)
IRC Bot (Oct 14 2021 at 13:09):@sthaan: pruvisto, thanks this solves my problem I think. Here's my example file, if anyone is interested:
IRC Bot (Oct 14 2021 at 13:10):@sthaan: https://upload.wiuwiu.de/share.php/cbe2e5b3-40e2-4521-9d26-88bd61ba2b02/Records.thy
IRC Bot (Oct 24 2021 at 10:30):@suhr[m]: I want to prove the following lemma split_nat: "\<exists> x y. (n::nat) = x + y \<and> (x = y \<or> y = x + 1)"
IRC Bot (Oct 24 2021 at 10:32):@suhr[m]: Using proof(intro exI) gives me n = ?x + ?y1 ∧ (?x = ?y1 ∨ ?y1 = ?x + 1) goal, but I don't know how to substitute x = n div 2 and y = n - x and prove the new goal.
IRC Bot (Oct 24 2021 at 10:33):@suhr[m]: I'm new to Isar proofs as well. Things used to be much more straightforward in dependently typed languages...
IRC Bot (Oct 24 2021 at 10:49):@sthaan: suhr, in this case your goal can be solved with by presburger
IRC Bot (Oct 24 2021 at 10:51):@suhr[m]: Cool. But it's a lemma for an exercise in prog-prove, so this kind of proof is probably a bit overkill.
IRC Bot (Oct 24 2021 at 10:52):@suhr[m]: Also, I still want to lean how to use structured proofs in Isabelle.
IRC Bot (Oct 24 2021 at 10:55):@sthaan: you could also do it like this
IRC Bot (Oct 24 2021 at 10:55):@sthaan: ```isabelle
IRC Bot (Oct 24 2021 at 10:55):@sthaan: proof (intro exI)
IRC Bot (Oct 24 2021 at 10:55):@sthaan: lemma split_nat: "\<exists> x y. (n::nat) = x + y \<and> (x = y \<or> y = x + 1)"
IRC Bot (Oct 24 2021 at 10:55):@sthaan: let ?x = "n div 2"
IRC Bot (Oct 24 2021 at 10:55):@sthaan: let ?y1 = "n - ?x"
IRC Bot (Oct 24 2021 at 10:55):@sthaan: show "n = ?x + ?y1 ∧ (?x = ?y1 ∨ ?y1 = ?x + 1)" by auto
IRC Bot (Oct 24 2021 at 10:55):@sthaan: qed
IRC Bot (Oct 24 2021 at 10:55):@sthaan: ```
IRC Bot (Oct 24 2021 at 11:01):@suhr[m]: Thanks.
IRC Bot (Oct 24 2021 at 11:02):@suhr[m]: So even after let's, Isabelle shows the goal as n = ?x + ?y1 ∧ (?x = ?y1 ∨ ?y1 = ?x + 1).
IRC Bot (Oct 24 2021 at 11:03):@suhr[m]: And only after show everything is substituted.
IRC Bot (Oct 24 2021 at 11:14):@suhr[m]: Well, I still have a problem applying this lemma.
IRC Bot (Oct 24 2021 at 11:15):@suhr[m]: sent a code block: https://libera.ems.host/_matrix/media/r0/download/libera.chat/dd1421bf9b8e5fbf2c2bccfab0b172249dbe4582
IRC Bot (Oct 24 2021 at 11:15):@suhr[m]: There's an error at auto for some reason.
IRC Bot (Oct 24 2021 at 11:40):@suhr[m]: sent a code block: https://libera.ems.host/_matrix/media/r0/download/libera.chat/814bc07ed6459992521a964c09d87863018f1706
IRC Bot (Oct 24 2021 at 11:42):@suhr[m]: So close, and yet I still can't complete the goal because of ∃.
IRC Bot (Oct 24 2021 at 11:43):@suhr[m]: If I replace have by show, I get Result contains obtained parameters: ly
IRC Bot (Oct 24 2021 at 11:46):@suhr[m]: Removing (intro exI) and adding show ?thesis by blast fixes the problem.
IRC Bot (Oct 24 2021 at 20:07):@pruvisto: <suhr[m]> "And only after show everything..." <- Yes, the let things are unnecessary
IRC Bot (Oct 24 2021 at 20:07):@pruvisto: they only introduce an abbreviation
IRC Bot (Oct 24 2021 at 20:07):@pruvisto: When you do a intro exI or rule exI, you get schematic variables in your goal. The standard way to instantiate these is with a show command.
IRC Bot (Oct 24 2021 at 20:08):@pruvisto: You can also do something like proof (rule exI[of _ "take ly xs"], rule exI[of _ "drop ly xs"])
IRC Bot (Oct 24 2021 at 20:08):@pruvisto: And the thing you mentioned last is also a common pattern:
IRC Bot (Oct 24 2021 at 20:09):@pruvisto: If your goal is ∃x y. P x y, you can just prove P x0 y0 for some concrete witnesses x0 and y0 and then show your actual goal with something like by blast
IRC Bot (Oct 24 2021 at 20:10):@pruvisto: I also made a inst_existentials tactic once that does essentially the same as these rule exI[of _ foo] I mentioned above for several variables at once and is a bit nicer to use, but it's not really in the standard set of tactics available in the standard distribution
IRC Bot (Nov 07 2021 at 08:26):@sthaan: I'm getting a lot of typing errors like this lately
IRC Bot (Nov 07 2021 at 08:26):@sthaan: https://upload.wiuwiu.de/share.php/945c7529-77a9-47aa-ac38-e69e1468eeaa/20211107_09h24m16s_grim.png
IRC Bot (Nov 07 2021 at 08:27):@sthaan: is there any way to see what type for M is expected here?
IRC Bot (Nov 07 2021 at 09:20):@sthaan: it's Ctrl-Mouseover :)
IRC Bot (Nov 08 2021 at 08:42):@pruvisto: yup
IRC Bot (Nov 08 2021 at 08:43):@pruvisto: Another thing I occasionally do is using [[unify_trace_failure]]
IRC Bot (Nov 08 2021 at 08:43):@pruvisto: that shows you where exactly the unification fails
IRC Bot (Nov 08 2021 at 08:43):@pruvisto: can be a life saver if there's something subtle going on, like polymorphism
IRC Bot (Nov 08 2021 at 08:44):@pruvisto: or a big term where the only difference is that in one place there's a y instead of an x
IRC Bot (Nov 08 2021 at 08:44):@pruvisto: or a bound variable x instead of a free variable x
IRC Bot (Nov 08 2021 at 08:44):@pruvisto: Wait, in what context are you working on Turing machines?
IRC Bot (Nov 08 2021 at 09:50):@sthaan: pruvisto: thanks, I will try it out next time :)
IRC Bot (Nov 08 2021 at 09:53):@sthaan: we are trying to formalize a paper in complexity theory
IRC Bot (Nov 08 2021 at 09:55):@pruvisto: Who's "we"?
IRC Bot (Nov 08 2021 at 09:58):@sthaan: Guest6716 and me :)
IRC Bot (Nov 08 2021 at 10:00):@pruvisto: And are you students? Researchers? Sorry, just always curious when people do stuff in Isabelle.
IRC Bot (Nov 08 2021 at 10:00):@pruvisto: Also I know at least three different people/groups working on similiar stuff.
IRC Bot (Nov 08 2021 at 10:00):@pruvisto: You're either part of one of them or you ought to know about them ^^
IRC Bot (Nov 08 2021 at 10:03):@sthaan: we are grad students working part-time on this project (lead Stefan Rass):
IRC Bot (Nov 08 2021 at 10:03):@sthaan: https://www.syssec.at/en/projekte/cave-pnp
IRC Bot (Nov 08 2021 at 10:04):@pruvisto: Ah, I think somebody told me about that recently.
IRC Bot (Nov 08 2021 at 10:05):@pruvisto: I just moved to Innsbruck a few weeks ago
IRC Bot (Nov 08 2021 at 10:05):@pruvisto: In any case: Mohammad Abdulaziz and some of his colleagues and students at TUM are working on formalising various NP-complete algorithms
IRC Bot (Nov 08 2021 at 10:06):@pruvisto: I think they're using register machines though
IRC Bot (Nov 08 2021 at 10:06):@pruvisto: René Thiemann has two Bachelor's students working on Turing machines
IRC Bot (Nov 08 2021 at 10:06):@pruvisto: And then there were some people in Bremen who were also doing something with register machines, I think, but their goal was to show that diophantine equations are undecidable
IRC Bot (Nov 08 2021 at 10:09):@sthaan: > I just moved to Innsbruck a few weeks ago
IRC Bot (Nov 08 2021 at 10:09):@sthaan: Innsbruck is a really nice city, I lived there for two years :)
IRC Bot (Nov 08 2021 at 10:09):@sthaan: Thank you for the names, are they all using Isabelle?
IRC Bot (Nov 08 2021 at 10:14):@pruvisto: yes
IRC Bot (Nov 08 2021 at 10:14):@pruvisto: I think Mohammad might be most interesting to you
IRC Bot (Nov 08 2021 at 10:32):@sthaan: thank you, we will get in touch :)
IRC Bot (Nov 12 2021 at 15:57):@sthaan: Hi, I was wondering why interpretations are lost if I re-open a locale?
IRC Bot (Nov 12 2021 at 15:57):@sthaan: https://upload.wiuwiu.de/share.php/cbe7e62b-5619-47d7-a1b5-2f30ac2eae41/SavingInterpretation.thy
IRC Bot (Nov 12 2021 at 16:00):@sthaan: here the seconde thm one_is_one fails because the interpretation of A is apparently lost
IRC Bot (Nov 12 2021 at 16:01):@sthaan: here the second thm one_is_one fails because the interpretation of A is apparently lost
IRC Bot (Nov 12 2021 at 16:56):@sthaan: okay we could solve this by using sublocale :)
IRC Bot (Nov 12 2021 at 17:02):@sthaan: https://upload.wiuwiu.de/share.php/1bcfc4b0-8f69-4123-89e7-c51c0e34b81e/SavingInterpretation.thy
IRC Bot (Nov 12 2021 at 17:51):@pruvisto: yup
IRC Bot (Nov 12 2021 at 17:51):@pruvisto: interpretations do not survive exiting the current context. sublocales do.
IRC Bot (Nov 19 2021 at 14:07):@sthaan: is it possible to introduce terms into a locale using only existence?
IRC Bot (Nov 19 2021 at 14:07):@sthaan: on the theory level I can use consts and specification to achieve this, but those are not allowed when I open a locale:
IRC Bot (Nov 19 2021 at 14:07):@sthaan: https://upload.wiuwiu.de/share.php/ae99725f-3265-486a-b3e7-406b0023a952/local_specification.thy
IRC Bot (Nov 19 2021 at 14:10):@int-e: Not sure what the story is (whether consts just hasn't been localized or whether there's an actual reason for this omission), but there's SOME x. P x if all else fails
IRC Bot (Nov 19 2021 at 14:12):@int-e: It's more cumbersome though: definition x where "x == SOME x. x \<ge> 3" and then prove "x \<ge> 3" from that.
IRC Bot (Nov 19 2021 at 14:38):@sthaan: int-e, thanks I didn't think of that!
IRC Bot (Nov 19 2021 at 14:38):@sthaan: is there any other way to introduce terms from existence? I scared of SOME
IRC Bot (Nov 19 2021 at 14:38):@sthaan: int-e, thanks I didn't think of that!
IRC Bot (Nov 19 2021 at 14:38):@sthaan: is there any other way to introduce terms from existence? I'm scared of SOME
IRC Bot (Nov 19 2021 at 14:43):@sthaan: ok I guess if I never unfold the definition, I get the same results :)
IRC Bot (Nov 19 2021 at 14:44):@int-e: yes that's the idea
IRC Bot (Nov 19 2021 at 15:16):@pruvisto: "some" and "the" aren't that scary
IRC Bot (Nov 19 2021 at 15:16):@pruvisto: And the specification command probably uses them internally anyway
IRC Bot (Nov 19 2021 at 15:16):@pruvisto: But I would indeed try to keep the definition folded and just work with the derived properties
IRC Bot (Nov 19 2021 at 15:17):@pruvisto: The automation is not good at working with them
IRC Bot (Nov 19 2021 at 15:23):@sthaan: > "some" and "the" aren't that scary
IRC Bot (Nov 19 2021 at 15:23):@sthaan: yes if I never unfold anything they aren't that scary I guess :D
IRC Bot (Nov 19 2021 at 16:02):@pruvisto: They're a bit annoying to use, but otherwise…
IRC Bot (Nov 19 2021 at 16:02):@pruvisto: oh there's also "Least"
IRC Bot (Nov 20 2021 at 03:09):@pie_: has this been around http://math.andrej.com/2021/11/20/proof-assistants-stackexchange-site/
IRC Bot (Dec 16 2021 at 06:44):@sthaan: It's a pitty we can't have instantiation nat :: floor_ceiling
IRC Bot (Dec 16 2021 at 06:46):@sthaan: one would think floor and ceiling should be well defined for nat...
IRC Bot (Jan 01 2022 at 21:59):@zfnmxt: Does Isabelle have anything like haskell's "@" operator for binding a pattern to a variable? (e.g., myFun x@(Just k) = ...)
IRC Bot (Jan 01 2022 at 22:19):@pruvisto: Pattern aliases I think
IRC Bot (Jan 01 2022 at 22:19):@pruvisto: There's something in the library to do this
IRC Bot (Jan 01 2022 at 22:40):@zfnmxt: pruvisto: https://isabelle.in.tum.de/library/HOL/HOL-Library/Pattern_Aliases.html yep, thank you :)
IRC Bot (Jan 19 2022 at 19:03):@zfnmxt: I'm trying to prove something of the form P1 -> P2 -> P3 with rule induction. The variable I'm doing induction over appears in both P1 and P3, but the inductive hypothesis only uses P2 and P3, so induction isn't instantiating the predicate which appears in the relevant induction rule with what I want--is there a way to specify it manually or something? I hope that's intelligible/sufficiently clear.
IRC Bot (Jan 19 2022 at 19:06):@pruvisto: the best way to do it is to do something like show P3 using P2 P1 proof (induction …)
IRC Bot (Jan 19 2022 at 19:06):@pruvisto: if the induction rule has n premises, the induction method will unify the first n chained facts with them
IRC Bot (Jan 19 2022 at 19:07):@pruvisto: and any remaining chained facts are then simply treated as part of the statement being proved
IRC Bot (Jan 19 2022 at 19:07):@pruvisto: if that doesn't work you may have to post something more concrete
IRC Bot (Jan 19 2022 at 19:07):@pruvisto: so I can understand what the problem is
IRC Bot (Jan 19 2022 at 19:17):@zfnmxt: pruvisto: Thanks for your fast response. One sec, a bit of experimentation is in order!
IRC Bot (Jan 19 2022 at 19:44):@zfnmxt: After taking a closer look at the induction rule, I realized that I had erroneous assumptions....so, my mistake! Thanks again for your help.
IRC Bot (Jan 19 2022 at 19:45):@zfnmxt: Actually, just to make sure: if I have some inductive datatype D x y, the induction rule generated will always look something like D x y -> (rules for the cases) -> P x y, right?
IRC Bot (Jan 19 2022 at 21:54):@pruvisto: you mean an inductive predicate, right?
IRC Bot (Jan 19 2022 at 21:54):@pruvisto: this ain't Coq :D
IRC Bot (Jan 19 2022 at 21:56):@pruvisto: but yeah that looks right, for inductive predicates
IRC Bot (Jan 19 2022 at 21:57):@pruvisto: the "rules for the cases" bit is the interesting part though, of course
IRC Bot (Jan 20 2022 at 13:03):@zfnmxt: Yeah, that's what I meant. I learned with Coq so...I still try to frame everything through that :D
IRC Bot (Jan 20 2022 at 13:03):@zfnmxt: Thanks for your help again.
IRC Bot (Feb 01 2022 at 12:20):@sthaan: https://upload.wiuwiu.de/share.php/c3d4288a-ac64-4af1-9e7d-e04ca11ce27c/20220201_13h20m19s_grim.png
IRC Bot (Feb 01 2022 at 12:21):@sthaan: what could cause this "Bad number of arguments" error, but only the second time?
IRC Bot (Feb 01 2022 at 12:39):@pruvisto: huh
IRC Bot (Feb 01 2022 at 12:39):@pruvisto: I never quite understood how "(structure)" works though
IRC Bot (Feb 01 2022 at 12:39):@pruvisto: that… is an excellent question
IRC Bot (Feb 01 2022 at 12:44):@sthaan: removing (structure) gives the same error :(
IRC Bot (Feb 01 2022 at 12:44):@sthaan: also if I remove the second locale definition, the error starts appearing on the first locale
Manuel Eberl (Feb 01 2022 at 12:58):Can you show a more complete example? Including at least the definition of TM?
IRC Bot (Feb 01 2022 at 12:59):@pruvisto: Oops, that was me on Zulip. :D
IRC Bot (Feb 01 2022 at 12:59):@int-e: Oh. The '@' is a bit unfortunate.
Mathias Fleury (Feb 01 2022 at 13:00):My guess would be that the name foo_TM is already used internally somewhere, leading to the problem you observe.
IRC Bot (Feb 01 2022 at 13:00):@pruvisto: Not sure why it does that. But what is the problem?
IRC Bot (Feb 01 2022 at 13:06):@sthaan: foo_TM is not used anywhere else and a quick grep -ri "foo_TM" /opt/Isabelle2021-1/src/ also gives no result
Mathias Fleury (Feb 01 2022 at 13:08):unless foo_TM is generated as a name bei some package
IRC Bot (Feb 01 2022 at 13:13):@pruvisto: I'd be surprised if that were the cause of this behaviour. But we'll only really be able to tell once we see more of the code.
IRC Bot (Feb 01 2022 at 13:15):@sthaan: AHA! I found the problem: It was in a comment below
IRC Bot (Feb 01 2022 at 13:15):@sthaan: Here's a minimal example
IRC Bot (Feb 01 2022 at 13:16):@sthaan: https://upload.wiuwiu.de/share.php/79c53277-5393-479f-a5c8-c1b216ad0e50/Test.thy
IRC Bot (Feb 01 2022 at 13:16):@int-e: pruvisto: It clashes with the convention of using @ for addressing people (indicating a target, rather than a source).
IRC Bot (Feb 01 2022 at 13:17):@sthaan: Replacing typ>‹('a) R› with typ>‹('a, 'b) R› in the comment fixes the error
IRC Bot (Feb 01 2022 at 13:17):@pruvisto: sthaan: Ah, so the error came from the typ antiquotation
IRC Bot (Feb 01 2022 at 13:20):@sthaan: this is quite confusing as it breaks my intuition about where to look:
IRC Bot (Feb 01 2022 at 13:20):@sthaan: * stuff below can't cause an error further up
IRC Bot (Feb 01 2022 at 13:20):@sthaan: * comments do not matter
IRC Bot (Feb 01 2022 at 13:22):@pruvisto: These kinds of comments are not comments like when you "comment something out" in Java
IRC Bot (Feb 01 2022 at 13:22):@pruvisto: These comments are part of the formal proof document, so they are also checked (namely for type-correctness)
IRC Bot (Feb 01 2022 at 13:22):@pruvisto: there are also the (* foo *) comments, which, to my knowledge, are not checked in any way
IRC Bot (Feb 01 2022 at 13:23):@pruvisto: (they can, however, still cause "errors" occasionally because extremely long comments can mess with the parser in Isabelle/jEdit)
IRC Bot (Feb 01 2022 at 13:23):@sthaan: still the error should have been shown on the antiquotation, not on the definition further up 🤔�
IRC Bot (Feb 01 2022 at 13:24):@pruvisto: "stuff below can't cause an error further up", well, that can sometimes happen when you have a command invocation that spans multiple lines. Like, if you have a function definition that is 100 lines long and something fails in it, it might be the "fun" command at the very beginning that shows an error
IRC Bot (Feb 01 2022 at 13:24):@pruvisto: however, why this happens in this particular case, I have no idea
IRC Bot (Feb 01 2022 at 13:24):@pruvisto: I don't think it should
IRC Bot (Feb 01 2022 at 13:24):@pruvisto: feel free to send this to the mailing list
IRC Bot (Feb 01 2022 at 13:24):@pruvisto: I think Makarius does care about errors showing up in the right place
IRC Bot (Feb 01 2022 at 13:46):@sthaan: ok, thank you, I will send this example to the mailing list :)
IRC Bot (Feb 08 2022 at 16:13):@sthaan: I tried to send an email to isabelle-users@cl.cam.ac.uk, but it doesn't show up in the archive, and I don't see any signs that it was received correctly. Do I need to be subscribed to the mailing list to send emails to it?
IRC Bot (Feb 08 2022 at 17:24):@pruvisto: No but it might be waiting for moderator approval
IRC Bot (Feb 08 2022 at 18:36):@sthaan: hm, I did not get any conformation that my message is subject to moderator approval ...
IRC Bot (Feb 09 2022 at 10:36):@pruvisto: hm, it is odd that it still didn't go through
IRC Bot (Feb 09 2022 at 10:36):@pruvisto: the address that I use is cl-isabelle-users@lists.cam.ac.uk
IRC Bot (Feb 09 2022 at 10:37):@pruvisto: not sure if yours works as well
IRC Bot (Feb 09 2022 at 11:14):@sthaan: I got the address from https://isabelle.in.tum.de/ where it is shown without the cl-
IRC Bot (Feb 09 2022 at 11:14):@pruvisto: yeah maybe it's just an alias
IRC Bot (Feb 09 2022 at 11:15):@sthaan: ok, i've sent it to cl-isabelle-users@lists.cam.ac.uk too now, let's see if it goes through
IRC Bot (Feb 23 2022 at 09:51):@sthaan: hi, I sent an email to both isabelle-users@cl.cam.ac.uk and cl-isabelle-users@lists.cam.ac.uk on the 7th and 9th respectively and looking at the archives it seems like they didn't went through :frown:
IRC Bot (Feb 23 2022 at 09:53):@sthaan: I got no mails indicating what the error could have been...
IRC Bot (Feb 23 2022 at 09:53):@sthaan: any ideas what I could do about it?
Kevin Kappelmann (Feb 23 2022 at 10:00):It seems like you are not the only one facing that problem. Please send an email to Larry Paulson and tell him that your emails are not getting through lp15@cam.ac.uk
IRC Bot (Feb 23 2022 at 10:02):@sthaan: thank you, I will try that :smile:
Kevin Kappelmann (Feb 23 2022 at 17:06):I just saw that your email went through. Did it just get stuck or what happened? I am curious because I'd like to help people here on Zulip in case they have similar problems.
IRC Bot (Feb 23 2022 at 22:46):@sthaan: Messages from non-subscribers used to be silently dropped. Larry Paulson kindly changed to policy and it seems like moderators can approve mails from non-subscribers now.
IRC Bot (Feb 23 2022 at 22:46):@pruvisto: Urgh
IRC Bot (Feb 23 2022 at 22:46):@pruvisto: Sorry about that bad experience.
IRC Bot (Feb 23 2022 at 22:49):@sthaan: no need to be! we figured it out in the end, thank you for all the help :)
IRC Bot (Feb 23 2022 at 22:52):@sthaan: but there might be other people whose mails have also been silently deleted
IRC Bot (Mar 03 2022 at 10:04):@sthaan: is there a good way to stop blast from executing while I'm typing somewhere in the document?
IRC Bot (Mar 03 2022 at 10:04):@sthaan: If I'm rewriting something the proof below needs, blast starts, doesn't find anything and uses up all CPU
IRC Bot (Mar 04 2022 at 14:29):@pruvisto: I usually just comment it out and replace it with a sorry
IRC Bot (Mar 04 2022 at 14:35):@sthaan: okay, i see, I'm doing something similar, but I thought maybe there's a better way to stop checking the document temporariliy
Kevin Kappelmann (Mar 04 2022 at 14:40):Isn't there a switch to turn off continuous checking, cf 3.1.2 here https://isabelle.in.tum.de/dist/doc/jedit.pdf
IRC Bot (Mar 04 2022 at 22:02):@sthaan: Kevin Kappelmann, thank you, this works without commenting out stuff :)
IRC Bot (Mar 18 2022 at 17:51):@TheHermann: hi, where i can find tutorial for first order logic in Isabelle?. I checked the official site but i didnt found useful tutorial.
IRC Bot (Mar 18 2022 at 19:37):@sthaan: TheHermann, I think first order propositions can often be solved by means like blast, auto, ...
IRC Bot (Mar 18 2022 at 19:37):@sthaan: What are you looking to prove?
IRC Bot (Mar 18 2022 at 22:24):@TheHermann: sthaan, an security protocol with first order logic
IRC Bot (Mar 18 2022 at 22:25):@TheHermann: but i dont undestand how use first order logic in Isabelle
IRC Bot (Mar 21 2022 at 10:53):@TheHermann: hi
IRC Bot (Mar 21 2022 at 10:53):@TheHermann: how use first order logic in Isabelle?
Kevin Kappelmann (Mar 21 2022 at 11:36):Do you want to work in first-order logic or do you want to prove things about first-order logic?
For the former, you can build your sessions on top of Isabelle/FOL, for the latter you might want to use Isabelle/HOL and an existing AFP entry for FOL: https://www.isa-afp.org/topics.html
IRC Bot (Mar 21 2022 at 14:41):@TheHermann: isabelle_zulip_, i want to prove things about first order logic
IRC Bot (Mar 21 2022 at 15:52):@TheHermann: I have to try to write the public key Needham-Schroeder protocol in FOL. but I didn't understand Isabelle's syntax.
Kevin Kappelmann (Mar 21 2022 at 15:54):You should read a tutorial, for example this one: https://isabelle.in.tum.de/dist/Isabelle2021-1/doc/prog-prove.pdf
IRC Bot (Mar 21 2022 at 16:25):@TheHermann: ok...i try to read this tutorial thanks :). im new in Isabelle
IRC Bot (Mar 21 2022 at 22:56):@TheHermann: are there any examples of protocols written in fol?
Kevin Kappelmann (Mar 23 2022 at 08:23):there are examples of protocols in the afp https://www.isa-afp.org/topics.html
Why do you need fol for your protocol? Can't you just formalise whatever rules of interaction you have in mind in Isabelle/HOL directly?
IRC Bot (Mar 28 2022 at 15:31):@TheHermann: how write axiom like A send B the message A,B in Isabelle?
IRC Bot (Mar 28 2022 at 16:54):@TheHermann: in FOL
IRC Bot (Mar 28 2022 at 17:04):@int-e: There's a mismatch here. FOL just has quantifiers, function symbols, and predicates. There's nothing about messages. Presumably what you describe would be captured by a predicate. There's bound to be papers on this by people who've formalized cryptographic protocols, but I don't know anything about it.
IRC Bot (Mar 28 2022 at 17:05):@int-e: The other oddity here is why you'd want to use FOL rather than HOL when doing this with Isabelle... HOL is more expressive and has much better support.
IRC Bot (Mar 28 2022 at 17:07):@TheHermann: I have to use FOL, but i dont undestand how write functions and predicares in Isabelle
IRC Bot (Mar 28 2022 at 17:15):@int-e: If you really want to use Isabelle/FOL, apparently the bool type is o. A predicate would be a function to o. For example, it declares eq :: ‹['a, 'a] ⇒ o› near the top of https://isabelle.in.tum.de/library/FOL/FOL/IFOL.html
IRC Bot (Mar 28 2022 at 17:17):@int-e: Actually, even if your goal is to use Isabelle/FOL you should probably go through one of the Isabelle/HOL tutorials (like progprove, which somebody suggested earlier) first... there's a lot of syntax, semantics, tools, and quirks to learn before you can hope to use Isabelle/* for anything productively.
IRC Bot (Mar 28 2022 at 17:18):@int-e: A lot of the syntax is actually established in Isabelle/Pure which is the foundation for both HOL and FOL (and a couple of others).
IRC Bot (Mar 28 2022 at 18:35):@aweinstock: TheHermann: https://en.wikipedia.org/wiki/Burrows-Abadi-Needham_logic#Basic_rules looks like it's a set of predicates and axioms you can encode into first-order logic to start with, but it's allegedly unsound
IRC Bot (Mar 28 2022 at 18:45):@aweinstock: things like https://eprint.iacr.org/2000/067.pdf and https://eprint.iacr.org/2006/398.pdf provider stronger guarantees than BAN logic, but they're much more involved to formalize
IRC Bot (Mar 28 2022 at 18:46):@aweinstock: (they both involve encodings of computable functions and the plumbing to network them)
IRC Bot (Mar 28 2022 at 21:54):@TheHermann: thanks for the replies
IRC Bot (Mar 28 2022 at 21:55):@TheHermann: I go to sleep, night!!
IRC Bot (Apr 05 2022 at 16:25):@TheHermann: hi, How do I know if there is already a rule on Isabelle that I can apply ?. Is there a list of all the FOL rules I can apply ?.
IRC Bot (Apr 09 2022 at 08:41):@TheHermann: how works functions on Isabelle? is https://pastebin.com/P5nm68qc functions or predicate?
IRC Bot (Apr 09 2022 at 16:20):@TheHermann: Is it possible to prove a lemma using other preceding lemmas ?. Like I have to prove the lemma D but to do it I have to use the lemma A and the lemma B
Manuel Eberl (Apr 09 2022 at 23:58):Of course. How that looks exactly depends on whether you're using Isar or tactic-style proofs.
Manuel Eberl (Apr 09 2022 at 23:59):In Isar it's something like have "a = b" using mylemmy by some_proof_method
Manuel Eberl (Apr 09 2022 at 23:59):*mylemma
Manuel Eberl (Apr 09 2022 at 23:59):in tactic-style proofs it's… well actually exactly the same, also with "using"
Manuel Eberl (Apr 10 2022 at 00:00):with respect to your other question, as has been said multiple times, you're probably not going to get a lot of answers if you ask questions about Isabelle/ZF (the fact that you have an "o" in your type indicates that that is the case).
Manuel Eberl (Apr 10 2022 at 00:00):(or Isabelle/FOL in your case I guess)
Manuel Eberl (Apr 10 2022 at 00:01):So the best approach is probably to learn a bit of Isabelle/HOL and then switch to ZF or FOL or whatever; by that point hopefully a lot of things will have become much clearer to you.
IRC Bot (Apr 14 2022 at 14:28):@TheHermann: hi
IRC Bot (Apr 14 2022 at 14:29):@TheHermann: how compare two predicate in isabelle?
IRC Bot (Apr 29 2022 at 21:32):@hesse: I get Response_reference(TTP, B) from server and Store_id(A, B) from user A. how compare Response_reference(TTP, B) and Store_id(A, B) if the identity B returned by the server is equal to the identity B that A has?. I thought about using Response_reference and Store_id as predicate. i using only first order logic
IRC Bot (Apr 30 2022 at 05:04):@int-e: This protocol verification (I guess) project feels so wrong. Squeezing protocol descriptions (and specifications?) into FOL is already a tall order, but then why target Isabelle/FOL? It's not exactly well developed...
IRC Bot (Apr 30 2022 at 10:25):@TheHermann: I get Response_reference(TTP, B) from server and Store_id(A, B) from user A. how compare Response_reference(TTP, B) and Store_id(A, B) if the identity B returned by the server is equal to the identity B that A has?. I thought about using Response_reference and Store_id as predicate. i using only first order logic
IRC Bot (Jun 24 2022 at 10:53):@sthaan: hi, how would you go about contributing lemmas to the standard library?
IRC Bot (Jun 24 2022 at 10:53):@sthaan: is there any policy about what is 'interesting enough' to qualify?
Manuel Eberl (Jun 24 2022 at 11:33):Not really. It has to be of sufficient general interest.
Manuel Eberl (Jun 24 2022 at 11:33):So if it's something fairly basic about lists, multisets, numbers, analysis, etc. that probably belongs in the algebra.
Manuel Eberl (Jun 24 2022 at 11:34):If it's something interesting but big enough to be packaged in an AFP entry, an AFP entry is probably a better choice.
Manuel Eberl (Jun 24 2022 at 11:34):Feel free to post something here and I can tell you what my opinion is.
IRC Bot (Jun 24 2022 at 11:38):@sthaan: for example this
IRC Bot (Jun 24 2022 at 11:38):@sthaan: ```isabelle
IRC Bot (Jun 24 2022 at 11:38):@sthaan: lemma ae_word_length_iff[iff]:
IRC Bot (Jun 24 2022 at 11:38):@sthaan: fixes P :: "'s::finite list ⇒ bool"
IRC Bot (Jun 24 2022 at 11:38):@sthaan: shows "Alm_all P ⟷ (∃n. ∀w. n ≤ length w ⟶ P w)"
IRC Bot (Jun 24 2022 at 11:38):@sthaan: ```
IRC Bot (Jun 24 2022 at 11:39):@sthaan: ```isabelle
IRC Bot (Jun 24 2022 at 11:39):@sthaan: lemma finite_imp_inj_to_nat_fix_one:
IRC Bot (Jun 24 2022 at 11:39):@sthaan: fixes A::"'a set" and x::'a and y::nat
IRC Bot (Jun 24 2022 at 11:39):@sthaan: assumes "finite A"
IRC Bot (Jun 24 2022 at 11:39):@sthaan: shows "∃g. inj_on g A ∧ g x = y"
IRC Bot (Jun 24 2022 at 11:39):@sthaan: ```
IRC Bot (Jun 24 2022 at 11:39):@sthaan: ```isabelle
IRC Bot (Jun 24 2022 at 11:39):@sthaan: lemma nat_strict_mono_greatest:
IRC Bot (Jun 24 2022 at 11:39):@sthaan: fixes f::"nat ⇒ nat" and N::nat
IRC Bot (Jun 24 2022 at 11:39):@sthaan: assumes "strict_mono f" "f 0 ≤ N"
IRC Bot (Jun 24 2022 at 11:39):@sthaan: obtains n where "f n ≤ N" and "∀m. f m ≤ N ⟶ m ≤ n"
IRC Bot (Jun 24 2022 at 11:39):@sthaan: ```
Manuel Eberl (Jun 24 2022 at 11:44):Hmm I don't know, these seem a bit too specific for my taste.
Manuel Eberl (Jun 24 2022 at 11:47):The third one seems fairly simple to me: for functions nat ⇒ nat, strict_mono f implies filterlim f at_top sequentially (i.e. the sequence f tends to ∞)
Manuel Eberl (Jun 24 2022 at 11:47):Thus there exists some number n such that f n > N, and thus there also exists a least n such that f n > N.
Manuel Eberl (Jun 24 2022 at 11:47):Doing it that way the proof shouldn't be more than like 5 lines or so.
Manuel Eberl (Jun 24 2022 at 11:50):Your second lemma could easily be generalised to countable instead of finite, and in fact it could even be generalised to something like "if A ⊆ B and B is countable, then any injective function f : A → ℕ can be extended to an injective function g : B → ℕ"
Manuel Eberl (Jun 24 2022 at 11:51):in that form one could potentially think of adding it to the library (if it doesn't already exist there in a similar form)
Manuel Eberl (Jun 24 2022 at 11:51):(of course this could be generalised even further, but then one has to talk about cardinalities.)
Manuel Eberl (Jun 24 2022 at 11:53):something like "if A ⊆ B and |B| ≤ |C| as cardinal numbers, then any injective function f : A → C can be extended to an injective function f : A → C"
Manuel Eberl (Jun 24 2022 at 11:53):err, f : B → C at the end there
Manuel Eberl (Jun 24 2022 at 11:53):actually g : B → C
Manuel Eberl (Jun 24 2022 at 11:53):apparently COVID is eating away my brain
Manuel Eberl (Jun 24 2022 at 11:54):So yeah in any case, that's another criterion: if you want to add it to the library, it should be as general as possible (within reason, of course – if the generalisation is much more complicated, maybe not)
Manuel Eberl (Jun 24 2022 at 11:55):The first one is questionable… the "finite" typeclass makes it very restrictive since there aren't that many finite types that you typically use. But it might be somewhat useful. I'd say if it can be proven within just a few lines, I probably wouldn't add it to the library. Otherwise one might consider it.
IRC Bot (Jun 24 2022 at 12:03):@sthaan: > Thus there exists some number n such that f n > N, and thus there also exists a least n such that f n > N.
IRC Bot (Jun 24 2022 at 12:03):@sthaan: Yes, but this is not the conclusion of nat_strict_mono_greatest?
Manuel Eberl (Jun 24 2022 at 12:04):Okay well you still have to subtract 1 I guess.
Manuel Eberl (Jun 24 2022 at 12:05):Or you just use the GREATEST operator instead.
Manuel Eberl (Jun 24 2022 at 12:05):Should also work.
Manuel Eberl (Jun 24 2022 at 12:06):Or indeed you just write Max {n. f n ≤ N}, which works because {n. f n ≤ N} ⊆ {..<n0} which implies finiteness (where n0 is that number we obtained where f n0 > N)
IRC Bot (Jun 24 2022 at 12:09):@sthaan: yes, that's kind of how we proved it :)
IRC Bot (Jun 24 2022 at 12:09):@sthaan: https://upload.kikeriki.at:5281/file_share/CyLYWnTQcroiClZP2sqgb_Rf/nat_strict_mono_greatest.txt
IRC Bot (Jun 24 2022 at 12:11):@sthaan: ok this file got mangled somehow (?)
IRC Bot (Jun 24 2022 at 12:12):@sthaan: https://upload.kikeriki.at:5281/file_share/V1QOjCVk71LJno_MLPvxp7Ex/nat_strict_mono_greatest.txt
IRC Bot (Jun 24 2022 at 13:06):@sthaan: ok the proof for finite_imp_inj_to_nat_fix_one for countable A is probably kind of lengthy...:
IRC Bot (Jun 24 2022 at 13:06):@sthaan: https://upload.kikeriki.at:5281/file_share/4iltzEL5YrsLohGfv2NuhMWv/Contrib.thy
IRC Bot (Aug 25 2022 at 17:13):@rawburt: hey all. i'm working through https://github.com/nipkow/fds_ss20/blob/master/ex01.pdf and i'm having trouble proving the lmax function. (i'm not a student... just trying to learn through these resources :) i've tried a few helper lemmas and nothing seems to stick. i've created a few infinite loops. here's my code https://gist.github.com/rawburt/2e8596e44241b46aecfd5607988f4167 it doesn't include any of the failed attempts. the hint in t
IRC Bot (Aug 25 2022 at 17:13):@rawburt: the hint in the worksheet says "you may need an auxiliary lemma about lmax and snoc" and i'm failing to discover what the lemma may be. any nudges in the right direction would be much appreciated. thanks!
Alexander Taepper (Aug 25 2022 at 17:38):I think a list to its reverse behave similar to # to snoc :)
IRC Bot (Aug 25 2022 at 18:32):@rawburt: thanks! i'll poke around some more
Manuel Eberl (Aug 25 2022 at 19:21):To expand a bit more on this: a common approach with these problems is to see where the simplifier gets stuck.
Manuel Eberl (Aug 25 2022 at 19:22):If you have a goal where you have something like "length (append xs ys)", then that's a sign that you need to prove a lemma about how "length" and "append" interact. And that perhaps you even want to add that as a [simp] lemma.
Manuel Eberl (Aug 25 2022 at 19:22):The situation here is probably similar, just with lmax and snoc.
IRC Bot (Aug 25 2022 at 19:23):@rawburt: i've definitely been doing that. i'm quite new to it all so the full vision/intuition isn't quite there. but, that's why i'm working through these exercises :)
IRC Bot (Aug 25 2022 at 19:23):@rawburt: i appreciate all the pointers and feedback
Manuel Eberl (Aug 25 2022 at 19:25):Well if you need further hints feel free to ask.
Manuel Eberl (Aug 25 2022 at 19:26):The learning curve for theorem provers is pretty horrible.
IRC Bot (Aug 25 2022 at 19:29):@rawburt: yes it is, ha!
IRC Bot (Aug 25 2022 at 19:29):@rawburt: but that's part of the fun... and the pain
IRC Bot (Aug 29 2023 at 05:26):@shamelessshill: Sorry for asking this, but anybody in here?
Lukas Stevens (Aug 29 2023 at 08:01):Hi, most people are on zulip (isabelle.zulipchat.com) or on the mailing list.
IRC Bot (Oct 06 2023 at 13:23):@zzai`ed: https://www.youtube.com/watch?v=sqSA-SY5Hro
IRC Bot (Oct 06 2023 at 13:23):@zzai`ed: God, if you’re 5 foot 3 and you’re 300 pounds
IRC Bot (Oct 06 2023 at 13:23):@zzai`ed: Taxes ought not to pay for your bags of fudge rounds
IRC Bot (Oct 06 2023 at 13:23):@zzai`ed: Young men are puttin’ themselves six feet in the ground
IRC Bot (Oct 06 2023 at 13:23):@zzai`ed: ‘Cause all this damn country does is keep on kickin’ them down
IRC Bot (Oct 06 2023 at 13:23):@zzai`ed: irc.supernets.org #superbowl
IRC Bot (Oct 06 2023 at 13:24):@**zzaied**: zzaied pie_ dagit landonf bfiedler int-e isabelle_zulip proidiot mal``
IRC Bot (Dec 11 2023 at 21:44):@baruchel: Somebody here?
Last updated: Dec 26 2024 at 08:23 UTC