OAI/Combinatorics/LowSpaceSubsetSum/Streams/TieGroup.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.LowSpaceSubsetSum.TieGroup.State line 21
2. def OAI.LowSpaceSubsetSum.TieGroup.step line 28
3. structure OAI.LowSpaceSubsetSum.TieGroup.Result line 35
4. def OAI.LowSpaceSubsetSum.TieGroup.run line 41
5. theorem OAI.LowSpaceSubsetSum.TieGroup.step_bounds line 54

   Source documentation

   Bounds on callbacks follow from the actual suffix reporter, not from assumed trial or implementation bounds.

   theorem step_bounds (read₂ : σ₂ → Option (β × σ₂)) (key₂ : β → ℤ) (K : ℤ)
       (report : α → β → τ → τ × Bool) (view₂ : σ₂ → List β)
       (hread₂ : RowMerge.IsReader read₂ view₂) (buffer : Array β) (saved : σ₂)
       (long : Bool) (fuel₂ : ℕ) (x : α) (a : State σ₂ τ) :
       (step read₂ key₂ K report buffer saved long fuel₂ x a).1.reports ≤
           a.reports + (buffer.size + (TieBuffer.groupView key₂ K view₂ saved).length) ∧
       (step read₂ key₂ K report buffer saved long fuel₂ x a).1.queries ≤
           a.queries + (buffer.size + (TieBuffer.groupView key₂ K view₂ saved).length + 1) ∧
       (step read₂ key₂ K report buffer saved long fuel₂ x a).1.restores ≤ a.restores + 1 := by
   …

   Mentions: OAI.LowSpaceSubsetSum.RowMerge.IsReader, OAI.LowSpaceSubsetSum.TieGroup.State, OAI.LowSpaceSubsetSum.TieGroup.step, OAI.LowSpaceSubsetSum.TieBuffer.groupView

6. theorem OAI.LowSpaceSubsetSum.TieGroup.run_bounds line 69
7. theorem OAI.LowSpaceSubsetSum.TieGroup.state_complete line 119

   Source documentation

   On a continuing run every occurrence in the Cartesian tie group is reported, in first-stream order and then second-stream order.

   theorem state_complete (read₁ : σ₁ → Option (α × σ₁)) (key₁ : α → ℤ)
       (read₂ : σ₂ → Option (β × σ₂)) (key₂ : β → ℤ) (K : ℤ)
       (report : α → β → τ → τ × Bool) (hreport : ∀ x y a, (report x y a).2 = false)
       (view₁ : σ₁ → List α) (hread₁ : RowMerge.IsReader read₁ view₁)
       (view₂ : σ₂ → List β) (hread₂ : RowMerge.IsReader read₂ view₂)
       (B fuel₁ fuel₂ : ℕ) (s₁ : σ₁) (s₂ : σ₂) (a : τ)
       (hfuel₁ : (TieBuffer.groupView key₁ K view₁ s₁).length ≤ fuel₁)
       (hfuel₂ : (TieBuffer.groupView key₂ K view₂ s₂).length ≤ fuel₂) :
       (run read₁ key₁ read₂ key₂ K report B fuel₁ fuel₂ s₁ s₂ a).outer.state.user =
         (TieBuffer.groupView key₁ K view₁ s₁).foldl
           (fun a x => (TieBuffer.groupView key₂ K view₂ s₂).foldl
             (fun a y => (report x y a).1) a) a := by
   …

   Mentions: OAI.LowSpaceSubsetSum.RowMerge.IsReader, OAI.LowSpaceSubsetSum.TieBuffer.groupView, OAI.LowSpaceSubsetSum.TieGroup.run

