OAI/Computability/WLIdentification/BinaryAddresses.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.WLIdentification.BinaryAddress.Bits line 9
  2. def OAI.WLIdentification.BinaryAddress.value line 11
  3. theorem OAI.WLIdentification.BinaryAddress.value_nil line 15
  4. theorem OAI.WLIdentification.BinaryAddress.value_cons line 16
  5. theorem OAI.WLIdentification.BinaryAddress.value_zero line 19
  6. theorem OAI.WLIdentification.BinaryAddress.value_one line 24
  7. theorem OAI.WLIdentification.BinaryAddress.value_lt line 29
  8. theorem OAI.WLIdentification.BinaryAddress.value_injective line 37
  9. theorem OAI.WLIdentification.BinaryAddress.value_surjective line 51
  10. def OAI.WLIdentification.BinaryAddress.equiv line 61
  11. def OAI.WLIdentification.BinaryAddress.negate line 67
  12. theorem OAI.WLIdentification.BinaryAddress.negate_negate line 69
  13. theorem OAI.WLIdentification.BinaryAddress.value_negate line 72
  14. def OAI.WLIdentification.BinaryAddress.advance line 83

    Source documentation

    Little-endian carry without converting or enumerating the address space.

    def advance : {d : ℕ} → Bits d → Bits d
  | 0, v => v
  | _ + 1, v => Fin.cons (!(v 0))
      (if v 0 then advance (fun i => v i.succ) else fun i => v i.succ)

    Mentions: OAI.WLIdentification.BinaryAddress.Bits

  15. theorem OAI.WLIdentification.BinaryAddress.advance_one line 88
  16. theorem OAI.WLIdentification.BinaryAddress.value_advance line 97
  17. theorem OAI.WLIdentification.BinaryAddress.value_eq_last line 114
  18. theorem OAI.WLIdentification.BinaryAddress.advance_mod line 122
  19. def OAI.WLIdentification.BinaryAddress.Carry line 132

    Source documentation

    Each carry case fixes just the low prefix, including its first noncarry bit.

    def Carry {d : ℕ} (h : Fin d) (b : Bool) (v : Bits d) : Prop :=
…

    Mentions: OAI.WLIdentification.BinaryAddress.Bits

  20. def OAI.WLIdentification.BinaryAddress.flipPrefix line 135
  21. theorem OAI.WLIdentification.BinaryAddress.advance_carry line 138
  22. theorem OAI.WLIdentification.BinaryAddress.carry_exists line 159
  23. theorem OAI.WLIdentification.BinaryAddress.carry_not_last line 179
  24. def OAI.WLIdentification.BinaryAddress.ofNat line 193

    Source documentation

    The executable little-endian digit map; no search through 2^d addresses.

    def ofNat : (d : ℕ) → ℕ → Bits d
  | 0, _ => Fin.elim0
  | d + 1, n => Fin.cons (decide (n % 2 = 1)) (ofNat d (n / 2))

    Mentions: OAI.WLIdentification.BinaryAddress.Bits

  25. theorem OAI.WLIdentification.BinaryAddress.value_ofNat line 197
  26. theorem OAI.WLIdentification.BinaryAddress.ofNat_value line 205
  27. theorem OAI.WLIdentification.BinaryAddress.ofNat_zero line 208
  28. def OAI.WLIdentification.ProductMap.Rel line 217

    Source documentation

    The relation described by a table, without enumerating its product points.

    def Rel (D : ProductMap r) (x y : Fin r → Bool) : Prop :=
…

    Mentions: OAI.WLIdentification.ProductMap

  29. theorem OAI.WLIdentification.ProductMap.rel_point line 220
  30. theorem OAI.WLIdentification.ProductMap.rel_iff line 223
  31. def OAI.WLIdentification.ProductMap.singleton line 230
  32. theorem OAI.WLIdentification.ProductMap.singleton_rel line 236
  33. theorem OAI.WLIdentification.ProductMap.identity_rel line 241
  34. def OAI.WLIdentification.ProductMap.concat line 244
  35. theorem OAI.WLIdentification.ProductMap.concat_rel line 256
  36. def OAI.WLIdentification.ProductMap.inverse line 264
  37. theorem OAI.WLIdentification.ProductMap.inverse_rel line 276