OAI/Combinatorics/LowSpaceSubsetSum/Streams/CyclicCursor.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Constant-state cyclic array traversal

The mutable cursor has only a position, remaining length, and direction. next accesses the shared immutable array once and changes these fields. trace is an analysis view of repeated advances; it is not retained by the stream. A complete traversal permutes array occurrences, so equal-valued items are never lost at a cyclic pivot.

  1. structure OAI.LowSpaceSubsetSum.CyclicCursor.State line 25
  2. def OAI.LowSpaceSubsetSum.CyclicCursor.advance line 31
  3. def OAI.LowSpaceSubsetSum.CyclicCursor.next line 34
  4. theorem OAI.LowSpaceSubsetSum.CyclicCursor.next_eq_none_iff line 38
  5. theorem OAI.LowSpaceSubsetSum.CyclicCursor.advance_remaining line 42
  6. theorem OAI.LowSpaceSubsetSum.CyclicCursor.advance_reverse line 45
  7. def OAI.LowSpaceSubsetSum.CyclicCursor.trace line 48

    Source documentation

    Analysis only: the finite output of a bounded number of advances.

    def trace (a : Fin n → α) : ℕ → State n → List α
  | 0, _ => []
  | k + 1, c => if c.remaining = 0 then [] else a c.position :: trace a k (advance c)

    Mentions: OAI.LowSpaceSubsetSum.CyclicCursor.State, OAI.LowSpaceSubsetSum.CyclicCursor.advance

  8. def OAI.LowSpaceSubsetSum.CyclicCursor.order line 52
  9. theorem OAI.LowSpaceSubsetSum.CyclicCursor.trace_eq_ofFn line 58
  10. theorem OAI.LowSpaceSubsetSum.CyclicCursor.forward_trace_eq_rotate line 75
  11. theorem OAI.LowSpaceSubsetSum.CyclicCursor.reverse_trace_eq_reverse_forward line 86
  12. theorem OAI.LowSpaceSubsetSum.CyclicCursor.forward_trace_split line 104
  13. theorem OAI.LowSpaceSubsetSum.CyclicCursor.reverse_trace_split line 112
  14. theorem OAI.LowSpaceSubsetSum.CyclicCursor.direct_of_split line 120
  15. theorem OAI.LowSpaceSubsetSum.CyclicCursor.complementary_of_split line 137
  16. theorem OAI.LowSpaceSubsetSum.CyclicCursor.forward_trace_eq_direct line 154
  17. theorem OAI.LowSpaceSubsetSum.CyclicCursor.reverse_trace_eq_complementary line 162
  18. theorem OAI.LowSpaceSubsetSum.CyclicCursor.full_trace_perm line 170
  19. theorem OAI.LowSpaceSubsetSum.CyclicCursor.full_trace_array_perm line 176
  20. theorem OAI.LowSpaceSubsetSum.CyclicCursor.trace_length line 186

    Source documentation

    Every stopped traversal reports exactly the consumed number of occurrences.

    theorem trace_length (a : Fin n → α) (k : ℕ) (c : State n) (hk : k ≤ c.remaining) :
    (trace a k c).length = k := by rw [trace_eq_ofFn a k c hk, List.length_ofFn]

    Mentions: OAI.LowSpaceSubsetSum.CyclicCursor.State, OAI.LowSpaceSubsetSum.CyclicCursor.trace, OAI.LowSpaceSubsetSum.CyclicCursor.trace_eq_ofFn

  21. theorem OAI.LowSpaceSubsetSum.CyclicCursor.advance_iterate_remaining line 189