8. theorem OAI.LowSpaceSubsetSum.TieGroup.step_halted_false line 150
9. theorem OAI.LowSpaceSubsetSum.TieGroup.halted_false line 156
10. theorem OAI.LowSpaceSubsetSum.TieGroup.views_complete line 166

    Source documentation

    Both generator cursors end immediately after this key, so a surrounding merge join can continue without losing its next different-key occurrences.

    theorem views_complete (read₁ : σ₁ → Option (α × σ₁)) (key₁ : α → ℤ)
        (read₂ : σ₂ → Option (β × σ₂)) (key₂ : β → ℤ) (K : ℤ)
        (report : α → β → τ → τ × Bool) (hreport : ∀ x y a, (report x y a).2 = false)
        (view₁ : σ₁ → List α) (hread₁ : RowMerge.IsReader read₁ view₁)
        (view₂ : σ₂ → List β) (hread₂ : RowMerge.IsReader read₂ view₂)
        (B fuel₁ fuel₂ : ℕ) (s₁ : σ₁) (s₂ : σ₂) (a : τ)
        (hfuel₁ : (TieBuffer.groupView key₁ K view₁ s₁).length ≤ fuel₁)
        (hfuel₂ : (TieBuffer.groupView key₂ K view₂ s₂).length ≤ fuel₂)
        (hne : TieBuffer.groupView key₁ K view₁ s₁ ≠ []) :
        view₁ s₁ = TieBuffer.groupView key₁ K view₁ s₁ ++
            view₁ (run read₁ key₁ read₂ key₂ K report B fuel₁ fuel₂ s₁ s₂ a).outer.cursor ∧
        view₂ s₂ = TieBuffer.groupView key₂ K view₂ s₂ ++
    …

    Mentions: OAI.LowSpaceSubsetSum.RowMerge.IsReader, OAI.LowSpaceSubsetSum.TieBuffer.groupView, OAI.LowSpaceSubsetSum.TieGroup.run

11. theorem OAI.LowSpaceSubsetSum.TieGroup.query_bound line 207
12. theorem OAI.LowSpaceSubsetSum.TieGroup.bufferSize_le line 232
13. theorem OAI.LowSpaceSubsetSum.TieGroup.restores_eq_zero_of_short line 241

    Source documentation

    Without a long suffix, there are no generator restores.

    theorem restores_eq_zero_of_short (read₁ : σ₁ → Option (α × σ₁)) (key₁ : α → ℤ)
        (read₂ : σ₂ → Option (β × σ₂)) (key₂ : β → ℤ) (K : ℤ)
        (report : α → β → τ → τ × Bool) (B fuel₁ fuel₂ : ℕ)
        (s₁ : σ₁) (s₂ : σ₂) (a : τ)
        (hshort : TieBuffer.hasKey read₂ key₂ K (TieBuffer.fill read₂ key₂ K B s₂).cursor = false) :
        (run read₁ key₁ read₂ key₂ K report B fuel₁ fuel₂ s₁ s₂ a).outer.state.restores = 0 := by
    …

    Mentions: OAI.LowSpaceSubsetSum.TieBuffer.hasKey, OAI.LowSpaceSubsetSum.TieBuffer.fill, OAI.LowSpaceSubsetSum.TieGroup.run

14. theorem OAI.LowSpaceSubsetSum.TieGroup.copies_charged line 255

    Source documentation

    Every snapshot/restore is charged to potential partners, including partners not reached when the execution halts.

    theorem copies_charged (read₁ : σ₁ → Option (α × σ₁)) (key₁ : α → ℤ)
        (read₂ : σ₂ → Option (β × σ₂)) (key₂ : β → ℤ) (K : ℤ)
        (report : α → β → τ → τ × Bool)
        (view₁ : σ₁ → List α) (hread₁ : RowMerge.IsReader read₁ view₁)
        (view₂ : σ₂ → List β) (hread₂ : RowMerge.IsReader read₂ view₂)
        (B fuel₁ fuel₂ : ℕ) (s₁ : σ₁) (s₂ : σ₂) (a : τ) :
        B * ((if (run read₁ key₁ read₂ key₂ K report B fuel₁ fuel₂ s₁ s₂ a).snapshot then 1 else 0) +
          (run read₁ key₁ read₂ key₂ K report B fuel₁ fuel₂ s₁ s₂ a).outer.state.restores) ≤
          2 * ((TieBuffer.groupView key₁ K view₁ s₁).length *
            (TieBuffer.groupView key₂ K view₂ s₂).length) := by
    …

    Mentions: OAI.LowSpaceSubsetSum.RowMerge.IsReader, OAI.LowSpaceSubsetSum.TieGroup.run, OAI.LowSpaceSubsetSum.TieBuffer.groupView