OAI/Computability/FiniteCompiler/Effectivity.lean

GitHub source file

145 declarations, 0 contain sorry, 0 declared as axioms

Primitive recursive encodings and effective finite compiler data.

  1. def OAI.FiniteAlgebraicEnvelopes.Effect.traverse line 14
  2. def OAI.FiniteAlgebraicEnvelopes.Effect.traverseStep line 18
  3. theorem OAI.FiniteAlgebraicEnvelopes.Effect.traverse_fix line 22
  4. theorem OAI.FiniteAlgebraicEnvelopes.Effect.partrec_traverse line 55
  5. def OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.Action.code line 80
  6. instance OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.(instance at line 92) line 92
  7. def OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.push line 95
  8. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.plan_cons line 102
  9. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.plan_fold line 117
  10. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.Action.primrec_code line 124
  11. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.Action.primrec_decode line 125
  12. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.Action.primrec_keep line 126
  13. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.Action.primrec_raw line 128
  14. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.Action.primrec_call line 130
  15. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.Action.primrec_cases line 133
  16. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.primrec_push line 144
  17. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.primrec_plan line 185
  18. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.Action.partrec_partial line 190
  19. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.partrec_execute line 201
  20. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.partrec_partialSource line 209
  21. def OAI.FiniteAlgebraicEnvelopes.Effect.Graph.expand line 219
  22. def OAI.FiniteAlgebraicEnvelopes.Effect.Graph.search line 222
  23. theorem OAI.FiniteAlgebraicEnvelopes.Effect.Graph.mem_expand line 227
  24. theorem OAI.FiniteAlgebraicEnvelopes.Effect.Graph.search_sub line 232
  25. theorem OAI.FiniteAlgebraicEnvelopes.Effect.Graph.search_mono line 242
  26. theorem OAI.FiniteAlgebraicEnvelopes.Effect.Graph.expand_ext line 249
  27. theorem OAI.FiniteAlgebraicEnvelopes.Effect.Graph.search_stable line 256
  28. def OAI.FiniteAlgebraicEnvelopes.Effect.Graph.component line 274
  29. theorem OAI.FiniteAlgebraicEnvelopes.Effect.Graph.mem_search_connected line 277
  30. theorem OAI.FiniteAlgebraicEnvelopes.Effect.Graph.mem_component_iff line 290
  31. theorem OAI.FiniteAlgebraicEnvelopes.Effect.Graph.primrec_listAny line 316
  32. theorem OAI.FiniteAlgebraicEnvelopes.Effect.Graph.primrec_listFilter line 325
  33. theorem OAI.FiniteAlgebraicEnvelopes.Effect.Graph.primrec_expand line 337
  34. theorem OAI.FiniteAlgebraicEnvelopes.Effect.Graph.primrec_search line 349
  35. theorem OAI.FiniteAlgebraicEnvelopes.Effect.Graph.primrec_component line 359
  36. def OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Sector.code line 370
  37. instance OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.(instance at line 376) line 376
  38. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Sector.primrec_code line 381
  39. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Sector.primrec_decode line 382
  40. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Sector.primrec_left line 385
  41. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Sector.primrec_head line 387
  42. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Sector.primrec_right line 389
  43. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Sector.primrec_lb line 391
  44. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Sector.primrec_rb line 393
  45. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Sector.primrec_mk line 396
  46. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.primrec_baseSkeleton line 402
  47. def OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.finiteList line 411

    Source comment

    All finite choices below are literal lists. No finset or finite-connectivity decision is used as a computability oracle.
    noncomputable def finiteList (α : Type*) [Fintype α] : List α := (Finset.univ : Finset α).toList
  48. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.mem_finiteList line 413
  49. def OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.wordList line 417
  50. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.mem_wordList line 421
  51. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.primrec_wordList line 430
  52. def OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.sectorList line 438
  53. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.mem_sectorList line 445
  54. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.primrec_sectorList line 450
  55. def OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.universeList line 469
  56. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.mem_universeList line 473
  57. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.primrec_universeList line 481
  58. def OAI.FiniteAlgebraicEnvelopes.Compiler.Instruction.code line 493
  59. instance OAI.FiniteAlgebraicEnvelopes.Compiler.(instance at line 499) line 499
  60. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Instruction.primrec_head line 502
  61. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Instruction.primrec_tag line 505
  62. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Instruction.primrec_cross line 509
  63. def OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.flip line 519
  64. def OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.rightStep line 522
  65. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.step_rightStep line 529
  66. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.primrec_flip line 550
  67. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.primrec_rightStep line 556
  68. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.primrec_step line 597
  69. def OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.stepBool line 607
  70. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.primrec_stepBool line 609
  71. def OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.componentList line 613
  72. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.mem_componentList line 617
  73. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.primrec_componentList line 629
  74. def OAI.FiniteAlgebraicEnvelopes.Effect.priorityList line 638
  75. theorem OAI.FiniteAlgebraicEnvelopes.Effect.priorityList_toFinset line 644
  76. theorem OAI.FiniteAlgebraicEnvelopes.Effect.primrec_listIsEmpty line 654
  77. theorem OAI.FiniteAlgebraicEnvelopes.Effect.primrec_priorityList line 658
  78. theorem OAI.FiniteAlgebraicEnvelopes.Effect.primrec_listMin line 670
  79. theorem OAI.FiniteAlgebraicEnvelopes.Effect.minList_eq line 683
  80. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.representative_list line 703
  81. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.primrec_representative line 714
  82. def OAI.FiniteAlgebraicEnvelopes.Effect.finitePrimcodable line 724
  83. def OAI.FiniteAlgebraicEnvelopes.Effect.codeOrder line 727
  84. theorem OAI.FiniteAlgebraicEnvelopes.Effect.primrec_codeOrder line 730
  85. instance OAI.FiniteAlgebraicEnvelopes.Compiler.(instance at line 738) line 738
  86. instance OAI.FiniteAlgebraicEnvelopes.Compiler.(instance at line 739) line 739
  87. instance OAI.FiniteAlgebraicEnvelopes.Compiler.(instance at line 740) line 740
  88. instance OAI.FiniteAlgebraicEnvelopes.Compiler.(instance at line 741) line 741
  89. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Control.primrec_entry line 748
  90. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Control.primrec_success line 754
  91. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Control.primrec_representative line 759
  92. def OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.cleanAnchor line 770
  93. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.rawSweep_takeDrop line 776
  94. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.primrec_rawSweep line 792
  95. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.primrec_rawNormal line 804
  96. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.trimQuota_drop line 815
  97. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.primrec_trimQuota line 822
  98. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.primrec_quotaNormal line 825
  99. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.primrec_unmerge line 841
  100. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.primrec_pendingPreprocess line 876
  101. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.primrec_cleanupOutput line 879
  102. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.primrec_cleanupNormal line 886
  103. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.primrec_cleanupPreprocess line 903
  104. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.primrec_mapHead line 909
  105. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.primrec_internalPreprocess line 922
  106. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.primrec_preprocess line 940
  107. def OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Sector.code line 975
  108. instance OAI.FiniteAlgebraicEnvelopes.Compiler.Path.(instance at line 981) line 981
  109. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Sector.primrec_code line 986
  110. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Sector.primrec_decode line 987
  111. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Sector.primrec_left line 990
  112. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Sector.primrec_head line 992
  113. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Sector.primrec_right line 994
  114. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Sector.primrec_lb line 996
  115. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Sector.primrec_rb line 998
  116. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Sector.primrec_mk line 1001
  117. instance OAI.FiniteAlgebraicEnvelopes.Compiler.Path.(instance at line 1008) line 1008
  118. instance OAI.FiniteAlgebraicEnvelopes.Compiler.Path.(instance at line 1009) line 1009
  119. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.primrec_shape line 1012
  120. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.primrec_heads line 1021
  121. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.primrec_lefts line 1025
  122. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.primrec_rights line 1029
  123. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.primrec_encode line 1034
  124. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.primrec_glue line 1049
  125. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.cuts_fold line 1062
  126. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.primrec_cuts line 1069
  127. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.primrec_mem line 1077
  128. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.primrec_decode line 1080
  129. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.primrec_prepareChunk line 1104
  130. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.primrec_prepareChunks line 1110
  131. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.primrec_prepare line 1114
  132. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.primrec_literal line 1122
  133. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.primrec_unliteral line 1125
  134. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.primrec_sectorPreprocess line 1140
  135. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.primrec_preprocess line 1146
  136. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.primrec_raw line 1151
  137. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.primrec_rawLetters line 1161
  138. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.primrec_readRaw line 1167
  139. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.primrec_classify line 1172
  140. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.primrec_realize line 1179
  141. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.partrec_partialNormal line 1184
  142. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.semanticStep_lift_head line 1209
  143. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.semanticStep_lift line 1231

    Source documentation

    Infinite semantic transitions can always be realized by materializing at most one implicit blank. This is a completeness statement, not an assumption on accepting trajectories.

    theorem semanticStep_lift {c : Tape (S := S) (Γ := Γ) (Q := Q)}
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Tape

  144. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.semanticRun_lift line 1246
  145. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.semantic_halted_iff line 1256