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 :)

@**pruvisto[m]**: The main concern is that we have to maybe rein in the trash talk a bit now. :P

@**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. :)

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? :)

@**int-e**: Uh, no more talk about bugs?

@**int-e**: Bugs in Isabelle, I mean. *ducks*

@**pruvisto[m]**: I think that's okay. As of yet, Makarius still boycotts Zulip, I think?

@**int-e**: it's hard to tell who's lurking behind the isabelle_zulip nick

@**pruvisto[m]**: Yeah also Zulip is archived semi-publicly.

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

@**pruvisto[m]**: I don't even know who made this channel in the first place.

@**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")

@**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.

@**int-e**: (even if it requires registration it still is public to my mind)

@**int-e**: Oh I'm an op here? I forgot...

@**pruvisto[m]**: Yes, absolutely.

@**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.

@**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.

@**pruvisto[m]**: You mean the people who are currently actively online there or the ones that are subscribed to the IRC stream?

@**int-e**: In any case, personally I think we can try this out and see where it goes.

@**pruvisto[m]**: (i.e. who see what is going on there?)

@**int-e**: the latter I think

@**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

@**int-e**: people we might actually talk to if we catch there interest in the moment

@**int-e**: *their

@**pruvisto[m]**: in any case, Zulip is probably a better venue for any concrete questions

@**pruvisto[m]**: because it is threaded and more searchable

@**pruvisto[m]**: so if people have concrete questions, it would be better to ask on there

@**int-e**: browser windows take up too much space

@**int-e**: :P

@**pruvisto[m]**: I usually have it as a pinned tab in Firefox

@**pruvisto[m]**: (with Tree Style Tabs)

@**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

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

@**pruvisto[m]**: Private messages are probably difficult because there is only one user on the Zulip side (Kevin's bot).

@**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

@**pruvisto[m]**: So it would probably be a bit awkward to use.

@**pruvisto[m]**: actually even from the IRC side it would be awkward

@**pruvisto[m]**: the same problem, you'd have to tell the bot which user the message is supposed to go to

@**pruvisto[m]**: This is probably difficult to do with the current bridge.

@**int-e**: pruvisto[m]: Yeah I realized that "private chat" was ambiguous... messaging Zulip users privately is different from what I asked.

Here's the relevant thread about direct messaging containing some thoughts https://github.com/42wim/matterbridge/issues/191

@**pruvisto[m]**: Then what did you mean?

@**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).

@**int-e**: Anyway it's not a huge deal... as far as I can see right now.

@**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.

@**int-e**: But I'm not sure... I joined much later.

The archive lives here btw: https://isabelle.systems/zulip-archive/

@**int-e**: Odd. I thought I had extended that ban.

@**pruvisto[m]**: hm?

@**int-e**: wrong channel, my bad.

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).

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.

@**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.

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!

@**int-e**: I often thought that the experience would be less awful if the cursor keys would *not* work in that mode.

@**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?

@**pruvisto[m]**: The operation also has to be commutative and associative

@**pruvisto[m]**: then you can use Finite_Set.fold

@**pruvisto[m]**: Take a look at the comp_fun_commute and comp_fun_idem locales, and how e.g. the sum function does it.

@**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)

@**JCaesar**: ty.

@**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?

@**pruvisto[m]**: You should try the zulip

@**pruvisto[m]**: isabelle.zulipchat.com

@**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...)

@**aindilis**: pruvisto[m]: ty!

@**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/

Hm, somehow I can't post anything on this channel anymore through Matrix. >_>

I was going to reply to what you said with "You have got to be joking"

Hm, the messages also don't show up in my Matrix. Maybe the bridge is broken?

@**pruvisto[m]**: Ah, I think I got it working again. :)

@**pruvisto[m]**: Something was broken with my Matrix bridge and so I couldn't talk on #isabelle anymore

@**kit_ty_kate**: hi, does anyone know where i can report issues/bugs by any chance?

@**kit_ty_kate**: I haven't seen any mention of a bug tracker for Isabelle anywhere

@**NieDzejkob**: you could send a mail to the isabelle-users mailing list

@**int-e**: The isabelle-users mailing list is the usual place for odd behaviors.

@**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.)

@**kit_ty_kate**: :D

@**pruvisto[m]**: Of course, the IRC here or the Zulip (isabelle.zulipchat.com) also works.

@**pruvisto[m]**: As a first place to get some input on it (possibly more timely input than on the mailing list).

@**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.

@**pruvisto[m]**: ("should Isabelle have a bug tracker" is also a long-standing point of contention with Makarius >_>)

@**pie_**: ....wat. <pruvisto[m]> ("should Isabelle have a bug tracker" is also a long-standing point of contention with Makarius >_>)

@**NieDzejkob**: hmm, looks like isabelle.in.tum.de and concrete-semantics.org are down

@**pruvisto[m]**: sigh yes

@**pruvisto[m]**: The Isabelle website at least is mirrored in a few places: https://www.cl.cam.ac.uk/research/hvg/Isabelle/

@**pruvisto[m]**: I'd hoped those instability problems were resolved now that everything was moved to a new server

@**aindilis**: are there any free online courses that teach mechanization at the same time as the subject itself?

Nipkow's Concrete Semantics could fit that description.

@**pruvisto[m]**: It's a book though, not a course as such.

@**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.

