OAI/Computability/Superstring/Combinators.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Superstring.BitCode.bitSize_sublist line 7
  2. theorem OAI.Superstring.BitCode.bitSize_append line 14
  3. def OAI.Superstring.BitCode.foldStep line 20
  4. theorem OAI.Superstring.BitCode.iterate_foldStep line 25
  5. theorem OAI.Superstring.BitCode.Poly.foldStep line 38
  6. theorem OAI.Superstring.BitCode.Poly.foldl line 48

    Source documentation

    A bounded list fold, with its genuine encoded-data invariant exposed. The bound concerns mathematical intermediate values, not an assumed runtime.

     theorem foldl {α β : Type} [Coded α] [Coded β] {f : β → α → β}
    (hf : Poly (fun p : β × α => f p.1 p.2)) (R : Polynomial ℕ)
    (hs : ∀ (xs : List α) (a : β) (j : ℕ), bitSize ((xs.take j).foldl f a) ≤ R.eval (bitSize (xs, a))) :
    Poly (fun p : List α × β => p.1.foldl f p.2) := by
…

    Mentions: OAI.Superstring.BitCode.Coded, OAI.Superstring.BitCode.Poly, OAI.Superstring.BitCode.bitSize

  7. theorem OAI.Superstring.BitCode.bitSize_mem line 79
  8. theorem OAI.Superstring.BitCode.foldl_size_additive line 88
  9. theorem OAI.Superstring.BitCode.Poly.foldl_additive line 104
  10. theorem OAI.Superstring.BitCode.Poly.reverse line 126
  11. theorem OAI.Superstring.BitCode.bitSize_reverse line 144
  12. theorem OAI.Superstring.BitCode.Poly.map line 155
  13. theorem OAI.Superstring.BitCode.Poly.append line 171
  14. theorem OAI.Superstring.BitCode.Poly.length line 183
  15. theorem OAI.Superstring.BitCode.Poly.not line 197
  16. theorem OAI.Superstring.BitCode.Poly.and line 201
  17. theorem OAI.Superstring.BitCode.Poly.or line 205
  18. theorem OAI.Superstring.BitCode.Poly.eqBool line 209
  19. theorem OAI.Superstring.BitCode.Poly.pred line 213
  20. theorem OAI.Superstring.BitCode.Poly.isZero line 220
  21. theorem OAI.Superstring.BitCode.Poly.add line 227
  22. def OAI.Superstring.BitCode.Block.encodeBitList line 251
  23. theorem OAI.Superstring.BitCode.Block.encodeBitList_exec line 254
  24. theorem OAI.Superstring.BitCode.fold_encodeBitList line 275
  25. theorem OAI.Superstring.BitCode.listCode_bit line 284
  26. theorem OAI.Superstring.BitCode.Poly.encoding line 295

    Source documentation

    Materialize the input encoding as an ordinary typed bit list. Each marker and bit is written by charged finite-state stack code.

     theorem encoding {α : Type} [Coded α] : Poly (bits : α → List Bool) := by
…

    Mentions: OAI.Superstring.BitCode.Coded, OAI.Superstring.BitCode.Poly, OAI.Superstring.BitCode.bits

  27. def OAI.Superstring.BitCode.compareBitsStep line 324
  28. theorem OAI.Superstring.BitCode.compareBits_correct line 329
  29. theorem OAI.Superstring.BitCode.compareBits_size line 342
  30. theorem OAI.Superstring.BitCode.Poly.compareBitsStep line 349
  31. theorem OAI.Superstring.BitCode.Poly.eqBits line 362
  32. theorem OAI.Superstring.BitCode.Poly.eq line 371
  33. theorem OAI.Superstring.BitCode.bitSize_map_le line 387
  34. def OAI.Superstring.BitCode.mapWithStep line 398
  35. theorem OAI.Superstring.BitCode.foldl_mapWithStep line 401
  36. theorem OAI.Superstring.BitCode.Poly.mapWith line 412
  37. theorem OAI.Superstring.BitCode.Poly.flatten line 449
  38. theorem OAI.Superstring.BitCode.Poly.filter line 467
  39. theorem OAI.Superstring.BitCode.Poly.filterWith line 479