OAI/Computability/MaxCut/PCP/ContextClear.lean

GitHub source file

77 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceContextClear.Tape line 11
2. def OAI.MaxCutGames.Foundations.Hastad.SourceContextClear.fieldAt line 15
3. def OAI.MaxCutGames.Foundations.Hastad.SourceContextClear.fields line 18
4. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContextClear.fieldAt_injective line 20
5. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContextClear.fields_length line 27
6. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContextClear.fields_nodup line 30
7. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContextClear.field_mem line 33
8. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContextClear.mem_fields_iff line 38
9. def OAI.MaxCutGames.Foundations.Hastad.SourceContextClear.outputTapes line 46
10. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContextClear.output_field line 50
11. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContextClear.output_frame line 53
12. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceContextClear.Label line 57
13. def OAI.MaxCutGames.Foundations.Hastad.SourceContextClear.entryLabel_inline_SourceContextClear line 60
14. def OAI.MaxCutGames.Foundations.Hastad.SourceContextClear.main line 64
15. def OAI.MaxCutGames.Foundations.Hastad.SourceContextClear.program line 68
16. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContextClear.entryLabel_eq_inline_SourceContextClear line 73
17. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContextClear.entry_eq_inline_SourceContextClear line 80
18. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContextClear.finalTapes_eq line 84
19. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContextClear.lengthSum_update_inline_SourceContextClear line 90
20. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContextClear.steps_eq_of_nodup_inline_SourceContextClear line 101

    Source documentation

    Distinct chosen tapes make the pre-cleanup length sum the exact drain cost.

    private theorem steps_eq_of_nodup_inline_SourceContextClear {K : Type} [DecidableEq K] (chosen : List K)
        (h : chosen.Nodup) (base : K → List Bool) :
        MachineDrainMany.steps chosen base =
          MachineDrainMany.lengthSum chosen base + chosen.length := by
    …

21. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContextClear.trace_trans_inline_SourceContextClear line 113
22. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContextClear.clearTrace line 117
23. def OAI.MaxCutGames.Foundations.Hastad.SourceContextClear.clearInTime line 129
24. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContextClear.lengthSum_le_selected_inline_SourceContextClear line 137
25. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContextClear.clauseField_length_le line 149
26. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContextClear.variables_add_two_le_input line 157
27. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContextClear.loaded_field_length_le line 164
28. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContextClear.loaded_cost_le line 173
29. def OAI.MaxCutGames.Foundations.Hastad.SourceContextClear.clearLoadedInTime line 186
30. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContextClear.output_loaded_eq_base line 198
31. def OAI.MaxCutGames.Foundations.Hastad.SourceContextClear.clearLoadedToBaseInTime line 211

    Source documentation

    With initially clean fields and lookup work tapes, loading followed by this cleanup restores the caller's original frame exactly.

    def clearLoadedToBaseInTime (F : Target.Formula) (tuple : Fin u → Fin F.clauses.length)
        (base : Tape u Extra → List Bool) (hfields : ∀ j s, base (.field j s) = [])
        (hindex : base .index = []) (hwork : base .work = []) (register : Option Bool) :
        StateTransition.EvalsToInTime (TM2.step program)
          ⟨some main, ((), register), SourceContextLoad.stageTapes F tuple base u⟩
          (some ⟨none, ((), none), base⟩)
          (6 * u * ((formulaBits F).length + 1) + 1) := by
    …

    Mentions: OAI.MaxCutGames.Foundations.Target.Formula, OAI.MaxCutGames.Foundations.Hastad.SourceContextClear.Tape, OAI.MaxCutGames.Foundations.Hastad.SourceContextClear.program, OAI.MaxCutGames.Foundations.Hastad.SourceContextClear.main, OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.stageTapes

