Zulip Chat Archive

Stream: general

Topic: MIU formal system


Gihan Marasingha (Jul 22 2020 at 19:16):

Thanks to all the excellent documentation out there, I've felt confident enough to try formalising a little system in Lean. I chose the MIU formal system, as described in Douglas Hofstadter's book Gödel, Escher, Bach.

Using Lean, I proved that a particular typographical condition on strings gives a decision procedure for derivability. I'm sure the code is rough around the edges and could be much improved, but it works!

The MIU project is on GitHub. Any thoughts or feedback from experienced Leaners (if that's the right word) are much appreciated!

Dan Stanescu (Jul 22 2020 at 20:00):

I'm not an experienced Leaner but I'd like to suggest that this go into mathlib/archive. Or any other community place a more experienced Leaner finds appropriate.

Scott Morrison (Jul 22 2020 at 23:48):

I agree!

We generally have pretty high standards for archive --- if material coming into mathlib isn't considered "relevant enough" to go in the main library (i.e. it's unlikely to ever be reused), then it has to have good pedagogical value. I've only looked at this code briefly, but it does look nicely done, so getting it through a PR into archive seems quite plausible.

Scott Morrison (Jul 22 2020 at 23:49):

(The advantages are: 1. hopefully you learn useful things by surviving a PR process, (and we try to be friendly) 2. it means the material won't bitrot away as Lean progresses, 3. it contributes useful material for new users to learn from.)

Yury G. Kudryashov (Jul 23 2020 at 06:01):

Looking at https://github.com/gihanmarasingha/miu_language/blob/master/src/arithmetic.lean : a good general way to do this is to prove ∃ᶠ n in at_top, 2^(n:nat) ≡ 1 [MOD 3] and similarly for 2 [MOD 3]. Then you get the rest from tendsto (pow 2) (at_top : filter nat) at_top.

Yury G. Kudryashov (Jul 23 2020 at 06:01):

(and general lemmas about filter.eventually, filter.frequently, and filter.at_top).

Yury G. Kudryashov (Jul 23 2020 at 06:02):

And the lemma about pow follows from ∃ᶠ n in at_top, n ≡ a [MOD b].

Gihan Marasingha (Jul 28 2020 at 23:26):

Thanks for the comments!

Mario Carneiro (Jul 28 2020 at 23:29):

How about presenting this theorem as a proof of decidable_rel derivable, by proving it is equivalent to decstr (without defining decstr directly)?

Mario Carneiro (Jul 28 2020 at 23:30):

that way you can just #eval to_bool (derivable "MU") and get ff

Mario Carneiro (Jul 28 2020 at 23:38):

Also your derivable relation can be more clearly written like

inductive derivable : miustr  Prop
| mk : derivable "MI"
| r1 {x} : derivable (x ++ [I])  derivable (x ++ [I, U])
| r2 {x} : derivable (M :: x)  derivable (M :: x ++ x)
| r3 {x y} : derivable (x ++ [I, I, I] ++ y)  derivable (x ++ U :: y)
| r4 {x y} : derivable (x ++ [U, U] ++ y)  derivable (x ++ y)

Gihan Marasingha (Aug 07 2020 at 21:11):

I still need to learn more about filters before I can implement @Yury G. Kudryashov 's suggestion. I haven't yet made @Mario Carneiro's suggested change. Perhaps I should just make a PR to the mathlib archive and do required changes through code review before my teaching and admin overwhelms me.

So, as per your LFTCM2020 video, @Scott Morrison , can I ask someone to give me permission to push a branch?

Also, where precisely should I ask for this to live? Should it go in (say) mathlib/archive/miu_language ? The directory structure of archive isn't clear to me.

Bryan Gin-ge Chen (Aug 07 2020 at 21:12):

I've sent you an invitation: https://github.com/leanprover-community/mathlib/invitations

Gihan Marasingha (Aug 07 2020 at 21:13):

Thanks!

Bryan Gin-ge Chen (Aug 07 2020 at 21:13):

archive/miu_language sounds like a good place

Yury G. Kudryashov (Aug 07 2020 at 21:13):

archive/miu_language looks like a good choice.

Gihan Marasingha (Aug 11 2020 at 10:08):

Slightly annoying issue: I've cloned mathlib and put my files in archive/miu_language, but I can't import (say) the file basic.lean in this directory to other files in the same directory as archive isn't in the lean path.

Is there a way to import files that aren't in the path or to modify the path? If not, I can just put everything in one big file.

Scott Morrison (Aug 11 2020 at 10:11):

You can use relative imports import .foo

Scott Morrison (Aug 11 2020 at 10:11):

This isn't allowed in the src/ directory, but I guess is the right plan in archive/.

Gihan Marasingha (Aug 11 2020 at 10:11):

Thanks @Scott Morrison! It works now.

Gihan Marasingha (Aug 11 2020 at 11:07):

Ah, I'm afraid committing the @derive suggestion broke things. How do I go back and fix it? @Scott Morrison. Thanks!

Gihan Marasingha (Aug 11 2020 at 11:15):

Never mind, I think I've reverted successfully, but still not sure how to use @derive in this case.

Gihan Marasingha (Aug 11 2020 at 16:11):

Sorry more git noob question: when making edits as per the review suggestions, should I only commit the changes via the github interface or can I make them locally and push?

Doing it via github doesn't allow me to check whether the edits work but making the changes locally presumably doesn't allow the commits to be registered as a response to the review.

Thanks.

Bryan Gin-ge Chen (Aug 11 2020 at 16:13):

Either is fine. If you make the changes locally, just remember to add replies to and / or "resolve" the comments that you addressed.

Gihan Marasingha (Aug 11 2020 at 16:14):

Thanks!

Gihan Marasingha (Aug 12 2020 at 13:28):

@Scott Morrison thanks for the really useful review feedback. I'm especially happy that your suggestion of removing in the goodm definition has enabled me to prove decidable_pred derivable, as per @Mario Carneiro's idea.

As the code has substantially changed since original PR, should I cancel the PR and create a new one or can the review process continue as it is?

Kevin Buzzard (Aug 12 2020 at 13:48):

github should be able to handle this fine. Make the changes on your local miu branch and push, and everything should just work fine -- old comments will be marked as resolved etc

Kevin Buzzard (Aug 12 2020 at 13:49):

Only if I'm wrong and for some reason gh is a mess should you make a new PR, is my instinct.

Gihan Marasingha (Aug 12 2020 at 13:50):

Thanks Kevin!

Kevin Buzzard (Aug 12 2020 at 14:00):

I'm reviewing it now. Did you just do this for fun or are you planning on using it for teaching?

Gihan Marasingha (Aug 12 2020 at 14:17):

Just for fun.

But due to the popularity of _Gödel, Escher, Bach_, this project might be also be good for spread the good word among the nerd community. I'd be happy to write something up if that seems sensible. I've previously written popular articles for _Mathematics Today_, the IMA's newsletter.

Kevin Buzzard (Aug 12 2020 at 16:33):

I am increasingly of the opinion that there's something here for the math nerd community if only we can figure out how to deliver it to them. You can turn what you have into a playable game where people can experiment with making various strings. If you host it on CoCalc then people won't even need to install lean. You could make some simple levels and then give them the statements of some of the theorems you've proved and get them to prove other ones as long as the argument is relatively straightforward. The goal should be to convince people they're proving theorems even though you've done the hard work behind the scenes

Kevin Buzzard (Aug 12 2020 at 16:34):

Like me you have access to a huge number of undergraduates and the more toys we can offer them the better


Last updated: Dec 20 2023 at 11:08 UTC