@**pruvisto[m]**: resolution with the right rule, e.g. conjI for "and", impI for implication

@**pruvisto[m]**: i.e. "rule conjI"

@**pruvisto[m]**: there's also "safe", which applies a number of sensible intro/elim rules

@**pruvisto[m]**: in particular all the ones that you probably think about, but sometimes it does a bit too much for my taste

@**int-e**: there's also `apply standard`

, the thing that `proof`

does by default

@**pruvisto[m]**: and you can use "intro" to apply resolution with some rules exhaustively

@**int-e**: (but it really doesn't come up in practice)

@**pruvisto[m]**: I often write things like "apply (intro conjI impI allI)

@**pruvisto[m]**: to get basically a more "controlled" version of "apply safe"

@**int-e**: Yeah I do (or did, not formalizing atm) that a lot as well.

@**int-e**: I've done a good deal of proof (intro conjI impI allI, goal_cases)

@**int-e**: (usually assigning names to the cases when there were more than a couple)

@**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?

it's just `rule exI`

@**int-e**: Right, it just goes from drunk a ⟶ (∀x. drunk x) to ∃x. drunk x ⟶ (∀x. drunk x).

@**pruvisto[m]**: .. is roughly equivalent to "by standard"

@**pruvisto[m]**: Which in this case just picks a suitable rule

@**pruvisto[m]**: Which is indeed exI

@**pruvisto[m]**: The introduction rule for the existential quantifier in HOL

@**int-e**: (You can see the thing it shows in the proof state if your cursor is somewhere in the "show ?thesis " part)

@**int-e**: the thing it shows = the relevant proof goal

@**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 ?

@**int-e**: A is a witness for the existential

@**int-e**: exI is P(a) -> ∃ x. P(x)

@**Gurkenglas**: yea but P->R and P->Q don't combine into Q->R

@**int-e**: ?

@**int-e**: P(x) is an implication here.

@**int-e**: ∃x. drunk x ⟶ (∀x. drunk x) is ∃x. (drunk x ⟶ (∀x. drunk x))

@**Gurkenglas**: Oh darn I tried to introduce P Q and R to distinguish it from previous terms

@**Gurkenglas**: ohh i thought it was trying to prove (∃x. drunk x) -> (∀x. drunk x)

@**int-e**: but that would be false

@**Gurkenglas**: indeed

@**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.

@**Gurkenglas**: Haskell has that.

well, haskell is not a very good proof assistant :P

@**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 ;)

@**pruvisto[m]**: Should be worth one paper at least

(it has happened before, can't recall whether it was 1 or 2 papers in the end)

@**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)

@**gr0n**: is there any way that one could bootstrap isabelle from the hg repository rather than downloading the pre-built binary for linux?

@**pruvisto[m]**: Yes

@**pruvisto[m]**: isabelle components -I

@**pruvisto[m]**: isabelle components -a

@**gr0n**: pruvisto[m]: yeah, but the URL that 2021 gets aren't accessible anymore

@**pruvisto[m]**: Run that on the development version and you're set

@**pruvisto[m]**: Ah

@**pruvisto[m]**: No that's probably not possible

@**pruvisto[m]**: Although

@**pruvisto[m]**: I'm actually surprised

@**pruvisto[m]**: Which component is the problem?

@**pruvisto[m]**: But why can't you run the regular Isabelle2021 release?

@**pruvisto[m]**: You shouldn't have to fetch any components for that

@**pruvisto[m]**: They're all bundled with it

@**pruvisto[m]**: The component fetching is only for the development version on mercurial

@**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

@**gr0n**: so i'm just trying to take the most barebones thing and bootstrap as much of isabelle as possible manually

@**pruvisto[m]**: Oof

you might be interested in https://github.com/nspin/nix-isabelle

@**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)

@**pruvisto[m]**: People then want support for that on the mailing list and it takes time to figure out what the problem is

@**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)

@**pruvisto[m]**: But of course I understand there are reasons for doing this

@**pruvisto[m]**: I don't know how long Makarius keeps the components on the server

@**gr0n**: also... it seems to be working now? i'm not sure why it wasn't a few minutes ago.

@**gr0n**: maybe i hit a weird timing

@**pruvisto[m]**: But I was under the impression that he does so pretty much indefinitely

@**pruvisto[m]**: For one, we sometimes like to go back to old versions to figure out regressions

@**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

@**pruvisto[m]**: For one, it will keeps its files in .isabelle

@**pruvisto[m]**: Not in .isabelle/Isabelle2021

@**gr0n**: hmm, so the preferred approach would be just to fetch the -linux tar.gz and distribute that?

@**pruvisto[m]**: And it will not display its name as Isabelle 2021 but as "unspecified repository version"

@**gr0n**: right, that sounds pretty... unacceptable to say the least :)

@**pruvisto[m]**: <gr0n "hmm, so the preferred approach w"> I would indeed recommend that if it is an option

@**gr0n**: pruvisto[m]: i think given a good enough a reason, it is.

@**gr0n**: and this seems like one

@**pruvisto[m]**: But Jakub seems to know a thing or two about packaging Isabelle

@**pruvisto[m]**: So if you prefer to look into alternatives, maybe have a look at the thing he linked

@**gr0n**: oh i totally missed that link... the @** caught me off guard and i thought it was another conversation :)

@**gr0n**: thnaks

@**pruvisto[m]**: No it's just the zulip bridge