32. def OAI.MaxCutGames.Foundations.Hastad.SourceContextClear.machine line 221
33. def OAI.MaxCutGames.Foundations.Hastad.SourceQueryOrder.occurrenceBits line 239
34. def OAI.MaxCutGames.Foundations.Hastad.SourceQueryOrder.slotBits line 242
35. def OAI.MaxCutGames.Foundations.Hastad.SourceQueryOrder.tupleBits line 246
36. theorem OAI.MaxCutGames.Foundations.Hastad.SourceQueryOrder.equationBits_eq line 249
37. theorem OAI.MaxCutGames.Foundations.Hastad.SourceQueryOrder.prefixBits_eq_slotBits line 256
38. theorem OAI.MaxCutGames.Foundations.Hastad.SourceQueryOrder.sourceLoopInTime line 269
39. structure OAI.MaxCutGames.Foundations.Hastad.SourceTupleTape.Snapshot line 313
40. def OAI.MaxCutGames.Foundations.Hastad.SourceTupleTape.tapes line 323
41. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleTape.tapes_rank line 331
42. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleTape.tapes_rightBase line 333
43. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleTape.tapes_leftBase line 335
44. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleTape.tapes_zero line 337
45. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleTape.tapes_accumulator line 339
46. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleTape.tapes_coefficient line 341
47. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleTape.tapes_dummy line 343
48. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleTape.tapes_leftBlock line 345
49. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleTape.tapes_queryTemporary line 347
50. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleTape.tapes_queryScratch line 349
51. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleTape.tapes_field line 351
52. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleTape.tapes_current line 353
53. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleTape.tapes_formula line 355
54. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleTape.tapes_index line 357
55. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleTape.tapes_work line 359
56. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleTape.tapes_variableHeader line 361
57. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleTape.tapes_clauseHeader line 363
58. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleTape.update_rank line 368
59. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleTape.update_rightBase line 377
60. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleTape.update_leftBase line 386
61. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleTape.update_zero line 395
62. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleTape.update_emitted line 404
63. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleTape.query_result line 414
64. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleTape.horner_clause_result line 423
65. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleTape.horner_variable_result line 430
66. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleTape.horner_right_result line 438
67. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleTape.horner_left_result line 445
68. structure OAI.MaxCutGames.Foundations.Hastad.SourceTupleTape.WorkClean line 452
69. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleTape.clean_clause line 459
70. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleTape.clean_variable line 467
71. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleTape.clean_base line 475
72. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleTape.tapes_coordinateOutput line 483
73. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleTape.tapes_stageTapes line 497
74. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleTape.final_tapes line 509
75. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleTape.empty_tapes line 522
76. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleTape.clear_loaded line 529
77. def OAI.MaxCutGames.Foundations.Hastad.SourceTupleTape.clearLoadedSnapshotInTime line 537

    Source documentation

    Apply the checked actual field cleanup directly to an overlaid loaded context.

    def clearLoadedSnapshotInTime (F : Target.Formula) (c : ClauseContext F u)
        (base : Arena u Extra → List Bool) (s : Snapshot)
        (hfields : ∀ j k, base (.field j k) = []) (hindex : base .index = []) (hwork : base .work = [])
        (register : Option Bool) :
        StateTransition.EvalsToInTime (TM2.step SourceContextClear.program)
          ⟨some SourceContextClear.main, ((), register), tapes (SourceContextLoad.stageTapes F c base u) s⟩
          (some ⟨none, ((), none), tapes base s⟩)
          (6 * u * ((formulaBits F).length + 1) + 1) := by
    …

    Mentions: OAI.MaxCutGames.Foundations.Target.Formula, OAI.MaxCutGames.Foundations.Hastad.SourceTupleTape.Snapshot, OAI.MaxCutGames.Foundations.Hastad.SourceContextClear.program, OAI.MaxCutGames.Foundations.Hastad.SourceContextClear.main, OAI.MaxCutGames.Foundations.Hastad.SourceTupleTape.tapes, OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.stageTapes