Query Bounds for Iteration Constructs #
This file lifts the structural query-bound predicates (IsTotalQueryBound,
IsQueryBoundP, IsPerIndexQueryBound) across the iteration combinators
OracleComp.replicate, OracleComp.replicateTR, List.mapM, and List.foldlM.
For the fixed-body case replicate n oa, the bound is exactly multiplicative —
we get an iff between the loop bound n * k and the body bound k (when
0 < n) for IsTotalQueryBound and IsQueryBoundP. The reverse direction
goes through isTotalQueryBound_iff_counting_total_le /
isQueryBoundP_iff_counting_filter_le and a witness lemma showing every
counting-oracle support point of oa lifts to an n-fold copy in
replicate n oa.
For the variable-body case (List.mapM / List.foldlM), only the forward
direction is available: the loop bound is the element-wise sum of body bounds.
Forward replicate bounds #
theorem
OracleComp.isTotalQueryBound_replicate
{ι : Type u}
{spec : OracleSpec ι}
{α : Type u}
{oa : OracleComp spec α}
{k : ℕ}
(h : oa.IsTotalQueryBound k)
(n : ℕ)
:
(replicate n oa).IsTotalQueryBound (n * k)
theorem
OracleComp.isQueryBoundP_replicate
{ι : Type u}
{spec : OracleSpec ι}
{α : Type u}
{oa : OracleComp spec α}
{p : ι → Prop}
[DecidablePred p]
{k : ℕ}
(h : oa.IsQueryBoundP p k)
(n : ℕ)
:
(replicate n oa).IsQueryBoundP p (n * k)
theorem
OracleComp.isPerIndexQueryBound_replicate
{ι : Type u}
{spec : OracleSpec ι}
{α : Type u}
[DecidableEq ι]
{oa : OracleComp spec α}
{qb : ι → ℕ}
(h : oa.IsPerIndexQueryBound qb)
(n : ℕ)
:
(replicate n oa).IsPerIndexQueryBound (n • qb)
Divide-trick iff for the fixed-body case #
When the body oa is fixed, the loop bound n * k is exactly characterized by the body
bound k: forward by isTotalQueryBound_replicate, reverse by lifting any
counting-oracle support point of oa to an n-fold copy in replicate n oa.
theorem
OracleComp.isTotalQueryBound_replicate_iff
{ι : Type u}
{spec : OracleSpec ι}
{α : Type u}
[Finite ι]
[spec.Inhabited]
{oa : OracleComp spec α}
{n k : ℕ}
(hn : 0 < n)
:
theorem
OracleComp.isQueryBoundP_replicate_iff
{ι : Type u}
{spec : OracleSpec ι}
{α : Type u}
[Finite ι]
[spec.Inhabited]
{oa : OracleComp spec α}
{p : ι → Prop}
[DecidablePred p]
{n k : ℕ}
(hn : 0 < n)
:
replicateTR corollaries #
theorem
OracleComp.isTotalQueryBound_replicateTR
{ι : Type u}
{spec : OracleSpec ι}
{α : Type u}
{oa : OracleComp spec α}
{k : ℕ}
(h : oa.IsTotalQueryBound k)
(n : ℕ)
:
(replicateTR n oa).IsTotalQueryBound (n * k)
theorem
OracleComp.isQueryBoundP_replicateTR
{ι : Type u}
{spec : OracleSpec ι}
{α : Type u}
{oa : OracleComp spec α}
{p : ι → Prop}
[DecidablePred p]
{k : ℕ}
(h : oa.IsQueryBoundP p k)
(n : ℕ)
:
(replicateTR n oa).IsQueryBoundP p (n * k)
theorem
OracleComp.isPerIndexQueryBound_replicateTR
{ι : Type u}
{spec : OracleSpec ι}
{α : Type u}
[DecidableEq ι]
{oa : OracleComp spec α}
{qb : ι → ℕ}
(h : oa.IsPerIndexQueryBound qb)
(n : ℕ)
:
(replicateTR n oa).IsPerIndexQueryBound (n • qb)
theorem
OracleComp.isTotalQueryBound_replicateTR_iff
{ι : Type u}
{spec : OracleSpec ι}
{α : Type u}
[Finite ι]
[spec.Inhabited]
{oa : OracleComp spec α}
{n k : ℕ}
(hn : 0 < n)
:
theorem
OracleComp.isQueryBoundP_replicateTR_iff
{ι : Type u}
{spec : OracleSpec ι}
{α : Type u}
[Finite ι]
[spec.Inhabited]
{oa : OracleComp spec α}
{p : ι → Prop}
[DecidablePred p]
{n k : ℕ}
(hn : 0 < n)
:
List.mapM and List.foldlM (forward only) #
theorem
OracleComp.isTotalQueryBound_listMapM
{ι : Type u}
{spec : OracleSpec ι}
{α β : Type u}
{f : α → OracleComp spec β}
{k : α → ℕ}
(h : ∀ (x : α), (f x).IsTotalQueryBound (k x))
(xs : List α)
:
(List.mapM f xs).IsTotalQueryBound (List.map k xs).sum
theorem
OracleComp.isTotalQueryBound_listMapM_const
{ι : Type u}
{spec : OracleSpec ι}
{α β : Type u}
{f : α → OracleComp spec β}
{k : ℕ}
(h : ∀ (x : α), (f x).IsTotalQueryBound k)
(xs : List α)
:
(List.mapM f xs).IsTotalQueryBound (xs.length * k)
theorem
OracleComp.isTotalQueryBound_listFoldlM
{ι : Type u}
{spec : OracleSpec ι}
{α β : Type u}
{f : β → α → OracleComp spec β}
{k : α → ℕ}
(h : ∀ (b : β) (x : α), (f b x).IsTotalQueryBound (k x))
(b₀ : β)
(xs : List α)
:
(List.foldlM f b₀ xs).IsTotalQueryBound (List.map k xs).sum
theorem
OracleComp.isQueryBoundP_listMapM
{ι : Type u}
{spec : OracleSpec ι}
{α β : Type u}
{f : α → OracleComp spec β}
{p : ι → Prop}
[DecidablePred p]
{k : α → ℕ}
(h : ∀ (x : α), (f x).IsQueryBoundP p (k x))
(xs : List α)
:
(List.mapM f xs).IsQueryBoundP p (List.map k xs).sum
theorem
OracleComp.isQueryBoundP_listMapM_const
{ι : Type u}
{spec : OracleSpec ι}
{α β : Type u}
{f : α → OracleComp spec β}
{p : ι → Prop}
[DecidablePred p]
{k : ℕ}
(h : ∀ (x : α), (f x).IsQueryBoundP p k)
(xs : List α)
:
(List.mapM f xs).IsQueryBoundP p (xs.length * k)
theorem
OracleComp.isQueryBoundP_listFoldlM
{ι : Type u}
{spec : OracleSpec ι}
{α β : Type u}
{f : β → α → OracleComp spec β}
{p : ι → Prop}
[DecidablePred p]
{k : α → ℕ}
(h : ∀ (b : β) (x : α), (f b x).IsQueryBoundP p (k x))
(b₀ : β)
(xs : List α)
:
(List.foldlM f b₀ xs).IsQueryBoundP p (List.map k xs).sum
theorem
OracleComp.isPerIndexQueryBound_listMapM
{ι : Type u}
{spec : OracleSpec ι}
{α β : Type u}
[DecidableEq ι]
{f : α → OracleComp spec β}
{qb : α → ι → ℕ}
(h : ∀ (x : α), (f x).IsPerIndexQueryBound (qb x))
(xs : List α)
:
(List.mapM f xs).IsPerIndexQueryBound (List.map qb xs).sum
theorem
OracleComp.isPerIndexQueryBound_listMapM_const
{ι : Type u}
{spec : OracleSpec ι}
{α β : Type u}
[DecidableEq ι]
{f : α → OracleComp spec β}
{qb : ι → ℕ}
(h : ∀ (x : α), (f x).IsPerIndexQueryBound qb)
(xs : List α)
:
(List.mapM f xs).IsPerIndexQueryBound (xs.length • qb)
theorem
OracleComp.isPerIndexQueryBound_listFoldlM
{ι : Type u}
{spec : OracleSpec ι}
{α β : Type u}
[DecidableEq ι]
{f : β → α → OracleComp spec β}
{qb : α → ι → ℕ}
(h : ∀ (b : β) (x : α), (f b x).IsPerIndexQueryBound (qb x))
(b₀ : β)
(xs : List α)
:
(List.foldlM f b₀ xs).IsPerIndexQueryBound (List.map qb xs).sum