@**pruvisto[m]**: That's what it looks like when someone writes on zulip

@**gr0n**: yeah, i see it now but completely glossed over it before :D

@**pruvisto[m]**: This big bundle is Makarius's solution to our very own dependency hell

@**pruvisto[m]**: It's not perfect, but it works very well for almost everyone

@**gr0n**: alright, that nix-isabelle thing is quite helpful. thanks for all the advice and information

@**int-e**: any opinions on the libera/freenode split?

@**pruvisto[m]**: Ugh

@**pruvisto[m]**: Yeah we should probably switch to libera

@**int-e**: ugh covers it well :-/

@**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.

@**int-e**: And of course there are other options... like OFTC, or giving up the IRC presence entirely (sniff)

I wouldn't have found the zulip without IRC, so...

@**aweinstock**: #haskell seems to be around halfway moved (~770 vs ~370 at the moment)

@**aweinstock**: well, existent in both places, so not exactly moved

@**int-e**: Note: It is now against Freenode policy to advertise libera.chat in the topic for project channels, and this is being enforced.

@**int-e**: #isabelle exists on irc.libera.chat does exist though in case anyone wants to meet up there.

@**int-e**: details (as of now, policies seem to be chaning every few hours): https://freenode.net/policies#channel-ownership

@**int-e**: this obviously doesn't mention Libera anywhere, but it's considered *spam*.

@**pruvisto[m]**: Libera does not have a Matrix bridge. :/

@**pruvisto[m]**: otherwise I'd happily vote for switching to that.

@**pruvisto[m]**: We are just moving another channel to oftc

@**pruvisto[m]**: A Matrix–Libera bridge is in progress, according to official information.

@**pruvisto[m]**: So I guess we should just move this thing to Libera and be done with it.

@**pruvisto[m]**: It's a damn shame Freenode had to go out like this.

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?

@**pruvisto[m]**: I don't know, but if it were that easy, they would already have done it.

@**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.

@**pruvisto[m]**: The problem, I think, is that the big Matrix bridges need some form of collaboration from the IRC side to work.

@**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.

The 'impersonation' feature where the bridge posts as many users with the [m] prefix might require collaboration

@**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.

@**pruvisto[m]**: So I guess the big Matrix bridges usually bundle these somehow, in circumvention of the "normal" IRC protocol

@**pruvisto[m]**: at least that's what I gather from half-overheard remarks

@**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

@**pruvisto[m]**: sigh

@**pruvisto[m]**: They're hoping to get the Matrix bridge on Libera up tomorrow

@**pie_**: -> libera

Just a test if the bridge to zulip works.

@**Guest8864**: works here.

@**int-e**: hi zulip

@**pruvisto**: Test?

@**pruvisto**: Ah okay it still works.

@**pruvisto**: And my name even appears as "pruvisto", not as "pruvisto[m]". Yay!

@**pruvisto**: int-e: Well I could take over the channel if you want me to.

@**pruvisto**: I haven't been op of an IRC channel since, uh, I don't know. Many years ago. :D

@**pruvisto**: But I could probably figure it out.

@**pruvisto**: I'm not terribly eager to do it, but if you're even less eager I'd happily do it.

@**int-e**: pruvisto: added you on chanserv. so /msg chanserv op #isabelle will work, for example.

@**pruvisto**: thanks

@**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."

@**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.

@**pruvisto**: I have no idea

@**pruvisto**: Perhaps they thought we don't know about the other one?

@**pruvisto**: We should put the information that this channel is bridged to zulip in the topic

@**int-e**: right, I took that out because it was false at the time

@**pruvisto**: fyi the word is "unofficial"

@**pruvisto**: "inofficial", if it exists at all, is very rare

@**pruvisto**: so you just outed yourself as a German speaker. ;)

@**int-e**: just giving you an incentife to try out those op powers ;)

@**int-e**: wow

@**int-e**: incentive.

@**int-e**: I need to wake up.

@**pruvisto**: incentife sounds like something a French person might write. :D

@**pruvisto**: In paper reviews you can often tell what country a person is from by the mistakes they make

@**pruvisto**: I once had a reviewer tell me "I was deceived by the presentation", presumable French because "décevoir" = "disappoint"

@**int-e**: that's an almost sinister shift in meaning

@**pruvisto**: There, I did it

@**int-e**: wee

@**pruvisto**: Who was op of the old Freenode channel anyway?

@**pruvisto**: Not sure how many regulars we lost in the move. And how many newbies.

@**pruvisto**: I guess I can advertise the channel on Twitter

@**pruvisto**: From the Isabelle account

@**pruvisto**: I wonder if we can somehow plumb a Matrix room to this one…

@**int-e**: pruvisto: larsh, Igloo, lispy, you, and I

@**pruvisto**: Me? Huh.

@**int-e**: Igloo founded it, I suspect because he wanted to formalize a darcs-like theory of patches.

@**int-e**: then I got ops from lispy one day and I looked for more active people actually involved in Isabelle :P

@**int-e**: And ended up picking larsh and you :P

@**aweinstock**: win move 12

@**aweinstock**: oops

@**int-e**: /lose :-)

