Roll Bounds for the Free Monad of a Polynomial Functor

We define PFunctor.FreeM.IsRollBound oa budget canRoll cost, a generalized predicate that bounds the number of roll constructors a term oa : FreeM P α unfolds, parameterized by:

• B — the budget type
• budget : B — the initial budget
• canRoll : P.A → B → Prop — whether a roll at position a is allowed under budget b
• cost : P.A → B → B — how the budget is updated after a roll at a

The definition is structural via FreeM.construct: pure satisfies any bound, and roll a r satisfies the bound when canRoll a b holds and each continuation r y satisfies the bound at cost a b.

OracleComp.IsQueryBound (in VCVio/OracleComp/QueryTracking/QueryBound.lean) is the specialization of this predicate to FreeM (spec.toPFunctor) and is equal to IsRollBound definitionally; the bridge lemma in QueryBound.lean witnesses the equivalence by Iff.rfl.

def PFunctor.FreeM.IsRollBound {P : PFunctor.{uA, uB}} {α : Type v} {B : Type u_1} (oa : P.FreeM α) (budget : B) (canRoll : P.A → B → Prop) (cost : P.A → B → B) : Prop

Generalized roll bound on FreeM P parameterized by a budget type B, a validity check canRoll, and a cost function cost. pure satisfies any bound; roll a r satisfies the bound when canRoll a b holds and every continuation satisfies the bound at cost a b.

@[simp]

theorem PFunctor.FreeM.isRollBound_pure {P : PFunctor.{uA, uB}} {α : Type v} {B : Type u_1} (x : α) (b : B) (canRoll : P.A → B → Prop) (cost : P.A → B → B) : (pure x).IsRollBound b canRoll cost

@[simp]

theorem PFunctor.FreeM.isRollBound_roll_iff {P : PFunctor.{uA, uB}} {α : Type v} {B : Type u_1} (a : P.A) (r : P.B a → P.FreeM α) (b : B) (canRoll : P.A → B → Prop) (cost : P.A → B → B) : (roll a r).IsRollBound b canRoll cost ↔ canRoll a b ∧ ∀ (y : P.B a), (r y).IsRollBound (cost a b) canRoll cost

@[simp]

theorem PFunctor.FreeM.isRollBound_liftA_iff {P : PFunctor.{uA, uB}} {B : Type u_1} (a : P.A) (b : B) (canRoll : P.A → B → Prop) (cost : P.A → B → B) : (liftA a).IsRollBound b canRoll cost ↔ canRoll a b

@[simp]

theorem PFunctor.FreeM.isRollBound_map_iff {P : PFunctor.{uA, uB}} {α β : Type v} {B : Type u_1} (oa : P.FreeM α) (f : α → β) (b : B) (canRoll : P.A → B → Prop) (cost : P.A → B → B) : (f <$> oa).IsRollBound b canRoll cost ↔ oa.IsRollBound b canRoll cost

theorem PFunctor.FreeM.isRollBound_iff_of_map_eq {P : PFunctor.{uA, uB}} {α β : Type v} {B : Type u_1} {oa : P.FreeM α} {ob : P.FreeM β} {f : α → β} {b : B} (h : f <$> oa = ob) (canRoll : P.A → B → Prop) (cost : P.A → B → B) : oa.IsRollBound b canRoll cost ↔ ob.IsRollBound b canRoll cost

If f <$> oa = ob for any f, the roll-bound predicate transfers between them. The standard shape arises when oa and ob are two views of the same underlying computation that agree up to a projection.

theorem PFunctor.FreeM.isRollBound_congr {P : PFunctor.{uA, uB}} {α : Type v} {B : Type u_1} {oa : P.FreeM α} {b : B} {canRoll₁ canRoll₂ : P.A → B → Prop} {cost₁ cost₂ : P.A → B → B} (hcan : ∀ (a : P.A) (b : B), canRoll₁ a b ↔ canRoll₂ a b) (hcost : ∀ (a : P.A) (b : B), cost₁ a b = cost₂ a b) : oa.IsRollBound b canRoll₁ cost₁ ↔ oa.IsRollBound b canRoll₂ cost₂

theorem PFunctor.FreeM.IsRollBound.proj {P : PFunctor.{uA, uB}} {α : Type v} {B : Type u_1} {B' : Type u_2} (proj : B → B') {oa : P.FreeM α} {b : B} {canRoll : P.A → B → Prop} {cost : P.A → B → B} {canRoll' : P.A → B' → Prop} {cost' : P.A → B' → B'} (h_can : ∀ (a : P.A) (b' : B), canRoll a b' → canRoll' a (proj b')) (h_cost : ∀ (a : P.A) (b' : B), canRoll a b' → proj (cost a b') = cost' a (proj b')) (h : oa.IsRollBound b canRoll cost) : oa.IsRollBound (proj b) canRoll' cost'

Project an IsRollBound along a budget projection proj : B → B'.

If the source bound at budget b validates rolls at every step, the projected bound at proj b is also validated, provided:

• h_can — whenever a step is allowed in the source (canRoll a b'), it is allowed in the projection (canRoll' a (proj b'));
• h_cost — the projection commutes with the cost step on the allowed branch (proj (cost a b') = cost' a (proj b')).

theorem PFunctor.FreeM.isRollBound_bind {P : PFunctor.{uA, uB}} {α β : Type v} {B : Type u_1} {oa : P.FreeM α} {ob : α → P.FreeM β} {canRoll : P.A → B → Prop} {cost : P.A → B → B} (combine : B → B → B) {b₁ b₂ : B} (h_can : ∀ (a : P.A) (b₁' b₂' b : B), canRoll a b → canRoll a (combine b₁' b) ∧ canRoll a (combine b b₂')) (h_cost : ∀ (a : P.A) (b₁' b₂' b : B), canRoll a b → combine b₁' (cost a b) = cost a (combine b₁' b) ∧ cost a (combine b b₂') = combine (cost a b) b₂') (h₁ : oa.IsRollBound b₁ canRoll cost) (h₂ : ∀ (x : α), (ob x).IsRollBound b₂ canRoll cost) : (oa >>= ob).IsRollBound (combine b₁ b₂) canRoll cost

Generic bind composition for IsRollBound parameterised by an arbitrary budget type B and a binary combine operation on it.

The two side conditions are universally quantified so they survive recursion under generalizing b₁:

• h_can — extending any validated budget on either side via combine keeps the roll valid;
• h_cost — cost distributes left and right over combine on validated budgets.

theorem PFunctor.FreeM.isRollBound_seq {P : PFunctor.{uA, uB}} {α β : Type v} {B : Type u_1} {og : P.FreeM (α → β)} {oa : P.FreeM α} {canRoll : P.A → B → Prop} {cost : P.A → B → B} (combine : B → B → B) {b₁ b₂ : B} (h_can : ∀ (a : P.A) (b₁' b₂' b : B), canRoll a b → canRoll a (combine b₁' b) ∧ canRoll a (combine b b₂')) (h_cost : ∀ (a : P.A) (b₁' b₂' b : B), canRoll a b → combine b₁' (cost a b) = cost a (combine b₁' b) ∧ cost a (combine b b₂') = combine (cost a b) b₂') (h₁ : og.IsRollBound b₁ canRoll cost) (h₂ : oa.IsRollBound b₂ canRoll cost) : (og <*> oa).IsRollBound (combine b₁ b₂) canRoll cost

Forward-direction seq analogue of isRollBound_bind. Reduces to the bind case via seq_eq_bind_map plus isRollBound_map_iff.