Commit 2023-02-15 04:21 16ba0275

View on Github →

feat: port Computability.TuringMachine (#2125)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Computability/TuringMachine.lean

added def Turing.BlankExtends.above

added theorem Turing.BlankExtends.above_of_le

added theorem Turing.BlankExtends.below_of_le

added theorem Turing.BlankExtends.refl

added theorem Turing.BlankExtends.trans

added def Turing.BlankExtends

added def Turing.BlankRel.above

added def Turing.BlankRel.below

added theorem Turing.BlankRel.equivalence

added theorem Turing.BlankRel.refl

added def Turing.BlankRel.setoid

added theorem Turing.BlankRel.symm

added theorem Turing.BlankRel.trans

added def Turing.BlankRel

added inductive Turing.Dir

added def Turing.FRespects

added def Turing.ListBlank.append

added theorem Turing.ListBlank.append_assoc

added theorem Turing.ListBlank.append_mk

added def Turing.ListBlank.bind

added theorem Turing.ListBlank.bind_mk

added def Turing.ListBlank.cons

added theorem Turing.ListBlank.cons_bind

added theorem Turing.ListBlank.cons_head_tail

added theorem Turing.ListBlank.cons_mk

added theorem Turing.ListBlank.exists_cons

added theorem Turing.ListBlank.ext

added def Turing.ListBlank.head

added theorem Turing.ListBlank.head_cons

added theorem Turing.ListBlank.head_map

added theorem Turing.ListBlank.head_mk

added def Turing.ListBlank.map

added theorem Turing.ListBlank.map_cons

added theorem Turing.ListBlank.map_mk

added theorem Turing.ListBlank.map_modifyNth

added def Turing.ListBlank.mk

added def Turing.ListBlank.modifyNth

added def Turing.ListBlank.nth

added theorem Turing.ListBlank.nth_map

added theorem Turing.ListBlank.nth_mk

added theorem Turing.ListBlank.nth_modifyNth

added theorem Turing.ListBlank.nth_succ

added theorem Turing.ListBlank.nth_zero

added def Turing.ListBlank.tail

added theorem Turing.ListBlank.tail_cons

added theorem Turing.ListBlank.tail_map

added theorem Turing.ListBlank.tail_mk

added def Turing.ListBlank

added theorem Turing.PointedMap.headI_map

added theorem Turing.PointedMap.map_pt

added theorem Turing.PointedMap.mk_val

added structure Turing.PointedMap.{u,

added theorem Turing.Reaches.to₀

added def Turing.Reaches

added theorem Turing.Reaches₀.head

added theorem Turing.Reaches₀.refl

added theorem Turing.Reaches₀.single

added theorem Turing.Reaches₀.tail'

added theorem Turing.Reaches₀.tail

added theorem Turing.Reaches₀.trans

added def Turing.Reaches₀

added theorem Turing.Reaches₁.to₀

added def Turing.Reaches₁

added def Turing.Respects

added def Turing.TM0.Cfg.map

added structure Turing.TM0.Cfg

added def Turing.TM0.Machine.map

added theorem Turing.TM0.Machine.map_respects

added theorem Turing.TM0.Machine.map_step

added def Turing.TM0.Machine

added def Turing.TM0.Reaches

added def Turing.TM0.Stmt.map

added inductive Turing.TM0.Stmt

added def Turing.TM0.Supports

added def Turing.TM0.init

added theorem Turing.TM0.map_init

added def Turing.TM0.step

added theorem Turing.TM0.step_supports

added theorem Turing.TM0.univ_supports

added def Turing.TM0to1.tr

added def Turing.TM0to1.trCfg

added theorem Turing.TM0to1.tr_respects

added inductive Turing.TM0to1.Λ'

added structure Turing.TM1.Cfg

added inductive Turing.TM1.Stmt

added def Turing.TM1.Supports

added def Turing.TM1.SupportsStmt

added def Turing.TM1.init

added def Turing.TM1.step

added def Turing.TM1.stepAux

added theorem Turing.TM1.step_supports

added theorem Turing.TM1.stmts_supportsStmt

added theorem Turing.TM1.stmts_trans

added theorem Turing.TM1.stmts₁_self

added theorem Turing.TM1.stmts₁_supportsStmt_mono

added theorem Turing.TM1.stmts₁_trans

added def Turing.TM1to0.tr

added def Turing.TM1to0.trAux

added def Turing.TM1to0.trCfg

added theorem Turing.TM1to0.tr_eval

added theorem Turing.TM1to0.tr_respects

added theorem Turing.TM1to0.tr_supports

added def Turing.TM1to0.Λ'

added theorem Turing.TM1to1.exists_enc_dec

added def Turing.TM1to1.move

added def Turing.TM1to1.read

added def Turing.TM1to1.readAux

added theorem Turing.TM1to1.stepAux_move

added theorem Turing.TM1to1.stepAux_read

added theorem Turing.TM1to1.stepAux_write

added theorem Turing.TM1to1.supportsStmt_move

added theorem Turing.TM1to1.supportsStmt_read

added theorem Turing.TM1to1.supportsStmt_write

added def Turing.TM1to1.tr

added def Turing.TM1to1.trCfg

added def Turing.TM1to1.trNormal

added def Turing.TM1to1.trTape'

added theorem Turing.TM1to1.trTape'_move_left

added theorem Turing.TM1to1.trTape'_move_right

added def Turing.TM1to1.trTape

added theorem Turing.TM1to1.trTape_mk'

added theorem Turing.TM1to1.tr_respects

added theorem Turing.TM1to1.tr_supports

added def Turing.TM1to1.write

added inductive Turing.TM1to1.Λ'

added structure Turing.TM2.Cfg

added def Turing.TM2.Reaches

added inductive Turing.TM2.Stmt

added def Turing.TM2.Supports

added def Turing.TM2.SupportsStmt

added def Turing.TM2.init

added def Turing.TM2.step

added def Turing.TM2.stepAux

added theorem Turing.TM2.step_supports

added theorem Turing.TM2.stmts_supportsStmt

added theorem Turing.TM2.stmts_trans

added theorem Turing.TM2.stmts₁_self

added theorem Turing.TM2.stmts₁_supportsStmt_mono

added theorem Turing.TM2.stmts₁_trans

added inductive Turing.TM2to1.StAct

added inductive Turing.TM2to1.TrCfg

added def Turing.TM2to1.addBottom

added theorem Turing.TM2to1.addBottom_head_fst

added theorem Turing.TM2to1.addBottom_map

added theorem Turing.TM2to1.addBottom_modifyNth

added theorem Turing.TM2to1.addBottom_nth_snd

added theorem Turing.TM2to1.addBottom_nth_succ_fst

added def Turing.TM2to1.stRun

added def Turing.TM2to1.stVar

added def Turing.TM2to1.stWrite

added theorem Turing.TM2to1.step_run

added theorem Turing.TM2to1.stk_nth_val

added def Turing.TM2to1.stmtStRec.{l}

added theorem Turing.TM2to1.supports_run

added def Turing.TM2to1.tr

added theorem Turing.TM2to1.trCfg_init

added def Turing.TM2to1.trInit

added def Turing.TM2to1.trNormal

added theorem Turing.TM2to1.trNormal_run

added def Turing.TM2to1.trStAct

added theorem Turing.TM2to1.trStmts₁_run

added theorem Turing.TM2to1.tr_eval

added theorem Turing.TM2to1.tr_eval_dom

added theorem Turing.TM2to1.tr_respects

added theorem Turing.TM2to1.tr_respects_aux

added theorem Turing.TM2to1.tr_respects_aux₁

added theorem Turing.TM2to1.tr_respects_aux₂

added theorem Turing.TM2to1.tr_respects_aux₃

added theorem Turing.TM2to1.tr_supports

added def Turing.TM2to1.Γ'

added inductive Turing.TM2to1.Λ'

added theorem Turing.Tape.exists_mk'

added def Turing.Tape.left₀

added def Turing.Tape.map

added theorem Turing.Tape.map_fst

added theorem Turing.Tape.map_mk'

added theorem Turing.Tape.map_mk₁

added theorem Turing.Tape.map_mk₂

added theorem Turing.Tape.map_move

added theorem Turing.Tape.map_write

added def Turing.Tape.mk'

added theorem Turing.Tape.mk'_head

added theorem Turing.Tape.mk'_left

added theorem Turing.Tape.mk'_left_right₀

added theorem Turing.Tape.mk'_nth_nat

added theorem Turing.Tape.mk'_right

added theorem Turing.Tape.mk'_right₀

added def Turing.Tape.mk₁

added def Turing.Tape.mk₂

added def Turing.Tape.move

added theorem Turing.Tape.move_left_mk'

added theorem Turing.Tape.move_left_nth

added theorem Turing.Tape.move_left_right

added theorem Turing.Tape.move_right_left

added theorem Turing.Tape.move_right_mk'

added theorem Turing.Tape.move_right_n_head

added theorem Turing.Tape.move_right_nth

added def Turing.Tape.nth

added theorem Turing.Tape.nth_zero

added def Turing.Tape.right₀

added theorem Turing.Tape.right₀_nth

added def Turing.Tape.write

added theorem Turing.Tape.write_mk'

added theorem Turing.Tape.write_move_right_n

added theorem Turing.Tape.write_nth

added theorem Turing.Tape.write_self

added structure Turing.Tape

added theorem Turing.eval_maximal

added theorem Turing.eval_maximal₁

added theorem Turing.frespects_eq

added theorem Turing.fun_respects

added theorem Turing.mem_eval

added def Turing.proj

added theorem Turing.proj_map_nth

added theorem Turing.reaches_eval

added theorem Turing.reaches_total

added theorem Turing.reaches₀_eq

added theorem Turing.reaches₁_eq

added theorem Turing.reaches₁_fwd

added theorem Turing.tr_eval'

added theorem Turing.tr_eval

added theorem Turing.tr_eval_dom

added theorem Turing.tr_eval_rev

added theorem Turing.tr_reaches

added theorem Turing.tr_reaches_rev

added theorem Turing.tr_reaches₁