@**safinaskar**: how to prove this? (case f a of True ⇒ Some (a # b) | False ⇒ None) = Some s ⟹ a # b = s

@**pruvisto1**: I would try `apply (auto split: option.splits)

@**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

@**pruvisto1**: uh, wait, in this case it's bool.splits

@**pruvisto1**: why are you using a case expression on booleans anyway, instead of just an "if"?

@**pruvisto1**: It's not wrong of course, but somewhat unusual

@**pruvisto1**: the splitting rule for "if" is called if_splits

@**safinaskar**: pruvisto1: thanks for answer

@**safinaskar**: pruvisto1: i simply used "try" and then copied suggested proof to source

@**safinaskar**: pruvisto1: is there a way to avoid copy? i. e. i want proof method which simply does same thing as "try"

@**pruvisto1**: I don't know what you mean by that

@**pruvisto1**: When "try" suggests something you can normally just click on it and it will copy it over

@**safinaskar**: pruvisto1: yes, but then my source will contain this unreadable proof

@**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

@**pruvisto1**: uh, no

@**pruvisto1**: that's probably a sledgehammer proof

@**pruvisto1**: they tend to be something like "apply (metis â€¦)" or "apply (smt â€¦)" where the â€¦ is a list of facts

@**pruvisto1**: they can get pretty big and ugly, that's why I try to avoid them

@**safinaskar**: pruvisto1: ok, thanks a lot

@**safinaskar**: is there a way to run two proof methods truly in parallel?

@**safinaskar**: i can write "by (auto|blast)"

@**safinaskar**: but it seems that this will run "auto" and if it fails, then blast

@**safinaskar**: how to run them actually in parallel?

@**safinaskar**: okey, maybe there is a way to run a proof method with a timeout?

@**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?

@**pruvisto1**: There's no such thing because that would ruin any chance of a reproducible build

@**pruvisto1**: There is the stuff by Yutaka Nagashima: https://github.com/data61/PSL

@**pruvisto1**: not sure if this runs in parallel but I think it does

@**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

@**pruvisto1**: I've never used it myself

@**safinaskar**: pruvisto1: thanks

@**sthaan**: hello :)

@**sthaan**: is there a lexicographical order over finite sets in Isabelle?

@**sthaan**: if no, how I can define an alternative "≤" order over "nat set" instead of the default subset relation "⊆"?

@**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.

@**pruvisto**: The former is always a bit annoying to do.

@**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

@**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)

@**pruvisto**: But usually the "locale interpretation" approach works pretty well for orderings

@**pruvisto**: Something like that is e.g. done for multisets, see ~~/src/HOL/Library/Multiset.thy, search for "global_interpretation subset_mset"

@**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

@**sthaan**: pruvisto, thank you very much for your detailed answer

@**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?

@**sthaan**: zfnmxt: foo[symmetric]

@**zfnmxt**: sthaan: Thanks. :)

@**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 _".

@**zfnmxt**: s/of an f/of an if-then-else expression

@**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?

@**sthaan**: zfnmxt, you just forgot a bracket:

@**sthaan**: https://upload.wiuwiu.de/share.php/1ec724eb-621c-497b-9636-c42c1a9292bd/20210909_00h19m31s_grim.png

@**zfnmxt**: sthaan: Ah, I see, thank you. :)

@**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?

subst _some_rule_ might help

@**pruvisto**: That does exactly one step

@**zfnmxt**: Perfect, that's what I wanted. Thanks.

@**pruvisto**: And it simply adds the preconditions as new goals

@**pruvisto**: Whereas simp tries to solve them and fails if it can't

@**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.

@**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

@**pruvisto**: there's also the "rewrite" method somewhere in the library that allows for more sophisticated things

@**pruvisto**: and there's "unfolding" which acts something like a "simp only: "

@**pruvisto**: (mostly used for unfolding definitions)

@**pruvisto**: zfnmxt: There's the Isabelle/Isar reference manual in the Isabelle documentation

@**pruvisto**: There's also https://tips.isabelle.systems

@**pruvisto**: e.g. https://isabelle.systems/cookbook/src/proofs/methods/

@**zfnmxt**: Aha, that's also helpful, thanks.

@**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?

@**sthaan**: zfnmxt, try `rule if_distrib`

instead of `simp only: if_distrib`

@**zfnmxt**: sthaan: What exactly does `rule`

do here?

@**sthaan**: sadly, I do not know why it works, I'm just a beginner myself

@**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.

@**zfnmxt**: Err, I realize now that `A <===> B => A = B?`

is nonsensical. But my question of how to prove equalities with just rules remains :)

@**int-e**: zfnmxt: what is <===>? There's <--> or âŸ·, but that's an abbreviation for =.

@**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.

@**zfnmxt**: Oh, I guess maybe I should just use `set_eq`

.

@**zfnmxt**: `set_eqI`

, sorry.

@**int-e**: yep

@**zfnmxt**: Why is <--> an abbreviation for =?

@**int-e**: Because it *is* equality on bools. Distinguishing between those notions would hinder rewriting.

@**zfnmxt**: Is there a rule that says `[A -> B; B -> A] => (A <-> B)`

?

@**int-e**: Maybe? iffI is more useful, beecause it gives you meta implications directly

@**zfnmxt**: Ah! `iffI`

is exactly what I want, I think :)

@**int-e**: There's also iff_conv_conj_imp for rewriting. Which I found by putting "_ ⟶ _" "(_ ⟷ _) = (_ ∧ _)" into the "find theorems" panel

@**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.

@**zfnmxt**: Oh, what you wrote is a union of queries. I didn't know you could do that. Neat.

@**zfnmxt**: How can you explicitly extend the set of intro (or elim) rules used by `proof`

(when no arguments are supplied)?

@**sthaan**: zfnmxt, I think by declaring your facts `[intro]`

or `[elim]`

@**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.

@**sthaan**: declare your_fact[intro]

@**zfnmxt**: sthaan: Ah, I misunderstood. I see. Thank you. :)

@**zfnmxt**: Looks like `declare your_face[rule del]`

removes it.

@**zfnmxt**: s/face/fact

@**sthaan**: Let's say I have a record type and some restrictions on it, like this:

@**sthaan**: ```

@**sthaan**: I now want to extend the record and add additional assumptions as well:

@**sthaan**: locale wf_point =

@**sthaan**: fixes pt :: point (structure)

@**sthaan**: assumes "x pt ≤ 100" "y pt ≤ 100"

@**sthaan**: ```

@**sthaan**: record point = x :: nat y ::nat

@**sthaan**: ```

@**sthaan**: datatype color = Brown | Blue | Violet | Purple | Green

@**sthaan**: record cpoint = point + col :: color

@**sthaan**: locale wf_cpoint =

@**pruvisto**: sthaan: Bit of a late response, but did you sort out your problem?

@**pruvisto**: I don't even see what your problem is – did your message perhaps get cut off?

@**sthaan**: pruvisto, looking at the logs it seems my message indeed was cut off after 11 lines.

@**sthaan**: here is the full question:

@**sthaan**: https://upload.wiuwiu.de/share.php/40b68d9a-a37f-4bae-b59f-4e9d44b16b29/message.txt

@**pruvisto**: Isabelle/HOL does not have subtyping

@**pruvisto**: So if you have something that wants a `point`

, you can't give it a `cpoint`

. That's a type error.

@**pruvisto**: Well, it does have… what is that called… parametric subtyping?

@**pruvisto**: So e.g. `nat list`

is a subtype of `'a list`

@**pruvisto**: and this is how record extension works in Isabelle/HOL

@**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`

@**pruvisto**: And then when you extend it to`cpoint`

, it puts the new stuff (and another `more`

field) into the `more`

of the `point`

@**pruvisto**: So with this knowledge, I think the way to fix your locales is to do `fixes pt :: "'a point_scheme"`

@**pruvisto**: Where the `'a`

has to be a fresh type variable (the name doesn't matter, Isabelle will normalise it anyway)

@**sthaan**: pruvisto, thanks this solves my problem I think. Here's my example file, if anyone is interested:

@**sthaan**: https://upload.wiuwiu.de/share.php/cbe2e5b3-40e2-4521-9d26-88bd61ba2b02/Records.thy

@**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)"`

@**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.

@**suhr[m]**: I'm new to Isar proofs as well. Things used to be much more straightforward in dependently typed languages...

@**sthaan**: suhr, in this case your goal can be solved with `by presburger`

@**suhr[m]**: Cool. But it's a lemma for an exercise in prog-prove, so this kind of proof is probably a bit overkill.

@**suhr[m]**: Also, I still want to lean how to use structured proofs in Isabelle.

@**sthaan**: you could also do it like this

@**sthaan**: ```isabelle

@**sthaan**: proof (intro exI)

@**sthaan**: lemma split_nat: "\<exists> x y. (n::nat) = x + y \<and> (x = y \<or> y = x + 1)"

@**sthaan**: let ?x = "n div 2"

@**sthaan**: let ?y1 = "n - ?x"

@**sthaan**: show "n = ?x + ?y1 ∧ (?x = ?y1 ∨ ?y1 = ?x + 1)" by auto

@**sthaan**: qed

@**sthaan**: ```

@**suhr[m]**: Thanks.

@**suhr[m]**: So even after let's, Isabelle shows the goal as `n = ?x + ?y1 ∧ (?x = ?y1 ∨ ?y1 = ?x + 1)`

.

@**suhr[m]**: And only after `show`

everything is substituted.

@**suhr[m]**: Well, I still have a problem applying this lemma.

@**suhr[m]**: sent a code block: https://libera.ems.host/_matrix/media/r0/download/libera.chat/dd1421bf9b8e5fbf2c2bccfab0b172249dbe4582

@**suhr[m]**: There's an error at `auto`

for some reason.

@**suhr[m]**: sent a code block: https://libera.ems.host/_matrix/media/r0/download/libera.chat/814bc07ed6459992521a964c09d87863018f1706

@**suhr[m]**: So close, and yet I still can't complete the goal because of ∃.

@**suhr[m]**: If I replace `have`

by show, I get `Result contains obtained parameters: ly`

@**suhr[m]**: Removing `(intro exI)`

and adding `show ?thesis by blast`

fixes the problem.

@**pruvisto**: <suhr[m]> "And only after `show`

everything..." <- Yes, the `let`

things are unnecessary

@**pruvisto**: they only introduce an abbreviation

@**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.

@**pruvisto**: You can also do something like `proof (rule exI[of _ "take ly xs"], rule exI[of _ "drop ly xs"])`

@**pruvisto**: And the thing you mentioned last is also a common pattern:

@**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`

@**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

@**sthaan**: I'm getting a lot of typing errors like this lately

@**sthaan**: https://upload.wiuwiu.de/share.php/945c7529-77a9-47aa-ac38-e69e1468eeaa/20211107_09h24m16s_grim.png

@**sthaan**: is there any way to see what type for `M`

is expected here?

@**sthaan**: it's Ctrl-Mouseover :)

@**pruvisto**: yup

@**pruvisto**: Another thing I occasionally do is `using [[unify_trace_failure]]`

@**pruvisto**: that shows you where exactly the unification fails

@**pruvisto**: can be a life saver if there's something subtle going on, like polymorphism

@**pruvisto**: or a big term where the only difference is that in one place there's a y instead of an x

@**pruvisto**: or a bound variable x instead of a free variable x

@**pruvisto**: Wait, in what context are you working on Turing machines?

@**sthaan**: pruvisto: thanks, I will try it out next time :)

@**sthaan**: we are trying to formalize a paper in complexity theory

@**pruvisto**: Who's "we"?

@**sthaan**: Guest6716 and me :)

@**pruvisto**: And are you students? Researchers? Sorry, just always curious when people do stuff in Isabelle.

@**pruvisto**: Also I know at least three different people/groups working on similiar stuff.

@**pruvisto**: You're either part of one of them or you ought to know about them ^^

@**sthaan**: we are grad students working part-time on this project (lead Stefan Rass):

@**sthaan**: https://www.syssec.at/en/projekte/cave-pnp

@**pruvisto**: Ah, I think somebody told me about that recently.

@**pruvisto**: I just moved to Innsbruck a few weeks ago

@**pruvisto**: In any case: Mohammad Abdulaziz and some of his colleagues and students at TUM are working on formalising various NP-complete algorithms

@**pruvisto**: I think they're using register machines though

@**pruvisto**: René Thiemann has two Bachelor's students working on Turing machines

@**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

@**sthaan**: > I just moved to Innsbruck a few weeks ago

@**sthaan**: Innsbruck is a really nice city, I lived there for two years :)

@**sthaan**: Thank you for the names, are they all using Isabelle?

@**pruvisto**: yes

@**pruvisto**: I think Mohammad might be most interesting to you

@**sthaan**: thank you, we will get in touch :)

@**sthaan**: Hi, I was wondering why interpretations are lost if I re-open a locale?

@**sthaan**: https://upload.wiuwiu.de/share.php/cbe7e62b-5619-47d7-a1b5-2f30ac2eae41/SavingInterpretation.thy

@**sthaan**: here the seconde `thm one_is_one`

fails because the interpretation of A is apparently lost

@**sthaan**: here the second `thm one_is_one`

fails because the interpretation of A is apparently lost

@**sthaan**: okay we could solve this by using `sublocale`

:)

@**sthaan**: https://upload.wiuwiu.de/share.php/1bcfc4b0-8f69-4123-89e7-c51c0e34b81e/SavingInterpretation.thy

@**pruvisto**: yup

@**pruvisto**: interpretations do not survive exiting the current context. sublocales do.

@**sthaan**: is it possible to introduce terms into a locale using only existence?

@**sthaan**: on the theory level I can use `consts`

and `specification`

to achieve this, but those are not allowed when I open a locale:

@**sthaan**: https://upload.wiuwiu.de/share.php/ae99725f-3265-486a-b3e7-406b0023a952/local_specification.thy

@**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

@**int-e**: It's more cumbersome though: definition x where "x == SOME x. x \<ge> 3" and then prove "x \<ge> 3" from that.

@**sthaan**: int-e, thanks I didn't think of that!

@**sthaan**: is there any other way to introduce terms from existence? I scared of `SOME`

@**sthaan**: int-e, thanks I didn't think of that!

@**sthaan**: is there any other way to introduce terms from existence? I'm scared of `SOME`

@**sthaan**: ok I guess if I never unfold the definition, I get the same results :)

@**int-e**: yes that's the idea

@**pruvisto**: "some" and "the" aren't that scary

@**pruvisto**: And the specification command probably uses them internally anyway

@**pruvisto**: But I would indeed try to keep the definition folded and just work with the derived properties

@**pruvisto**: The automation is not good at working with them

@**sthaan**: > "some" and "the" aren't that scary

@**sthaan**: yes if I never unfold anything they aren't that scary I guess :D

@**pruvisto**: They're a bit annoying to use, but otherwise…

@**pruvisto**: oh there's also "Least"

@**pie_**: has this been around http://math.andrej.com/2021/11/20/proof-assistants-stackexchange-site/

@**sthaan**: It's a pitty we can't have `instantiation nat :: floor_ceiling`

@**sthaan**: one would think floor and ceiling should be well defined for nat...

@**zfnmxt**: Does Isabelle have anything like haskell's "@" operator for binding a pattern to a variable? (e.g., myFun x@(Just k) = ...)

@**pruvisto**: Pattern aliases I think

@**pruvisto**: There's something in the library to do this

@**zfnmxt**: pruvisto: https://isabelle.in.tum.de/library/HOL/HOL-Library/Pattern_Aliases.html yep, thank you :)

@**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.

@**pruvisto**: the best way to do it is to do something like `show P3 using P2 P1 proof (induction …)`

@**pruvisto**: if the induction rule has n premises, the `induction`

method will unify the first n chained facts with them

@**pruvisto**: and any remaining chained facts are then simply treated as part of the statement being proved

@**pruvisto**: if that doesn't work you may have to post something more concrete

@**pruvisto**: so I can understand what the problem is

@**zfnmxt**: pruvisto: Thanks for your fast response. One sec, a bit of experimentation is in order!

@**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.

@**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?

@**pruvisto**: you mean an inductive predicate, right?

@**pruvisto**: this ain't Coq :D

@**pruvisto**: but yeah that looks right, for inductive predicates

@**pruvisto**: the "rules for the cases" bit is the interesting part though, of course

@**zfnmxt**: Yeah, that's what I meant. I learned with Coq so...I still try to frame everything through that :D

@**zfnmxt**: Thanks for your help again.

@**sthaan**: https://upload.wiuwiu.de/share.php/c3d4288a-ac64-4af1-9e7d-e04ca11ce27c/20220201_13h20m19s_grim.png

@**sthaan**: what could cause this "Bad number of arguments" error, but only the second time?

@**pruvisto**: huh

@**pruvisto**: I never quite understood how "(structure)" works though

@**pruvisto**: thatâ€¦ is an excellent question

@**sthaan**: removing `(structure)`

gives the same error :(

@**sthaan**: also if I remove the second locale definition, the error starts appearing on the first locale

Can you show a more complete example? Including at least the definition of TM?

@**pruvisto**: Oops, that was me on Zulip. :D

@**int-e**: Oh. The '@' is a bit unfortunate.

My guess would be that the name `foo_TM`

is already used internally somewhere, leading to the problem you observe.

@**pruvisto**: Not sure why it does that. But what is the problem?

@**sthaan**: `foo_TM`

is not used anywhere else and a quick `grep -ri "foo_TM" /opt/Isabelle2021-1/src/`

also gives no result

unless foo_TM is generated as a name bei some package

@**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.

@**sthaan**: AHA! I found the problem: It was in a comment below

@**sthaan**: Here's a minimal example

@**sthaan**: https://upload.wiuwiu.de/share.php/79c53277-5393-479f-a5c8-c1b216ad0e50/Test.thy

@**int-e**: pruvisto: It clashes with the convention of using `@`

for addressing people (indicating a target, rather than a source).

@**sthaan**: Replacing `typ>‹('a) R›`

with `typ>‹('a, 'b) R›`

in the comment fixes the error

@**pruvisto**: sthaan: Ah, so the error came from the typ antiquotation

@**sthaan**: this is quite confusing as it breaks my intuition about where to look:

@**sthaan**: * stuff below can't cause an error further up

@**sthaan**: * comments do not matter

@**pruvisto**: These kinds of comments are not comments like when you "comment something out" in Java

@**pruvisto**: These comments are part of the formal proof document, so they are also checked (namely for type-correctness)

@**pruvisto**: there are also the (* foo *) comments, which, to my knowledge, are not checked in any way

@**pruvisto**: (they can, however, still cause "errors" occasionally because extremely long comments can mess with the parser in Isabelle/jEdit)

@**sthaan**: still the error should have been shown on the antiquotation, not on the definition further up ðŸ¤”ï¸�

@**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

@**pruvisto**: however, why this happens in this particular case, I have no idea

@**pruvisto**: I don't think it should

@**pruvisto**: feel free to send this to the mailing list

@**pruvisto**: I think Makarius does care about errors showing up in the right place

@**sthaan**: ok, thank you, I will send this example to the mailing list :)

@**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?

@**pruvisto**: No but it might be waiting for moderator approval

@**sthaan**: hm, I did not get any conformation that my message is subject to moderator approval ...

@**pruvisto**: hm, it is odd that it still didn't go through

@**pruvisto**: the address that I use is cl-isabelle-users@lists.cam.ac.uk

@**pruvisto**: not sure if yours works as well

@**sthaan**: I got the address from https://isabelle.in.tum.de/ where it is shown without the `cl-`

@**pruvisto**: yeah maybe it's just an alias

@**sthaan**: ok, i've sent it to cl-isabelle-users@lists.cam.ac.uk too now, let's see if it goes through

@**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:

@**sthaan**: I got no mails indicating what the error could have been...

@**sthaan**: any ideas what I could do about it?

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

@**sthaan**: thank you, I will try that :smile:

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.

@**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.

@**pruvisto**: Urgh

@**pruvisto**: Sorry about that bad experience.

@**sthaan**: no need to be! we figured it out in the end, thank you for all the help :)

@**sthaan**: but there might be other people whose mails have also been silently deleted

@**sthaan**: is there a good way to stop blast from executing while I'm typing somewhere in the document?

@**sthaan**: If I'm rewriting something the proof below needs, blast starts, doesn't find anything and uses up all CPU

@**pruvisto**: I usually just comment it out and replace it with a sorry

@**sthaan**: okay, i see, I'm doing something similar, but I thought maybe there's a better way to stop checking the document temporariliy

Isn't there a switch to turn off continuous checking, cf 3.1.2 here https://isabelle.in.tum.de/dist/doc/jedit.pdf

@**sthaan**: Kevin Kappelmann, thank you, this works without commenting out stuff :)

