[Merged by Bors] - feat(miu_language): a formalisation of the MIU language described by D. Hofstadter in "Gödel, Escher, Bach". #3739
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Hofstadter in "Gödel, Escher, Bach". We show that a string `en` in the language is derivable if and only if it satisfies `decstr en`, where `decstr` is a simple predicate that 'should' be decidable. However, we do not _prove_ decidability.
semorrison
reviewed
Aug 11, 2020
semorrison
reviewed
Aug 11, 2020
semorrison
reviewed
Aug 11, 2020
semorrison
reviewed
Aug 11, 2020
semorrison
reviewed
Aug 11, 2020
semorrison
reviewed
Aug 11, 2020
semorrison
reviewed
Aug 11, 2020
semorrison
reviewed
Aug 11, 2020
semorrison
reviewed
Aug 11, 2020
semorrison
reviewed
Aug 11, 2020
semorrison
reviewed
Aug 11, 2020
semorrison
reviewed
Aug 11, 2020
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
This reverts commit cc3fcb2.
robertylewis
added
the
awaiting-author
bryangingechen
changed the title
semorrison
added
awaiting-review
The new definition dispenses with `∃` and thereby facilitates automatic derivation of `decidable_pred decstr`.
…emises `l ≠ nil` Three results. The first states: if `count a = length l`, then `repeat a (count a l) = l`. The second states: if `l ≠ nil`, then `tail (l ++ [a]) = tail l ++ [a]`, if `l ≠ nil`. The last states: if `l ≠ nil`, then `∃ b L, l = b :: L`.
|
Can you mark as |
Remove three lemmas from `decision_nec` and `decision_suf`, having added them to `/src/data/list/basic.lean` in a previous commit.
gihanmarasingha
added
the
awaiting-review
bryangingechen
removed
the
awaiting-author
robertylewis
added
awaiting-author
* Use `derive` rather than explicit derivation of typeclass in `basic.lean` * Ensure all remaining goals are presented in indented blocks. * Eliminate nonterminal use of `simp`, replace with `simp only`.
gihanmarasingha
added
the
awaiting-review
bryangingechen
removed
the
awaiting-author
|
I think this is looking great. Since it's a big PR, I won't merge immediately to see if there are more comments. But I'm satisfied :) |
jcommelin
reviewed
Aug 18, 2020
There was a problem hiding this comment.
Sometimes there are multiple empty lines following each other... I would just use 1 empty line in those cases. @robertylewis what do you think?
@gihanmarasingha Thank you so much for writing this! It looks great!
Co-authored-by: Johan Commelin <johan@commelin.net>
Thanks all so much for the invaluable review suggestions. The code is so much better and I've become more proficient in Lean (and Git) through the process. |
github-actions
bot
added
ready-to-merge
bors bot
pushed a commit
that referenced
this pull request
Aug 18, 2020
…D. Hofstadter in "Gödel, Escher, Bach". (#3739) We define an inductive type `derivable` so that `derivable x` represents the notion that the MIU string `x` is derivable in the MIU language. We show `derivable x` is equivalent to `decstr x`, viz. the condition that `x` begins with an `M`, has no `M` in its tail, and for which `count I` is congruent to 1 or 2 modulo 3. By showing `decidable_pred decstr`, we deduce that `derivable` is decidable.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
We define an inductive type
derivableso thatderivable xrepresents the notion that the MIU stringxis derivable in the MIU language. We showderivable xis equivalent todecstr x, viz. the condition thatxbegins with anM, has noMin its tail, and for whichcount Iis congruent to 1 or 2 modulo 3.By showing
decidable_pred decstr, we deduce thatderivableis decidable.