OAI/Combinatorics/ParityLifts/TreePrograms.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ParityWL.Complexity.FCode.const line 7
  2. lemma OAI.ParityWL.Complexity.BEval.const line 11
  3. inductive OAI.ParityWL.Complexity.TExpr line 20

    Source documentation

    Finite tree expressions are uniformly linear in the size of their argument; no arithmetic or lookup oracle is concealed in an expression.

    inductive TExpr where
…
  4. def OAI.ParityWL.Complexity.TExpr.eval line 27
  5. def OAI.ParityWL.Complexity.TExpr.compile line 34
  6. def OAI.ParityWL.Complexity.TExpr.cost line 42
  7. lemma OAI.ParityWL.Complexity.TExpr.run line 49
  8. abbrev OAI.ParityWL.Complexity.TExpr.left line 70
  9. abbrev OAI.ParityWL.Complexity.TExpr.right line 71
  10. abbrev OAI.ParityWL.Complexity.TExpr.nil line 72
  11. lemma OAI.ParityWL.Complexity.BEval.loop_iterate line 74
  12. class OAI.ParityWL.Complexity.TreeCodec line 103
  13. abbrev OAI.ParityWL.Complexity.treeEncode line 107
  14. instance OAI.ParityWL.Complexity.(instance at line 109) line 109
  15. def OAI.ParityWL.Complexity.boolTree line 111
  16. instance OAI.ParityWL.Complexity.(instance at line 112) line 112
  17. lemma OAI.ParityWL.Complexity.treeEncode_false line 116
  18. lemma OAI.ParityWL.Complexity.treeEncode_true line 117
  19. instance OAI.ParityWL.Complexity.(instance at line 119) line 119
  20. lemma OAI.ParityWL.Complexity.treeEncode_pair line 129
  21. lemma OAI.ParityWL.Complexity.treeEncode_prod line 132
  22. def OAI.ParityWL.Complexity.DataTree.ofList line 135
  23. lemma OAI.ParityWL.Complexity.DataTree.ofList_injective line 139
  24. instance OAI.ParityWL.Complexity.(instance at line 153) line 153
  25. lemma OAI.ParityWL.Complexity.treeEncode_nil line 159
  26. lemma OAI.ParityWL.Complexity.treeEncode_cons line 160
  27. lemma OAI.ParityWL.Complexity.treeEncode_list_size line 163
  28. lemma OAI.ParityWL.Complexity.treeEncode_bits line 169
  29. structure OAI.ParityWL.Complexity.TreeProgram line 176

    Source documentation

    A verified program on a concrete tree encoding. time is a proved bound on both work and intermediate storage, never an oracle interpretation of code.

    structure TreeProgram (α β : Type) [TreeCodec α] [TreeCodec β] (f : α → β) where
…

    Mentions: OAI.ParityWL.Complexity.TreeCodec

  30. def OAI.ParityWL.Complexity.TreeProgram.id line 181
  31. def OAI.ParityWL.Complexity.TreeProgram.const line 186
  32. def OAI.ParityWL.Complexity.TreeProgram.fst line 192
  33. def OAI.ParityWL.Complexity.TreeProgram.snd line 199
  34. def OAI.ParityWL.Complexity.TreeProgram.comp line 206
  35. def OAI.ParityWL.Complexity.TreeProgram.pair line 213
  36. def OAI.ParityWL.Complexity.TreeProgram.ite line 220
  37. lemma OAI.ParityWL.Complexity.BEval.loop_terminates line 233
  38. def OAI.ParityWL.Complexity.TreeProgram.congr line 265
  39. def OAI.ParityWL.Complexity.FCode.foldBody line 272
  40. def OAI.ParityWL.Complexity.TreeProgram.foldWork line 275
  41. lemma OAI.ParityWL.Complexity.TreeProgram.foldBody_run line 281
  42. lemma OAI.ParityWL.Complexity.TreeProgram.foldLoop_run line 300
  43. def OAI.ParityWL.Complexity.TreeProgram.foldl line 309
  44. lemma OAI.ParityWL.Complexity.treeEncode_list_size_mono line 320
  45. lemma OAI.ParityWL.Complexity.TreeProgram.foldWork_bound line 325