@**TheHermann**: hi, where i can find tutorial for first order logic in Isabelle?. I checked the official site but i didnt found useful tutorial.

@**sthaan**: TheHermann, I think first order propositions can often be solved by means like `blast`

, `auto`

, ...

@**sthaan**: What are you looking to prove?

@**TheHermann**: sthaan, an security protocol with first order logic

@**TheHermann**: but i dont undestand how use first order logic in Isabelle

@**TheHermann**: hi

@**TheHermann**: how use first order logic in Isabelle?

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

@**TheHermann**: isabelle_zulip_, i want to prove things about first order logic

@**TheHermann**: I have to try to write the public key Needham-Schroeder protocol in FOL. but I didn't understand Isabelle's syntax.

You should read a tutorial, for example this one: https://isabelle.in.tum.de/dist/Isabelle2021-1/doc/prog-prove.pdf

@**TheHermann**: ok...i try to read this tutorial thanks :). im new in Isabelle

@**TheHermann**: are there any examples of protocols written in fol?

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?

@**TheHermann**: how write axiom like A send B the message A,B in Isabelle?

@**TheHermann**: in FOL

@**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.

@**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.

@**TheHermann**: I have to use FOL, but i dont undestand how write functions and predicares in Isabelle

@**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

@**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.

@**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).

