OAI/Computability/RationalHitting/Tabulation.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RationalHitting.StackLanguage.listCode line 9

    Source documentation

    Reusable dense records. Individual word lengths need not be fixed.

    def listCode {A : Type} (ca : A → List Bool) (l : List A) : List Bool :=
…
  2. lemma OAI.RationalHitting.StackLanguage.listCode_nil line 11
  3. lemma OAI.RationalHitting.StackLanguage.listCode_cons line 12
  4. lemma OAI.RationalHitting.StackLanguage.listCode_append line 14
  5. lemma OAI.RationalHitting.StackLanguage.listCode_singleton line 16
  6. lemma OAI.RationalHitting.StackLanguage.length_le_listCode line 18
  7. lemma OAI.RationalHitting.StackLanguage.listCode_length_le line 23
  8. lemma OAI.RationalHitting.StackLanguage.listCode_element line 32
  9. theorem OAI.RationalHitting.StackLanguage.Feasible.listCons line 45
  10. theorem OAI.RationalHitting.StackLanguage.Feasible.listSingleton line 49
  11. theorem OAI.RationalHitting.StackLanguage.Feasible.listAppend line 52
  12. theorem OAI.RationalHitting.StackLanguage.Feasible.unarySucc line 66
  13. def OAI.RationalHitting.StackLanguage.tableStep line 74

    Source documentation

    A complete uniform table-building step: evaluation of a compiled callback, indexed counter update, and append of an escaped dense record.

    def tableStep {A B : Type} (f : A × ℕ → B) (a : A × (ℕ × List B)) : A × (ℕ × List B) :=
…
  14. def OAI.RationalHitting.StackLanguage.tableStateCode line 77
  15. lemma OAI.RationalHitting.StackLanguage.tableStateCode_length line 80
  16. lemma OAI.RationalHitting.StackLanguage.tableStep_iterate_fields line 85
  17. lemma OAI.RationalHitting.StackLanguage.tableStep_iterate_size line 93
  18. lemma OAI.RationalHitting.StackLanguage.tableStep_iterate_start line 128
  19. theorem OAI.RationalHitting.StackLanguage.Feasible.tableStep line 139
  20. theorem OAI.RationalHitting.StackLanguage.Feasible.tabulate line 152

    Source documentation

    Polynomial-time tabulation of an arbitrary polynomial-time callback. The construction uses only one finite stack program, including all indexing, record layout, and loop control; the counter is unary.

    theorem tabulate (hf : Feasible (pairCode ca unaryCode) cb f) :
    Feasible (pairCode unaryCode ca) (listCode cb)
      (fun a => (List.range a.1).map (fun i => f (a.2,i))) := by
…

    Mentions: OAI.RationalHitting.StackLanguage.Feasible, OAI.RationalHitting.StackLanguage.pairCode, OAI.RationalHitting.StackLanguage.unaryCode, OAI.RationalHitting.StackLanguage.listCode

  21. class OAI.RationalHitting.StackLanguage.Coding line 173

    Source documentation

    Canonical storage format for the compositional finite-program proofs.

    class Coding (A : Type) where
…
  22. instance OAI.RationalHitting.StackLanguage.(instance at line 177) line 177
  23. instance OAI.RationalHitting.StackLanguage.(instance at line 178) line 178
  24. instance OAI.RationalHitting.StackLanguage.(instance at line 179) line 179
  25. instance OAI.RationalHitting.StackLanguage.(instance at line 180) line 180
  26. instance OAI.RationalHitting.StackLanguage.(instance at line 181) line 181
  27. structure OAI.RationalHitting.StackLanguage.Unary line 183
  28. instance OAI.RationalHitting.StackLanguage.(instance at line 186) line 186
  29. structure OAI.RationalHitting.StackLanguage.BitWord line 188
  30. instance OAI.RationalHitting.StackLanguage.(instance at line 191) line 191
  31. def OAI.RationalHitting.StackLanguage.Poly line 195

    Source documentation

    Polynomial time means a concrete finite clean stack program and actual step bound, through Procedure. It is not machine advice or an oracle.

    @[fun_prop] def Poly {A B : Type} [Coding A] [Coding B] (f : A → B) : Prop :=
…

    Mentions: OAI.RationalHitting.StackLanguage.Coding

  32. theorem OAI.RationalHitting.StackLanguage.Poly.id line 202
  33. theorem OAI.RationalHitting.StackLanguage.Poly.const line 203
  34. theorem OAI.RationalHitting.StackLanguage.Poly.comp line 204
  35. theorem OAI.RationalHitting.StackLanguage.Poly.pair line 206
  36. theorem OAI.RationalHitting.StackLanguage.Poly.fst line 208
  37. theorem OAI.RationalHitting.StackLanguage.Poly.snd line 209
  38. theorem OAI.RationalHitting.StackLanguage.Poly.subtypeVal line 210
  39. theorem OAI.RationalHitting.StackLanguage.Poly.subtypeMk line 213
  40. theorem OAI.RationalHitting.StackLanguage.Poly.of_eq line 217
  41. theorem OAI.RationalHitting.StackLanguage.Poly.cond line 220
  42. theorem OAI.RationalHitting.StackLanguage.Poly.natAdd line 224
  43. theorem OAI.RationalHitting.StackLanguage.Poly.natMul line 225
  44. theorem OAI.RationalHitting.StackLanguage.Poly.unarySucc line 227
  45. theorem OAI.RationalHitting.StackLanguage.Poly.unaryAdd line 229
  46. theorem OAI.RationalHitting.StackLanguage.Poly.listCons line 232
  47. theorem OAI.RationalHitting.StackLanguage.Poly.listSingleton line 233
  48. theorem OAI.RationalHitting.StackLanguage.Poly.listAppend line 234
  49. theorem OAI.RationalHitting.StackLanguage.Poly.wordAppend line 235
  50. theorem OAI.RationalHitting.StackLanguage.Poly.tabulate line 238
  51. example OAI.RationalHitting.StackLanguage.Poly.(example at line 245) line 245
  52. example OAI.RationalHitting.StackLanguage.Poly.(example at line 246) line 246