Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-18 20:22 5d2256da

View on Github →

feat(miu_language): a formalisation of the MIU language described by 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.

Estimated changes

added inductive miu.derivable
added inductive miu.miu_atom
added def miu.miustr.mrepr
added def miu.miustr
added def miu.decstr
added theorem miu.decstr_of_der
added def miu.goodm
added theorem miu.goodm_of_derivable
added theorem miu.goodm_of_rule1
added theorem miu.goodm_of_rule2
added theorem miu.goodm_of_rule3
added theorem miu.goodm_of_rule4
added theorem miu.goodmi
added theorem miu.not_derivable_mu
added theorem miu.add_mod2
added theorem miu.base_case_suf
added theorem miu.der_of_decstr
added theorem miu.ind_hyp_suf