@**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

@**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

@**aweinstock**: (they both involve encodings of computable functions and the plumbing to network them)

@**TheHermann**: thanks for the replies

@**TheHermann**: I go to sleep, night!!

@**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 ?.

@**TheHermann**: how works functions on Isabelle? is https://pastebin.com/P5nm68qc functions or predicate?

@**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

Of course. How that looks exactly depends on whether you're using Isar or tactic-style proofs.

In Isar it's something like have "a = b" using mylemmy by some_proof_method

*mylemma

in tactic-style proofs it's… well actually exactly the same, also with "using"

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).

(or Isabelle/FOL in your case I guess)

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.

@**TheHermann**: hi

@**TheHermann**: how compare two predicate in isabelle?

@**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

@**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...

@**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

@**sthaan**: hi, how would you go about contributing lemmas to the standard library?

@**sthaan**: is there any policy about what is 'interesting enough' to qualify?

Not really. It has to be of sufficient general interest.

So if it's something fairly basic about lists, multisets, numbers, analysis, etc. that probably belongs in the algebra.

If it's something interesting but big enough to be packaged in an AFP entry, an AFP entry is probably a better choice.

Feel free to post something here and I can tell you what my opinion is.

@**sthaan**: for example this

@**sthaan**: ```isabelle

@**sthaan**: lemma ae_word_length_iff[iff]:

@**sthaan**: fixes P :: "'s::finite list ⇒ bool"

@**sthaan**: shows "Alm_all P ⟷ (∃n. ∀w. n ≤ length w ⟶ P w)"

@**sthaan**: ```

