OAI/Computability/RationalHitting/BinaryDivision.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RationalHitting.StackLanguage.subtractBody line 8
  2. def OAI.RationalHitting.StackLanguage.subtractLoop line 11
  3. def OAI.RationalHitting.StackLanguage.subStep line 13
  4. def OAI.RationalHitting.StackLanguage.subFinish line 18
  5. lemma OAI.RationalHitting.StackLanguage.eval_subtractLoop line 23
  6. def OAI.RationalHitting.StackLanguage.subtract line 79

    Source documentation

    Subtract and compare, destructively. Output register 2 has the little-endian fixed-width modular difference; singleton register 3 is exactly the comparison bit (true iff the first number was smaller).

    def subtract : Program (Fin 5) :=
…

    Mentions: OAI.RationalHitting.StackLanguage.Program

  7. lemma OAI.RationalHitting.StackLanguage.eval_subtract line 83
  8. lemma OAI.RationalHitting.StackLanguage.bitNat_le_one line 114
  9. def OAI.RationalHitting.StackLanguage.reduceWord line 116
  10. lemma OAI.RationalHitting.StackLanguage.normalize_length_of_lt line 120
  11. lemma OAI.RationalHitting.StackLanguage.reduceWord_spec line 125
  12. def OAI.RationalHitting.StackLanguage.divideDigits line 143

    Source documentation

    Long division, scanning the original numerator most-significant-bit first. The quotient and remainder registers remain ordinary little-endian words.

    def divideDigits (b : List Bool) : List Bool → List Bool → List Bool → List Bool × List Bool
  | [],r,q => (r,q)
  | x::l,r,q =>
    let v := reduceWord (x::r) b
…

    Mentions: OAI.RationalHitting.StackLanguage.reduceWord

  13. lemma OAI.RationalHitting.StackLanguage.divideDigits_spec line 149
  14. lemma OAI.RationalHitting.StackLanguage.divideDigits_quotient_remainder line 171
  15. def OAI.RationalHitting.StackLanguage.Program.rename line 188
  16. lemma OAI.RationalHitting.StackLanguage.extend_update_store line 197
  17. lemma OAI.RationalHitting.StackLanguage.extend_transfer_store line 211
  18. theorem OAI.RationalHitting.StackLanguage.Eval.rename line 225

    Source documentation

    Uniform register allocation: renaming injectively never changes time and preserves every register outside its finite image.

    theorem Eval.rename {p : Program K} {s v : Store K} {t : ℕ} (h : Eval p s v t)
    (f : K → L) (hf : Injective f) (S : Store L) :
    Eval (p.rename f) (extend f s S) (extend f v S) t := by
…

    Mentions: OAI.RationalHitting.StackLanguage.Program, OAI.RationalHitting.StackLanguage.Store, OAI.RationalHitting.StackLanguage.Eval

  19. lemma OAI.RationalHitting.StackLanguage.extend_pull_store line 246
  20. lemma OAI.RationalHitting.StackLanguage.eval_rename_from line 255