OAI/Computability/Superstring/Encoding.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Superstring.BitCode.Steps.terminal_unique line 9
  2. theorem OAI.Superstring.BitCode.Block.Exec.deterministic line 24
  3. theorem OAI.Superstring.BitCode.Parses.separate line 30
  4. class OAI.Superstring.BitCode.Coded line 46
  5. abbrev OAI.Superstring.BitCode.bits line 51
  6. abbrev OAI.Superstring.BitCode.bitSize line 52
  7. def OAI.Superstring.BitCode.Poly line 54
  8. instance OAI.Superstring.BitCode.codedBool line 57
  9. instance OAI.Superstring.BitCode.codedUnit line 62
  10. instance OAI.Superstring.BitCode.codedNat line 67
  11. instance OAI.Superstring.BitCode.codedProd line 76
  12. instance OAI.Superstring.BitCode.codedList line 84
  13. theorem OAI.Superstring.BitCode.bits_bool line 100
  14. theorem OAI.Superstring.BitCode.bits_unit line 101
  15. theorem OAI.Superstring.BitCode.bits_nat line 102
  16. theorem OAI.Superstring.BitCode.bits_prod line 103
  17. theorem OAI.Superstring.BitCode.bits_nil line 105
  18. theorem OAI.Superstring.BitCode.bits_cons line 106
  19. theorem OAI.Superstring.BitCode.bitSize_nat line 108
  20. theorem OAI.Superstring.BitCode.bitSize_prod line 109
  21. theorem OAI.Superstring.BitCode.bitSize_nil line 111
  22. theorem OAI.Superstring.BitCode.bitSize_cons line 112
  23. theorem OAI.Superstring.BitCode.length_le_bitSize line 116
  24. theorem OAI.Superstring.BitCode.Poly.id line 125
  25. theorem OAI.Superstring.BitCode.Poly.const line 126
  26. theorem OAI.Superstring.BitCode.Poly.comp line 127
  27. theorem OAI.Superstring.BitCode.Poly.pair line 129
  28. theorem OAI.Superstring.BitCode.Poly.fst line 131
  29. theorem OAI.Superstring.BitCode.Poly.snd line 132
  30. theorem OAI.Superstring.BitCode.Poly.cons line 133
  31. theorem OAI.Superstring.BitCode.Poly.ite line 134
  32. theorem OAI.Superstring.BitCode.Poly.iterate line 139
  33. theorem OAI.Superstring.BitCode.Poly.output_size line 143
  34. def OAI.Superstring.BitCode.sumCode line 153
  35. theorem OAI.Superstring.BitCode.Parses.sum line 157
  36. instance OAI.Superstring.BitCode.codedSum line 190
  37. theorem OAI.Superstring.BitCode.bits_inl line 203
  38. theorem OAI.Superstring.BitCode.bits_inr line 205
  39. theorem OAI.Superstring.BitCode.Poly.sumCases line 210
  40. theorem OAI.Superstring.BitCode.Poly.reencode line 253

    Source documentation

    Merely changing a typed view of the SAME input bits does not execute the view function. This is used only with an explicit encoding equality below.

     theorem reencode {α β γ : Type} [Coded α] [Coded β] [Coded γ]
    {f : β → γ} (hf : Poly f) (r : α → β) (he : ∀ a, bits (r a) = bits a) :
    Poly (f ∘ r) := by
…

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

  41. theorem OAI.Superstring.BitCode.Poly.listCases line 263

    Source documentation

    One-step list destructor, implemented only by the leading spine marker. The nonempty branch receives exactly the head followed by the encoded tail.

     theorem listCases {α β : Type} [Coded α] [Coded β] (z : β)
    {f : α × List α → β} (hf : Poly f) :
    Poly (fun xs : List α => match xs with | [] => z | x :: xs => f (x, xs)) := by
…

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

  42. theorem OAI.Superstring.BitCode.Poly.tail line 273
  43. theorem OAI.Superstring.BitCode.Poly.headD line 276
  44. theorem OAI.Superstring.BitCode.Poly.isEmpty line 280
  45. def OAI.Superstring.BitCode.Block.countBits line 291
  46. theorem OAI.Superstring.BitCode.Block.countBits_exec line 293
  47. theorem OAI.Superstring.BitCode.Poly.size line 316
  48. theorem OAI.Superstring.BitCode.Poly.succ line 334
  49. theorem OAI.Superstring.BitCode.Poly.listCasesWith line 342
  50. theorem OAI.Superstring.BitCode.Poly.natCasesWith line 356