@**sthaan**: ```isabelle

@**sthaan**: lemma finite_imp_inj_to_nat_fix_one:

@**sthaan**: fixes A::"'a set" and x::'a and y::nat

@**sthaan**: assumes "finite A"

@**sthaan**: shows "∃g. inj_on g A ∧ g x = y"

@**sthaan**: ```

@**sthaan**: ```isabelle

@**sthaan**: lemma nat_strict_mono_greatest:

@**sthaan**: fixes f::"nat ⇒ nat" and N::nat

@**sthaan**: assumes "strict_mono f" "f 0 ≤ N"

@**sthaan**: obtains n where "f n ≤ N" and "∀m. f m ≤ N ⟶ m ≤ n"

@**sthaan**: ```

Hmm I don't know, these seem a bit too specific for my taste.

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 ∞)

Thus there exists some number `n`

such that `f n > N`

, and thus there also exists a least `n`

such that `f n > N`

.

Doing it that way the proof shouldn't be more than like 5 lines or so.

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 → ℕ"

in that form one could potentially think of adding it to the library (if it doesn't already exist there in a similar form)

(of course this could be generalised even further, but then one has to talk about cardinalities.)

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"

err, f : B → C at the end there

actually g : B → C

apparently COVID is eating away my brain

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)

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.

