OAI/Combinatorics/LowSpaceSubsetSum/Streams/StreamWitness.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LowSpaceSubsetSum.StreamWitness.remember line 13
2. theorem OAI.LowSpaceSubsetSum.StreamWitness.foldl_remember line 16
3. theorem OAI.LowSpaceSubsetSum.StreamWitness.matchFold_iff line 26
4. theorem OAI.LowSpaceSubsetSum.StreamWitness.matchFold_true line 37
5. theorem OAI.LowSpaceSubsetSum.StreamWitness.run_iff line 44

   Source documentation

   The actual finite-state join finds exactly the matching occurrences accepted by its pair predicate. The callback retains one Boolean word.

   theorem run_iff {σ₁ σ₂ : Type*}
       (read₁ : σ₁ → Option (α × σ₁)) (key₁ : α → ℤ)
       (read₂ : σ₂ → Option (β × σ₂)) (key₂ : β → ℤ) (hit : α → β → Bool)
       (view₁ : σ₁ → List α) (hread₁ : RowMerge.IsReader read₁ view₁)
       (view₂ : σ₂ → List β) (hread₂ : RowMerge.IsReader read₂ view₂)
       (B fuel₁ fuel₂ controlFuel : ℕ) (s₁ : σ₁) (s₂ : σ₂)
       (hsort₁ : (view₁ s₁).Pairwise (fun x y => key₁ x ≤ key₁ y))
       (hsort₂ : (view₂ s₂).Pairwise (fun x y => key₂ x ≤ key₂ y))
       (hcap₁ : (view₁ s₁).length ≤ fuel₁) (hcap₂ : (view₂ s₂).length ≤ fuel₂)
       (hfuel : (view₁ s₁).length + (view₂ s₂).length < controlFuel) :
       (StreamJoin.run read₁ key₁ read₂ key₂ (remember hit) B fuel₁ fuel₂ controlFuel s₁ s₂ false).user = true ↔
         ∃ x ∈ view₁ s₁, ∃ y ∈ view₂ s₂, key₁ x = key₂ y ∧ hit x y = true := by
   …

   Mentions: OAI.LowSpaceSubsetSum.RowMerge.IsReader, OAI.LowSpaceSubsetSum.StreamJoin.run, OAI.LowSpaceSubsetSum.StreamWitness.remember

6. theorem OAI.LowSpaceSubsetSum.StreamWitness.stopped_sound line 62

   Source documentation

   An arbitrary stopped control prefix also has one-sided soundness.

   theorem stopped_sound {σ₁ σ₂ : Type*}
       (read₁ : σ₁ → Option (α × σ₁)) (key₁ : α → ℤ)
       (read₂ : σ₂ → Option (β × σ₂)) (key₂ : β → ℤ) (hit : α → β → Bool)
       (view₁ : σ₁ → List α) (hread₁ : RowMerge.IsReader read₁ view₁)
       (view₂ : σ₂ → List β) (hread₂ : RowMerge.IsReader read₂ view₂)
       (B fuel₁ fuel₂ controlFuel : ℕ) (s₁ : σ₁) (s₂ : σ₂)
       (hsort₁ : (view₁ s₁).Pairwise (fun x y => key₁ x ≤ key₁ y))
       (hsort₂ : (view₂ s₂).Pairwise (fun x y => key₂ x ≤ key₂ y))
       (hcap₁ : (view₁ s₁).length ≤ fuel₁) (hcap₂ : (view₂ s₂).length ≤ fuel₂)
       (hyes : (StreamJoin.run read₁ key₁ read₂ key₂ (remember hit) B fuel₁ fuel₂
         controlFuel s₁ s₂ false).user = true) :
       ∃ x ∈ view₁ s₁, ∃ y ∈ view₂ s₂, key₁ x = key₂ y ∧ hit x y = true := by
   …

   Mentions: OAI.LowSpaceSubsetSum.RowMerge.IsReader, OAI.LowSpaceSubsetSum.StreamJoin.run, OAI.LowSpaceSubsetSum.StreamWitness.remember