MIU formal system

Stream: general

[Gihan Marasingha]

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]

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]

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]

(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]

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]

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

[Yury G. Kudryashov]

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

[Gihan Marasingha]

Thanks for the comments!

[Mario Carneiro]

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]

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

[Mario Carneiro]

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]

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]

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

[Gihan Marasingha]

Thanks!

[Bryan Gin-ge Chen]

archive/miu_language sounds like a good place

[Yury G. Kudryashov]

archive/miu_language looks like a good choice.

[Gihan Marasingha]

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]

You can use relative imports import .foo

[Scott Morrison]

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

[Gihan Marasingha]

Thanks @Scott Morrison! It works now.

[Gihan Marasingha]

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

[Gihan Marasingha]

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

[Gihan Marasingha]

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]

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]

Thanks!

[Gihan Marasingha]

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

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]

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

[Gihan Marasingha]

Thanks Kevin!

[Kevin Buzzard]

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

[Gihan Marasingha]

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]

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]

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