@**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`

.

@**sthaan**: Yes, but this is not the conclusion of nat_strict_mono_greatest?

Okay well you still have to subtract 1 I guess.

Or you just use the `GREATEST`

operator instead.

Should also work.

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`

)

@**sthaan**: yes, that's kind of how we proved it :)

@**sthaan**: https://upload.kikeriki.at:5281/file_share/CyLYWnTQcroiClZP2sqgb_Rf/nat_strict_mono_greatest.txt

@**sthaan**: ok this file got mangled somehow (?)

@**sthaan**: https://upload.kikeriki.at:5281/file_share/V1QOjCVk71LJno_MLPvxp7Ex/nat_strict_mono_greatest.txt

@**sthaan**: ok the proof for `finite_imp_inj_to_nat_fix_one`

for countable A is probably kind of lengthy...:

@**sthaan**: https://upload.kikeriki.at:5281/file_share/4iltzEL5YrsLohGfv2NuhMWv/Contrib.thy

@**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

@**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!

I think a list to its reverse behave similar to # to snoc :)

@**rawburt**: thanks! i'll poke around some more

To expand a bit more on this: a common approach with these problems is to see where the simplifier gets stuck.

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.

The situation here is probably similar, just with lmax and snoc.

@**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 :)

@**rawburt**: i appreciate all the pointers and feedback

Well if you need further hints feel free to ask.

The learning curve for theorem provers is pretty horrible.

@**rawburt**: yes it is, ha!

@**rawburt**: but that's part of the fun... and the pain

Last updated: Jun 07 2023 at 02:54 UTC