Stream: General

Topic: conditinoal comprehension rewriting

Matthew Pocock (Aug 30 2023 at 21:41):

Hi - I have this expression within a goal:

{if even n then (n, n div 2) else (n, 3 * n + 1) |n. True}

I would like to convince the proof to rewrite this as the union of two set comprehensions:

{(n, n div 2)|n. even n} \<union> {(n, 3*n+1|n. \<not> even n}

I have a lemma that proves this is safe in the general case:

lemma union_comprehension: "{if T then p else q| x. U} = ({p | x. U \<and> T} \<union> {q| x. U \<and> \<not> T})"
    apply auto
done

However, I have tried apply (subst union_comprehension) and similar things, but it isn't able to progress anything. I did try to rewrite this rule as a fun but couldn't figure it out.

Thanks.

Matthew Pocock (Aug 30 2023 at 21:52):

And of course within moments of posting, after an hour of scratching my head, I got it working. I had to make union_comprehension much more specific to get it to unify.

lemma union_comprehension:
    "{if T x then p x else q x| x. U x} =
        ({p x | x. U x \<and> T x} \<union> {q x| x. U x \<and> \<not> T x})"
    apply auto
done

I do have a genuine follow-up question though. I'm writing a few of these lemmas that only exist to guide another proof. Is there any way to introduce them within the proof that they are used in? As sort of in-line once-off rules?

Wolfgang Jeltsch (Aug 30 2023 at 22:04):

You should really switch to using Isar. Not only allows it to introduce these “local lemmas”; it also allows for much more readable proofs.

Matthew Pocock (Aug 30 2023 at 22:18):

Wolfgang Jeltsch said:

You should really switch to using Isar. Not only allows it to introduce these “local lemmas”; it also allows for much more readable proofs.

OK. Thanks. I guess that's my "next thing" :D and will probably be a good excuse to tidy what I've got so far.

Matthew Pocock (Aug 30 2023 at 23:15):

Wolfgang Jeltsch said:

You should really switch to using Isar. Not only allows it to introduce these “local lemmas”; it also allows for much more readable proofs.

What should I look at to learn isar? I have been working through https://isabelle.in.tum.de/doc/tutorial.pdf but it isn't really helping me to write proofs in isar.

Yutaka Nagashima (Aug 31 2023 at 00:04):

Matthew Pocock said:

Wolfgang Jeltsch said:

You should really switch to using Isar. Not only allows it to introduce these “local lemmas”; it also allows for much more readable proofs.

What should I look at to learn isar? I have been working through https://isabelle.in.tum.de/doc/tutorial.pdf but it isn't really helping me to write proofs in isar.

Part I, Section 5 of Concrete Semantics?
http://concrete-semantics.org

Mathias Fleury (Aug 31 2023 at 05:03):

For the original question: the issue is that you have the mark the dependencies in x, so:

lemma union_comprehension: "{if T x then p x else q x| x. U x} = ({p x | x. U x \<and> T x} \<union> {q x| x. U x \<and> \<not> T x})"
    apply auto
done

lemma ‹A = {if even n then (n, n div 2) else (n, 3 * n + 1) |n. True}›
  apply (subst union_comprehension)

Wolfgang Jeltsch (Aug 31 2023 at 17:04):

Matthew Pocock said:

What should I look at to learn isar? I have been working through https://isabelle.in.tum.de/doc/tutorial.pdf but it isn't really helping me to write proofs in isar.

I think that’s the old tutorial. The best way of getting into Isabelle, in my opinion, is the prog-prove tutorial, which is the very first piece of documentation listed on the documentation page of the Isabelle website and in the documentation panel of Isabelle/jEdit. From what I understand, it is a large excerpt from the first chapter of Concrete Semantics; so when @Yutaka Nagashima suggested to look at Part I, Section 5 of Concrete Semantics, he essentially suggested to look at Section 4 of the prog-prove tutorial. :smile:

Wolfgang Jeltsch (Aug 31 2023 at 17:11):

It happened several times recently that newcomers were looking at the old tutorial instead of prog-prove. I wonder why that is, given that prog-prove is listed first on the website and in Isabelle/jEdit and the old tutorial is listed under “Old Isabelle Manuals”. Do people just do a web search for “Isabelle tutorial” and find the old tutorial this way? @Matthew Pocock, how did you arrive at the old Isabelle tutorial?

Mathias Fleury (Aug 31 2023 at 17:18):

If I was a beginner, I would probably also start with the tutorial, because it seems to be the best place to start ("Programming and Proving" does not really sound like an introduction)

Wolfgang Jeltsch (Aug 31 2023 at 17:20):

Hmm, it’s Programming and Proving in Isabelle/HOL, which sounds to me like it would give a good overview about Isabelle/HOL. :man_shrugging:

Mathias Fleury (Aug 31 2023 at 17:22):

true, but if I think of programming in Isabelle, I mostly think of ML, but… I don't really know

Matthew Pocock (Aug 31 2023 at 20:26):

Wolfgang Jeltsch said:

It happened several times recently that newcomers were looking at the old tutorial instead of prog-prove. I wonder why that is

I hit the old tutorial both from google, and also perhaps google takes you to an older isabelle documentation page? Each time I googled for a tutorial and followed the links or the pages, it took me to the old tutorial. This is the first time I am seeing the prog-prove tutorial, and only because I added prog-prove into the google search term. It may be the first time google took me to the 2021 isabelle documentation page.

Wolfgang Jeltsch (Aug 31 2023 at 21:05):

The prog-prove tutorial has been in existence for a long time; so, even if you’re taken to, say, the Isabelle2021 documentation page, you should find it. What I can imagine is that, if you google for “Isabelle tutorial”, you are taken to the document that runs under the short name “Isabelle tutorial” but is unfortunately the outdated document.

Last updated: May 02 2024 at 01:06 UTC