You are an expert Lean4 and formal verification agent proving a Lean4 theorem. Your output **must** strictly adhere to the specified format.

### Input Information
You will receive the following components, relevant to the target theorem:
* <all_available_defs>: Definitions available from imported modules (either from the current Lean repository or from Mathlib)
* <all_available_lemmas>: Lemmas/theorems available that may assist the proof.
* <local_ctx>...</local_ctx>: The local file context (imports, namespaces, definitions, comments, etc.) from the top of the file up to—but not including—the target theorem or any previously defined local lemmas/theorems.
* <target_theorem>...</target_theorem>: The target theorem statement, ending with `:=`.

**Notes**
1. Definitions include their full bodies, but for definitions whose bodies contain proofs, the proof parts are replaced by `admit` (i.e., admit /- proof elided -/), while the rest of the definition is kept unchanged; lemmas include only their statements.
2. You may freely reference any definition or lemma contained in these tags without redefining them.
3. The tags for available definitions and lemmas (all_available_defs, all_available_lemmas) may be omitted if empty.

### Output Format & Requirements
Your output MUST contain a complete, syntactically correct Lean 4 proof for the target theorem.

**Strict Output Structure:**
<reasoning> 
...
</reasoning> 

<lean4_invented_lemmas>
-- each lemma is a full Lean 4 declaration with a complete proof
...
</lean4_invented_lemmas>

<lean4_proof>
-- Lean 4 proof body of the target theorem
...
</lean4_proof>

**Requirements:**
1. <reasoning> and <lean4_invented_lemmas> are OPTIONAL. Include them only if they aid proof construction.
2. <lean4_proof> MUST contain only the proof body (tactics/terms), starting by "by", NOT the theorem declaration.
3. <lean4_invented_lemmas> (if present) MUST contain syntactically correct lemma declarations that type checks AND complete proof bodies. Defining a lemma using `axiom` is NOT allowed.
4. <reasoning> contains high-level proof planning.
5. If you create a lemma under <lean4_invented_lemmas> whose name is namespaced (e.g., X.Y.Z), you MUST always refer to it using its fully qualified name. Do NOT rely on shortened names. For example, write rw [X.Y.Z], not rw [Z] for invented lemmas.
6. All Lean 4 code MUST be syntactically correct. No `sorry`, `admit`, or non-Lean text. Comments allowed using `--` or `/- ... -/`.
7. Follow the tags and structure EXACTLY. No extra text before, between, or after the sections.
8. Do NOT wrap invented lemmas in a `mutual` block unless they have genuine mutual recursion. Declare each lemma independently.

### Examples are provided here (example input are under "User Prompt", and example assistant response are under "Agent Response"):
Example 1 ------------------- 
User Prompt:
<all_available_defs>
structure BitVec (w : Nat) where
  /-- Construct a `BitVec w` from a number less than `2^w`.
  O(1), because we use `Fin` as the internal representation of a bitvector. -/
  ofFin ::

  /-- Interpret a bitvector as a number less than `2^w`.
  O(1), because we use `Fin` as the internal representation of a bitvector. -/
  toFin : Fin (hPow 2 w)
</all_available_defs>

<all_available_lemmas>
theorem List.getElem_append_left{α : Type u_1} {l₁ l₂ : List α} {i : Nat} (hn : i < l₁.length) : (l₁ ++ l₂)[i] = l₁[i]
theorem getElem_eq_testBit_toNat (x : BitVec w) (i : Nat) (h : i < w) :
  x[i] = x.toNat.testBit i := rfl
@[simp, grind =] theorem toNat_cons (b : Bool) (x : BitVec w) :
    (cons b x).toNat = (b.toNat <<< w) ||| x.toNat
@[simp, grind =] theorem getLsbD_of_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getLsbD x i = false
theorem testBit_toNat (x : BitVec w) : x.toNat.testBit i = x.getLsbD i
</all_available_lemmas>

<local_ctx>
import Mathlib.Computability.NFA
import Mathlib.Data.FinEnum
import Mathlib.Data.Rel
import Mathlib.Data.Vector.Basic
import Blase.AutoStructs.ForLean

open Set
open Mathlib
open SetRel

-- this is better because card is defeq to n
instance (α : Type) : Inter (Language α) := ⟨Set.inter⟩
instance (α : Type) : Union (Language α) := ⟨Set.union⟩

/--
The set of `n`-tuples of bit vectors of an arbitrary width.
-/
structure BitVecs (n : Nat) where
  w : Nat
  bvs : List.Vector (BitVec w) n

def BitVecs.cast (bvs : BitVecs n) (h : n = n') : BitVecs n' :=
  { w := bvs.w, bvs := h ▸ bvs.bvs }

abbrev BitVecs.empty : BitVecs n := ⟨0, List.Vector.replicate n .nil⟩
abbrev BitVecs.singleton {w : Nat} (bv : BitVec w) : BitVecs 1 := ⟨w, bv ::ᵥ .nil⟩
abbrev BitVecs.pair {w : Nat} (bv1 bv2 : BitVec w) : BitVecs 2 := ⟨w, bv1 ::ᵥ bv2 ::ᵥ .nil⟩

/--
The set of `n`-tuples of bit vectors of an arbitrary width, encoded as a list of
bit vectors of width `n`. The width of the encoded bit vectors is the length of
the list.
-/
abbrev BitVecs' (n : Nat) := List (BitVec n)

@[simps]
def dec (bvs' : BitVecs' n) : BitVecs n where
  w := bvs'.length
  bvs := List.Vector.ofFn fun k => BitVec.ofFn fun i => bvs'[i].getLsbD k

@[simp]
</local_ctx>

<target_theorem>
lemma dec_snoc n (bvs' : BitVecs' n) (a : BitVec n) :
  dec (bvs' ++ [a]) =
    { w := bvs'.length + 1
      bvs := List.Vector.ofFn fun k =>
        BitVec.cons (a.getLsbD k) ((dec bvs').bvs.get k) } :=
</target_theorem>

Agent Response:
<reasoning> 
The goal is to understand what `dec` does after appending one more bitvector `a` to `bvs'`. By definition, `dec` builds a width `= length` and a vector of bitvectors whose `i`-th bit at position `k` is `bvs'[i].getLsbD k`. So for `bvs' ++ [a]`, we expect the width to increase by 1 and each resulting bitvector to be `BitVec.cons` of the new bit coming from `a`.

First, I use `ext` twice: once on the record to focus on the `bvs` field, and once on the resulting bitvector. This reduces everything to a pointwise statement:
for fixed `k` and `i` with `i < bvs'.length + 1`,
the bit `(bvs' ++ [a])[i].getLsbD k` should match the bit at index `i` of `BitVec.cons (a.getLsbD k) ((dec bvs').bvs.get k)`.

At this point I need a clean description of indexing into `BitVec.cons`: if we have `x : BitVec n`, then `(cons b x)[i]` should give `b` at the new “last” index `n` and `x[i]` otherwise. That motivates an auxiliary lemma `getElem_cons` expressing exactly this behavior, proved via the `testBit`/`toNat` characterization and a case split on `i < n`, `i = n`, `i > n`.

Using `getElem_cons`, the RHS becomes an `if` on whether `i = bvs'.length`. So I split into cases:
- If `i = bvs'.length`, then `(bvs' ++ [a])[i]` is the appended `a`, so both sides reduce to `a.getLsbD k`.
- If `i ≠ bvs'.length`, the bound `i < bvs'.length + 1` forces `i < bvs'.length`. Then `(bvs' ++ [a])[i] = bvs'[i]` by `List.getElem_append_left`, and the RHS takes the “else” branch and likewise gives the bit from `bvs'[i]`. In both subcases, `simp` (plus the definition of `dec`) finishes.

So the whole proof is: `ext` to bit level, unfold `dec` with `simp_all`, rewrite with `getElem_cons`, split on the boundary index `i = length bvs'`, and in the “< length” branch use `List.getElem_append_left` and bounds to line up both sides.
</reasoning> 

<lean4_invented_lemmas>
@[grind =]
theorem getElem_cons {b : Bool} {n} {x : BitVec n} {i : Nat} (h : i < n + 1) :
    (cons b x)[i] = if h : i = n then b else x[i] := by
  simp only [BitVec.getElem_eq_testBit_toNat, BitVec.toNat_cons, Nat.testBit_or]
  rw [Nat.testBit_shiftLeft]
  rcases Nat.lt_trichotomy i n with i_lt_n | i_eq_n | n_lt_i
  · have p1 : ¬(n ≤ i) := by omega
    have p2 : i ≠ n := by omega
    simp [p1, p2]
  · simp only [i_eq_n, ge_iff_le, Nat.le_refl, decide_true, Nat.sub_self, Nat.testBit_zero,
    Bool.true_and, BitVec.testBit_toNat, BitVec.getLsbD_of_ge, Bool.or_false]
    cases b <;> trivial
  · have p1 : i ≠ n := by omega
    have p2 : i - n ≠ 0 := by omega
    simp [p1, p2, Nat.testBit_bool_toNat]
</lean4_invented_lemmas>

<lean4_proof>
by
  ext k i hi <;> simp_all
  rw [getElem_cons]
  split
  next heq => simp_all
  next h =>
    have hlt : i < List.length bvs' := by simp at hi; omega
    rw [List.getElem_append_left hlt]
    simp
</lean4_proof>

### Your task:
<all_available_defs>
inductive FreeMonad (f : Type u → Type v) (α : Type w) : Type (max (u + 1) v w)
  | protected pure (x : α) : FreeMonad f α
  | roll {β : Type u} (x : f β) (r : β → FreeMonad f α) : FreeMonad f α

def OracleSpec (ι : Type u) : Type (max u (v + 1)) :=
  (i : ι) → Type v × Type v

@[inline, reducible]
protected def domain (spec : OracleSpec ι) (i : ι) : Type v := (spec i).1

@[inline, reducible]
protected def range (spec : OracleSpec ι) (i : ι) : Type w := (spec i).2

structure List.Zipper (α : Type u) where
  left   : List α 
  focus  : α      
  right  : List α

DFunLike in Mathlib.Data.FunLike.Basic

Decidable.isTrue in Init.Prelude

instance instOfLawfulMonadLiftT {m n} [Monad m] [Monad n] [MonadLiftT m n] [LawfulMonadLiftT m n] :
    LawfulMonadRelation m n where
  monadRel_pure _ := by admit /- proof elided -/

def XComp : X ◃ P ≃ₚ P where
  equivA := (_root_.Equiv.uniqueSigma _).trans (Equiv.punitArrowEquiv P.A)
  equivB := fun _ => by admit /- proof elided -/

def bitvec_to_string (bv : BitVec 256) : String :=
  let rec chars (n : Nat) (acc : List Char) :=
    if n = 0 then acc
    else chars (n / 256) (Char.ofNat (n % 256) :: acc)
  String.mk (chars bv.toNat [])

def prodZero :
    Lens.Equiv.{max uA₁ uA₂, max uB₁ uB₂, uA₁, uB₁} (P * (0 : PFunctor.{uA₂, uB₂})) 0 where
  toLens := (fun a => PEmpty.elim a.2) ⇆ (fun _ x => PEmpty.elim x)
  invLens := PEmpty.elim ⇆ (fun pe _ => PEmpty.elim pe)
  left_inv := by admit /- proof elided -/

noncomputable instance hasEvalDist : HasEvalDist PMF where
  evalDist p := OptionT.mk p
  evalDist_pure _ := by admit /- proof elided -/

def Hybrid_1 : ProbComp Bool := do
  let b ←$ᵗ Bool
  let A ←$ᵗ Matrix (Fin n) (Fin m) (Fin p)
  let u ←$ᵗ Vector (Fin p) m
  let ⟨m₁, m₂, st⟩ ← adv.chooseMessages (A, u)
  let c ← if b then (uniformRegevAsymmEnc n m p χ he).encrypt (A, u) m₁
    else (uniformRegevAsymmEnc n m p χ he).encrypt (A, u) m₂
  let b' ← adv.distinguish st c
  return b = b'

def pi {I : Type v} (F : I → PFunctor.{uA, uB}) : PFunctor.{max uA v, max uB v} :=
  ⟨(i : I) → (F i).A, fun f => Σ i, (F i).B (f i)⟩

@[trans]
def trans {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}}
    (e₁ : P ≃ₗ Q) (e₂ : Q ≃ₗ R) : P ≃ₗ R :=
  ⟨e₂.toLens ∘ₗ e₁.toLens, e₁.invLens ∘ₗ e₂.invLens,
    by admit /- proof elided -/
      ⟩

instance : Functor Zipper where
  map := map

class MonadIso (m : Type u → Type v) (n : Type u → Type w) where
  toLift : MonadLiftT m n
  invLift : MonadLiftT n m
  monadLift_left_inv {α : Type u} :
    Function.LeftInverse (toLift.monadLift (α := α)) (invLift.monadLift (α := α))
  monadLift_right_inv {α : Type u} :
    Function.RightInverse (toLift.monadLift (α := α)) (invLift.monadLift (α := α))

def pure (x : α) : HoareState (PreCondition.top σ) α (fun s a s' => s = s' ∧ a = x)
  | ⟨s, h⟩ => ⟨(x, s), by admit /- proof elided -/
  ⟩

instance : Extract NonEmptyList where
  extract := NonEmptyList.head_nel

ReaderT in Init.Prelude

MonadState.get in Init.Prelude

Array.flatMapM in Init.Data.Array.Basic

MonadLift.monadLift in Init.Prelude

instance subSpec_append_right : spec₂ ⊂ₒ (spec₁ ++ₒ spec₂) where
  monadLift | query i t => query (inr i) t

Unit in Init.Prelude

instance {P : PreCondition σ} {comp : StateM σ α} :
    Subsingleton (StrongestPostcondition P comp) :=

Classical.decEq in Mathlib.Logic.Basic

List.zip in Init.Data.List.Basic

Option in Init.Prelude

pure_bindᵣ {α β : Type u} (x : j α) (f : j α → m β) :
    (pureᵣ x) >>=ᵣ f = f x

def DijkstraMonad.dMap {w d} [Monad w] [DijkstraMonad w d] {α β} {a : w α} (f : α → β) :
    d a → d (a >>= fun b => pure (f b)) := fun x => x >>=ᵈ (fun a => dPure (f a))

class LawfulRelativeMonad (j : Type u → Type w) (m : Type u → Type v)
    [RelativeMonad j m] extends LawfulRelativeFunctor j m where

TopologicalSpace in Mathlib.Topology.Defs.Basic

@[simp] protected def default : ExecutionMethod ProbComp where
  exec := id
  lift_probComp := id
  exec_lift_probComp _ := rfl

instance : MonadFunctor f (FreeMonad f) where
  monadMap g
    | FreeMonad.pure x => FreeMonad.pure x
    | FreeMonad.roll x r => g x >>= r

instance instLawfulFunctor [Comonad w] [LawfulFunctor w] : LawfulFunctor (StoreT s w) where
  id_map := by admit /- proof elided -/

structure NatEquiv (m : Type u → Type v) (n : Type u → Type w) where
  toFun : {α : Type u} → m α → n α
  invFun : {α : Type u} → n α → m α
  left_inv : ∀ {α}, Function.LeftInverse (@invFun α) (@toFun α) := by admit /- proof elided -/

structure Lens (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) where
  toFunA : P.A → Q.A
  toFunB : ∀ a, Q.B (toFunA a) → P.B a

class Monad.AssertAssume (m : Type u → Type v) [∀ α, Preorder (m α)] where
  assert_assume {α} : _root_.AssertAssume (m α)

def MonoStateContProp (σ : Type u) := MonoCont (σ → Prop)

instance [MonadTransformer t] [Monad m] [LawfulMonad m] [LawfulMonadTransformer t]
    : LawfulMonadLift m (t m) where
  monadLift_pure := LawfulMonadTransformer.liftOf_pure
  monadLift_bind := LawfulMonadTransformer.liftOf_bind

instance instOfMonadLiftT {m n} [MonadLiftT m n] : MonadRelation m n where
  monadRel := fun ma na => liftM ma = na

LawfulAlternative in Batteries.Control.AlternativeMonad

Function.update in Mathlib.Logic.Function.Basic

Matrix.mulVec in Mathlib.Data.Matrix.Mul

MonadStateOf.modifyGet in Init.Prelude

def comp {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}}
    (l : Lens Q R) (l' : Lens P Q) : Lens P R where
  toFunA := l.toFunA ∘ l'.toFunA
  toFunB := fun i => (l'.toFunB i) ∘ l.toFunB (l'.toFunA i)

outParam in Init.Prelude

instance : LawfulMonad (OracleComp spec) :=
  inferInstanceAs (LawfulMonad (OptionT (FreeMonad (OracleQuery spec))))

AddGroup in Mathlib.Algebra.Group.Defs

instance : LawfulFunctor (Prod ε) where
  id_map := by admit /- proof elided -/

def takeAtIndex [DecidableEq ι] (seed : QuerySeed spec) (i : ι) (n : ℕ) : QuerySeed spec :=
  Function.update seed i ((seed i).take n)

instance decidablePred_mem_finSupport [spec.DecidableEq] [spec.FiniteRange] [DecidableEq α]
    (oa : OracleComp spec α) : DecidablePred (· ∈ oa.finSupport) :=

@[simp] def head_nel (nel : NonEmptyList α) : α := nel.head

instance [Monad m] [LawfulMonad m] : LawfulMonadLift m (FreeContT f m) where
  monadLift_pure := by admit /- proof elided -/

DecidableEq in Init.Prelude

Vector.get in Init.Data.Vector.Basic

def zeroTensor : 0 ⊗ P ≃ₚ 0 where
  equivA := Equiv.pemptyProd P.A
  equivB := fun a => Equiv.pemptyProd (P.B a.2)

ExceptT in Init.Control.Except

instance (n : ℕ) : SelectableType (BitVec n) where
  selectElem := ofFin <$> ($ᵗ Fin (2 ^ n))
  mem_support_selectElem x := by admit /- proof elided -/

Stream'.drop in Mathlib.Data.Stream.Defs

Set.image2 in Mathlib.Data.Set.Operations

@[always_inline, inline]
protected def bind : FreeM P α → (α → FreeM P β) → FreeM P β
  | FreeM.pure x, g => g x
  | FreeM.roll x r, g => FreeM.roll x (λ u ↦ FreeM.bind (r u) g)

PMF in Mathlib.Probability.ProbabilityMassFunction.Basic

Equiv.pemptyArrowEquivPUnit in Mathlib.Logic.Equiv.Defs

def prodOne :
    Lens.Equiv.{max uA₁ uA₂, max uB₁ uB₂, uA₁, uB₁} (P * (1 : PFunctor.{uA₂, uB₂})) P where
  toLens := Prod.fst ⇆ (fun _ => Sum.inl)
  invLens := (fun p => (p, PUnit.unit)) ⇆ (fun _ => Sum.elim id PEmpty.elim)
  left_inv := by admit /- proof elided -/

Fin.castLE in Init.Data.Fin.Basic

inductive FreeDijkstra (m : Type u → Type v) [Monad m] : {α : Type u} → m α → Type _ where
  | protected pure {α} (x : α) : FreeDijkstra m (pure x)
  | roll {α β} (x : m α) {f : α → m β} (r : α → FreeDijkstra m (x >>= f)) : FreeDijkstra m (x >>= f)

def map (f : α → β) : NonEmptyList α → NonEmptyList β
  | ⟨h, t⟩ => ⟨f h, List.map f t⟩

def ulift {P : PFunctor.{uA, uB}} : P.ulift ≃ₗ P where
  toLens := (fun a => ULift.down a) ⇆ (fun _ b => ULift.up b)
  invLens := (fun a => ULift.up a) ⇆ (fun _ b => ULift.down b)
  left_inv := rfl
  right_inv := rfl

def zip : NonEmptyList α → NonEmptyList β → NonEmptyList (α × β)
  | ⟨h₁, t₁⟩, ⟨h₂, t₂⟩ => ⟨(h₁, h₂), List.zip t₁ t₂⟩

instance [IsEmpty I] {F : I → PFunctor.{u}} : IsEmpty (sigma F).A :=

instance : DecidableEq mock_hmac_sha256_out_type :=
  fun x y => match String.decEq x y with
  | isTrue h => isTrue h
  | isFalse h => isFalse h

instance : Inhabited (OracleSpec ι) := ⟨λ _ ↦ (PUnit, PUnit)⟩

def activeOracles [spec.FiniteRange] [DecidableEq ι] (oa : OracleComp spec α) : Finset ι :=

instance : Coe (BindHom m n) (NatHom m n) where
  coe f := f.toNatHom

alias PKE_Alg := AsymmEncAlg

instance {ρ} {m} [Monad m] [Commutative m] : Commutative (ReaderT ρ m) where
  bind_comm := fun ma mb => by admit /- proof elided -/

def generateSingleSeed (spec : OracleSpec ι) (i : ι) [SelectableType (spec.range i)]
    (n : ℕ) : ProbComp (QuerySeed spec) :=
  QuerySeed.ofList <$> ($ᵗ spec.range i).replicate n

@[elab_as_elim]
protected def construct {C : OracleComp spec α → Type*}
    (pure : (a : α) → C (pure a))
    (query_bind : {β : Type v} → (q : OracleQuery spec β) →
      (oa : β → OracleComp spec α) → ((u : β) → C (oa u)) → C (q >>= oa))
    (failure : C failure) (oa : OracleComp spec α) : C oa :=
  FreeMonad.construct (Option.rec failure pure) query_bind oa

def instFunctorOfRelativeMonad {j : Type u → Type w} [Functor j] {m : Type u → Type v}
    [RelativeMonad j m] : Functor m where
  map f x := bindᵣ (j := j) x (pureᵣ ∘ (Functor.map f))

protected def mapM [Pure m] [Bind m] :
    (oa : FreeMonad f α) → (s : {α : Type u} → f α → m α) → m α
  | .pure x, _ => pure x
  | .roll x r, s => s x >>= λ u ↦ (r u).mapM s

structure AbuseReport where
  message : SecretMessage
  franking_tag : FrankingTag
  reporting_tag : ReportingTag
  context : Context
  deriving Repr

def validate_abuse_report (report : AbuseReport) (facebook_key : BitVec 256) : Bool :=
  let (msg_bv, _) := serialize_message_data report.message.content report.message.nonce
  let computed_tf := mock_hmac_sha256 report.message.nonce msg_bv
  let context_bv := BitVec.ofNat 256 report.context.timestamp
  let serialized := report.franking_tag.tag.append (bitvec_to_string context_bv)
  let computed_rf := mock_hmac_sha256 facebook_key (string_to_bitvec serialized)
  (computed_tf = report.franking_tag.tag) && (computed_rf = report.reporting_tag.tag)

structure BindEquiv (m : Type u → Type v) [Bind m] (n : Type u → Type w) [Bind n]
    extends NatEquiv m n where
  map_bind' {α β : Type u} (x : m α) (y : α → m β) :
    toFun (x >>= y) = toFun x >>= (fun a => toFun (y a))

instance : coinSpec.FiniteRange where
  range_inhabited' := inferInstance
  range_fintype' := inferInstance

LE.le in Init.Prelude

structure ExecutionMethod (m : Type u → Type v) where
    exec {α : Type u} : m α → ProbComp α
    lift_probComp {α : Type u} : ProbComp α → m α
    exec_lift_probComp {α : Type u} (px : ProbComp α) :
      exec (lift_probComp px) = px

def toChart (e : P ≃ₚ Q) : Chart P Q where
  toFunA := e.equivA
  toFunB := fun a => e.equivB a

Equiv.Perm in Mathlib.Logic.Equiv.Defs

NatPow in Init.Prelude

class IsUpperClosed (m : Type u → Type v) (n : Type u → Type w) [Monad m] [OrderedMonad n]
    [MonadRelation m n] where
  monadRel_upper_closed {α} {ma : m α} {na na' : n α} (hr : ma ∼ₘ na) (hn : na ≤ₘ na') : ma ∼ₘ na'

Nat in Init.Prelude

def LHL_Consequence_Adv (n p : ℕ) := (Vector (Fin p) n) × (Fin p) → ProbComp Bool

instance {w d} [Monad w] [DijkstraMonad w d] : MonadRelation (fun α => (w : w α) × d w) w :=
  instOfMonadLiftT

@[always_inline, inline]
protected def bind : FreeMonad f α → (α → FreeMonad f β) → FreeMonad f β
  | FreeMonad.pure x, g => g x
  | FreeMonad.roll x r, g => FreeMonad.roll x (λ u ↦ FreeMonad.bind (r u) g)

ExceptT.lift in Init.Control.Except

Append in Init.Prelude

def fst {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} :
    Lens.{max uA₁ uA₂, max uB₁ uB₂, uA₁, uB₁} (P * Q) P :=
  Prod.fst ⇆ (fun _ => Sum.inl)

def zeroProd :
    Lens.Equiv.{max uA₁ uA₂, max uB₁ uB₂, uA₁, uB₁} ((0 : PFunctor.{uA₂, uB₂}) * P) 0 where
  toLens := (fun ⟨pa, _⟩ => PEmpty.elim pa) ⇆ (fun _ x => PEmpty.elim x)
  invLens := PEmpty.elim ⇆ (fun pe _ => PEmpty.elim pe)
  left_inv := by admit /- proof elided -/

Turing.TM2ComputableInPolyTime in Mathlib.Computability.TMComputable

instance : Coe (PureHom m n) (NatHom m n) where
  coe f := f.toNatHom

def extract (t : CofreeC F α) : α :=
  head t

def uliftUliftEquiv : P.ulift.ulift ≃ₚ P.ulift :=
  sorry

private def lawLargeNumsTest (trials : ℕ) (die : ℕ) : IO Unit := do
  let n : ℕ := trials * die
  let xs ← OracleComp.replicateTR n $[0..die - 1]
  IO.println ("Rolling " ++ toString n ++ " " ++ toString die ++ "-sided dice:")
  for i in List.range die do
    IO.println <| "▸Num " ++ toString (i + 1) ++ "s: " ++ toString (xs.count i)

@[inline, reducible] def unifSpec : OracleSpec.{0,0} ℕ :=
  λ n ↦ (Unit, Fin (n + 1))

associator in Mathlib.Algebra.Ring.Associator

structure ReportingTag where
  tag : mock_hmac_sha256_out_type 
  deriving Repr

CategoryTheory.NatTrans in Mathlib.CategoryTheory.NatTrans

Sum.map in Init.Data.Sum.Basic

instance {T U : Type v} [DecidableEq T] [DecidableEq U] : (T →ₒ U).DecidableEq where
  domain_decidableEq' := inferInstance
  range_decidableEq' := inferInstance

instance instComonad [Comonad w] : Comonad (StoreT s w) where

def ofList [DecidableEq ι] {i : ι} (xs : List (spec.range i)) : QuerySeed spec :=
  fun j => if h : i = j then h ▸ xs else []

class LawfulMonadState (σ : outParam (Type u)) (m : Type u → Type v) [Monad m] :
    Type (max (u+1) v) extends MonadState σ m where

def tildeL {P : PFunctor.{uA, uB}} : Lens P (X ◃ P) :=
  (fun a => ⟨PUnit.unit, fun _ => a⟩) ⇆ (fun _a => fun ⟨_, b⟩ => b)

def rightKanExtension {α β : Type u} (f : w β) (p : w α) :=
  { ext : β → w α // f >>= ext ≤ₘ p ∧ (∀ w', f >>= w' ≤ₘ p → ∀ a, w' a ≤ₘ ext a) }

def signingOracle (sigAlg : SignatureAlg m M PK SK S) (pk : PK) (sk : SK) :
    QueryImpl (M →ₒ S) (WriterT (QueryLog (M →ₒ S)) m) :=
  QueryImpl.withLogging ⟨fun | query () msg => sigAlg.sign pk sk msg⟩

def sigmaProdDistrib : (sigma F * P : PFunctor.{max uA₁ uA₂ v, max uB₁ uB₂}) ≃ₚ
    sigma (fun i => (F i * P : PFunctor.{max uA₁ uA₂, max uB₁ uB₂})) where
  equivA := sorry
  equivB := sorry

def generate_reporting_tag (franking_tag : FrankingTag) (context : Context)
    (facebook_key : BitVec 256) : ReportingTag :=
  
  let context_bv := BitVec.ofNat 256 context.timestamp
  let serialized := franking_tag.tag.append (bitvec_to_string context_bv)
  let rf_tag := mock_hmac_sha256 facebook_key (string_to_bitvec serialized)
  { tag := rf_tag }

instance : NatPow PFunctor.{max uA uB, uB} where
  pow := compNth

get_set : {s : σ} → (do set (m := m) s; MonadStateOf.get) = do set s; pure s

instance : Extract Zipper where
  extract := extract

instance range_decidableEq {i : ι} [h : spec.DecidableEq] :
    DecidableEq (spec.range i) := h.range_decidableEq' i

Finset.sum in Mathlib.Algebra.BigOperators.Group.Finset.Defs

def rangeDecidableEq [spec.DecidableEq] : OracleQuery spec α → DecidableEq α
  | query i t => inferInstance

noncomputable def ProbComp.advantage₂' (p q : ProbComp Bool) : ℝ :=
  |([= true | p]).toReal - ([= true | q]).toReal|

def parallelTestingAdversary (_G P : Type) := P → P → P → P → ProbComp Bool

def purePower (B : Type uB) : PFunctor.{uA, uB} :=
  PUnit X^ B

Monad in Init.Prelude

def tensor (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) :
    PFunctor.{max uA₁ uA₂, max uB₁ uB₂} :=
  ⟨P.A × Q.A, fun ab => P.B ab.1 × Q.B ab.2⟩

structure EncryptedMessage where
  ciphertext : BitVec 256
  deriving Repr

def punitSigma {F : PUnit → PFunctor.{uA, uB}} : sigma F ≃ₚ F PUnit.unit where
  equivA := _root_.Equiv.uniqueSigma _
  equivB := sorry

class MonadLift.LE (m : Type u → Type v) (n : Type u → Type w) [Monad m] [OrderedMonad n]
    [φ : MonadLift m n] [ψ : MonadLift m n] where
  monadLift_le {α} (a : m α) : φ.monadLift a ≤ₘ ψ.monadLift a

def parallelizationExp [DecidableEq P]
    (adversary : parallelizationAdversary G P) : ProbComp Unit := do
  let x ←$ᵗ P; let g₁ ←$ᵗ G; let g₂ ←$ᵗ G
  let x₁ := g₁ +ᵥ x
  let x₂ := g₂ +ᵥ x
  let x₃ ← adversary x x₁ x₂
  guard (x₃ = g₁ +ᵥ g₂ +ᵥ x)

def withPregen (so : QueryImpl spec m) : QueryImpl spec (ReaderT spec.QuerySeed m) where
  impl | query i t => do
    let seed ← read
    do match seed i with
      | u :: us => ReaderT.adapt (fun seed => seed.update i us) (return u)
      | [] => so.impl (query i t)

class LawfulMonadControlT (m : Type u → Type v) (n : Type u → Type w)
    [Monad m] [Monad n] [MonadControlT m n] : Prop where

@[inline, reducible]
def rename (spec : OracleSpec ι) (f : τ → ι) : OracleSpec τ := spec ∘ f

class LawfulMonadAlgebra (m : Type u → Type v) [Monad m] [MonadAlgebra m] where
  monadAlg_pure {α : Type u} (a : α) : monadAlg (pure a : m α) = a
  monadAlg_bind {α β : Type u} (ma : m α) (mb : α → m β) :
    monadAlg (mb (monadAlg ma)) = monadAlg (ma >>= mb)

def fixState {S : Type u} : Lens (selfMonomial S) (selfMonomial S ◃ selfMonomial S) :=
  (fun s₀ => ⟨s₀, fun s₁ => s₁⟩) ⇆ (fun _s₀ => fun ⟨_s₁, s₂⟩ => s₂)

def generate_franking_tag (nonce : BitVec 256) (msg : String) : FrankingTag :=
  let (msg_bv, _) := serialize_message_data msg nonce
  let tf := mock_hmac_sha256 nonce msg_bv 
  { tag := tf }

HPow in Init.Prelude

def QueryCache (spec : OracleSpec ι) : Type u :=
  (i : ι) → spec.domain i → Option (spec.range i)

@[reducible, inline]
def CorrectExp (encAlg : AsymmEncAlg m M PK SK C) (msg : M) :
    ProbComp Unit := encAlg.exec do
  let (pk, sk) ← encAlg.keygen
  guard (encAlg.decrypt sk (← encAlg.encrypt pk msg) = msg)

def HoareState (P : PreCondition σ) (α : Type*) (Q : PostCondition σ α) :=
  ∀ s : {s : σ // P s}, {result : α × σ // Q s result.1 result.2}

Finset.image₂ in Mathlib.Data.Finset.NAry

instance (i : PEmpty) : Unique ([]ₒ.domain i) := PUnit.instUnique

liftWith_pure {α : Type u} (a : α) :
    MonadControl.liftWith (m := m) (n := n) (fun _ => pure a) = pure a

def Hybrid_01_Reduction : LWE_Adversary n m p := fun Au => do
  let b ←$ᵗ Bool
  let ⟨m₁, m₂, st⟩ ← adv.chooseMessages Au
  let c ← if b then (uniformRegevAsymmEnc n m p χ he).encrypt Au m₁
  else (uniformRegevAsymmEnc n m p χ he).encrypt Au m₂
  let b' ← adv.distinguish st c
  return b'

instance {a} : Unique (B X a) := inferInstanceAs (Unique PUnit)

def IND_CCA_oracleSpec (_encAlg : AsymmEncAlg m M PK SK C) :=
    (C →ₒ Option M) ++ₒ ((M × M) →ₒ C)

Cont in Mathlib.Control.Monad.Cont

OptionT.mk in Init.Control.Option

Functor.map in Init.Prelude

local instance instPreorderProp : Preorder Prop where
  le := fun p q => p → q
  le_refl := fun p => id
  le_trans := fun p q r h1 h2 => h2 ∘ h1

instance : Coseq Stream' where
  coseq := Stream'.zip Prod.mk

PFunctor.M in Mathlib.Data.PFunctor.Univariate.M

Finset.filter in Mathlib.Data.Finset.Filter

List in Init.Prelude

Summable in Mathlib.Topology.Algebra.InfiniteSum.Defs

Finset.card in Mathlib.Data.Finset.Card

class MonadRelationHom (m₁ : Type u → Type v₁) (n₁ : Type u → Type w₁)
    (m₂ : Type u → Type v₂) (n₂ : Type u → Type w₂) where
  monadRelHomFst {α : Type u} : m₁ α → m₂ α
  monadRelHomSnd {α : Type u} : n₁ α → n₂ α

class Comonad (w : Type u → Type v) extends Coapplicative w, Extend w where
   
  map f wa := extend wa (f ∘ extract)
   
  coseq wa wb := extend wa (fun wa' => (extract wa', extract wb))

instance : Coapplicative NonEmptyList where

@[simp] def negligible_iff (f : ℕ → ℝ≥0∞) :
    negligible f ↔ SuperpolynomialDecay atTop (λ x ↦ ↑x) f := Iff.rfl

instance instLawfulCoapplicative [Comonad w] [LawfulCoapplicative w] : LawfulCoapplicative (EnvT e w) where
  
  coseqLeft_eq := by admit /- proof elided -/

instance {σ : Type*} : PartialOrder (PreCondition σ) where
  le P₁ P₂ := ∀ s, P₂ s → P₁ s
  le_refl P := by admit /- proof elided -/

def xTensor : X ⊗ P ≃ₗ P where
  toLens := Prod.snd ⇆ (fun _ b => (PUnit.unit, b))
  invLens := (fun p => (PUnit.unit, p)) ⇆ (fun _ bp => bp.2)
  left_inv := rfl
  right_inv := rfl

instance : IsEmpty (0 ◃ P).A where
  false := fun a => a.1.elim

liftM in Init.Prelude

def rangeFintype [spec.FiniteRange] : OracleQuery spec α → Fintype α
  | query i t => inferInstance

def withCounting (so : QueryImpl spec m) : QueryImpl spec (WriterT spec.QueryCount m) where
  impl | q => tell (QueryCount.single q.index) *> ↑(so.impl q)

instance : Comonad NonEmptyList where

instance (n : ℕ) : SelectableType (Fin (n + 1)) where
  selectElem := $[0..n]
  mem_support_selectElem := by admit /- proof elided -/

@[simp]
def duplicate {α : Type u} (wa : w α) : w (w α) :=
  extend wa id

def oneComp : (1 : PFunctor.{uA, uB}) ◃ P ≃ₚ 1 where
  equivA := (@_root_.Equiv.uniqueSigma _ (fun i => B 1 i → P.A)
    (instUniqueAOfNat_toMathlib.{uA, uB})).trans (Equiv.pemptyArrowEquivPUnit _)
  equivB := fun _ => Equiv.equivPEmpty _

Eq in Init.Prelude

instance support_fintype [spec.FiniteRange] [DecidableEq α] (oa : OracleComp spec α) :
    Fintype ↥oa.support :=

def supportWhen (oa : OracleComp spec α)
    (possible_outputs : {α : Type v} → OracleQuery spec α → Set α) : Set α :=

instance instMonadSigma {w d} [Monad w] [DijkstraMonad w d] :
    Monad (fun α => (w : w α) × d w) where
  pure x := ⟨pure x, dPure x⟩
  bind x f := ⟨x.1 >>= (fun a => (f a).1), x.2 >>=ᵈ (fun a => (f a).2)⟩

instReprString in Init.Data.Repr

def equivState (so : QueryImpl spec (StateT σ (OracleComp spec'))) (e : σ ≃ τ) :
    QueryImpl spec (StateT τ (OracleComp spec')) where
  impl q s := map id e <$> so.impl q (e.symm s)

instance subSpec_assoc : spec₁ ++ₒ (spec₂ ++ₒ spec₃) ⊂ₒ spec₁ ++ₒ spec₂ ++ₒ spec₃ where
  monadLift
    | query (inl i) t => query (inl (inl i)) t
    | query (inr (inl i)) t => query (inl (inr i)) t
    | query (inr (inr i)) t => query (inr i) t

def snd {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} :
    Lens.{max uA₁ uA₂, max uB₁ uB₂, uA₂, uB₂} (P * Q) Q :=
  Prod.snd ⇆ (fun _ => Sum.inr)

@[inherit_doc] scoped[PFunctor] infixr:80 " X^ " => monomial

structure forkInput (spec : OracleSpec ι) (α : Type) where
   
  main : OracleComp spec α
   
  queryBound : ι → ℕ
   
  js : List ι

def sigmaSumDistrib (F : I → PFunctor.{uA₂, uB₁}) :
    (sigma F + P : PFunctor.{max uA₁ uA₂ v, uB₁}) ≃ₚ
    sigma (fun i => (F i + P : PFunctor.{max uA₁ uA₂, uB₁})) where
  equivA := by admit /- proof elided -/

MonadControl.liftWith in Init.Control.Basic

Finset in Mathlib.Data.Finset.Defs

instance : LawfulCoapplicative NonEmptyList where
  coseqLeft_eq := by admit /- proof elided -/

instance {n : Type u → Type v} [MonadLiftT m n] : MonadLiftT (FreeContT f m) (FreeContT f n) where
  monadLift := fun x => fun handleEff handlePure => by admit /- proof elided -/

class SubSpec (spec : OracleSpec.{u,w} ι) (superSpec : OracleSpec τ)
  extends MonadLift (OracleQuery spec) (OracleQuery superSpec) where

Decidable.isFalse in Init.Prelude

Vector.zipWith in Init.Data.Vector.Basic

MonadControlT in Init.Control.Basic

def invTildeL {P : PFunctor.{uA, uB}} : Lens (X ◃ P) P :=
  (fun ⟨_, f⟩ => f PUnit.unit) ⇆ (fun _ b => ⟨PUnit.unit, b⟩)

CategoryTheory.EnrichedCategory in Mathlib.CategoryTheory.Enriched.Basic

@[inline, reducible] def cachingOracle :
    QueryImpl spec (StateT spec.QueryCache (OracleComp spec)) :=
  idOracle.withCaching

Equiv.punitProd in Mathlib.Logic.Equiv.Prod

instance [RelativeFunctor Id f] : Functor f where
  map := @mapᵣ Id f _
  mapConst := @mapConstᵣ Id f _

protected def mapM {m : Type u → Type v} {n : Type u → Type w}
    [AlternativeMonad n] (f : {α : Type u} → m α → n α)
    {α : Type u} (x : OptionT m α) : n α :=
  do (← f x.run).getM

instance : Repr mock_hmac_sha256_out_type := instReprString

CategoryTheory.Functor.prod in Mathlib.CategoryTheory.Products.Basic

Set.fintypeiUnion in Mathlib.Data.Set.Finite.Lattice

MonadState in Init.Prelude

def prodMap {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}}
    {W : PFunctor.{uA₄, uB₄}} (l₁ : Lens P R) (l₂ : Lens Q W) :
    Lens.{max uA₁ uA₂, max uB₁ uB₂, max uA₃ uA₄, max uB₃ uB₄} (P * Q) (R * W) :=
  (fun pq => (l₁.toFunA pq.1, l₂.toFunA pq.2)) ⇆
    (fun pq => Sum.elim (Sum.inl ∘ l₁.toFunB pq.1) (Sum.inr ∘ l₂.toFunB pq.2))

@[inline, reducible]
def emptySpec : OracleSpec PEmpty := λ _ ↦ (PUnit, PUnit)

Option.elimM in Init.Data.Option.Basic

def trans (e₁ : NatEquiv m n) (e₂ : NatEquiv n p) : NatEquiv m p where
  toFun := e₂.toFun ∘ e₁.toFun
  invFun := e₁.invFun ∘ e₂.invFun
  left_inv := by admit /- proof elided -/

instance {comp : StateM σ α} {Q : PostCondition σ α} :
    Subsingleton (WeakestPrecondition comp Q) :=

def C (A : Type uA) : PFunctor.{uA, uB} :=
  A X^ PEmpty

Nat.succ in Init.Prelude

Sum in Init.Core
</all_available_defs>

<all_available_lemmas>
@[simp] lemma input_query (i : ι) (t : spec.domain i) : (query i t).input = t

@[simp]
lemma mock_decrypt_mock_encrypt (msg : BitVec 256) :
    mock_decrypt (mock_encrypt msg) = msg

@[simp]
theorem fst_comp_prodMap (l₁ : Lens P R) (l₂ : Lens Q W) :
    Lens.fst ∘ₗ (l₁ ×ₗ l₂) = l₁ ∘ₗ Lens.fst

@[simp]
lemma bind_roll (a : P.A) (r : P.B a → FreeM P β) (g : β → FreeM P γ) :
    FreeM.bind (FreeM.roll a r) g = FreeM.roll a (λ u ↦ FreeM.bind (r u) g)

lemma countQ_singleton_self (i : ι) (t : spec.domain i) (u : spec.range i) :
    countQ (singleton (query i t) u) i = 1

theorem bind_eq_pmf_bind {p : SPMF α} {f : α → SPMF β} :
    (p >>= f) = PMF.bind p (fun a => match a with | some a' => f a' | none => PMF.pure none)

@[simp] lemma support_bind (oa : OracleComp spec α) (ob : α → OracleComp spec β) :
    (oa >>= ob).support = ⋃ x ∈ oa.support, (ob x).support

lemma probEvent_eq_tsum_subtype : [p | oa] = ∑' x : {x | p x}, [= x | oa]

lemma neverFails_eq_oracleComp_construct (oa : OracleComp spec α) :
    oa.neverFails = OracleComp.construct
      (fun _ ↦ True) (fun {β} _ _ r ↦ ∀ (x : β), r x) False oa

@[simp]
lemma PMF.monad_bind_eq_bind {α β : Type u}
      (p : PMF α) (q : α → PMF β) : p >>= q = p.bind q

@[simp]
theorem get_rule_basic :
    HoareTriple (fun _ => True) (get : StateM σ σ) (fun s x s' => s = x ∧ s = s')

@[simp] lemma finSupport_bind (oa : OracleComp spec α) (ob : α → OracleComp spec β)
    [hα : DecidableEq α] [hβ : DecidableEq β] [spec.FiniteRange] :
    (oa >>= ob).finSupport = oa.finSupport.biUnion (λ x ↦ (ob x).finSupport)

@[simp]
lemma finSupport_generateSeed_ne_empty [DecidableEq spec.QuerySeed] :
    (generateSeed spec qc js).finSupport ≠ ∅

@[simp] lemma probOutput_ne_top : [= x | oa] ≠ ∞

@[simp]
lemma probFailure_eq_zero_iff (oa : OracleComp spec α) : [⊥ | oa] = 0 ↔ oa.neverFails

@[simp]
lemma probEvent_pure (p : α → Prop) [DecidablePred p] :
    [p | (pure x : OracleComp spec α)] = if p x then 1 else 0

@[simp]
lemma getQ_cons (log : QueryLog spec) (q : (i : ι) × spec.domain i × spec.range i) (i : ι) :
    getQ (q :: log) i =
      if h : q.1 = i then h ▸ (q.2.1, q.2.2) :: getQ log i else getQ log i

@[simp]
lemma snd_map_prod_map (oa : OracleComp spec (α × β)) (f : α → γ) (g : β → δ) :
    snd <$> map f g <$> oa = (g ∘ Prod.snd) <$> oa

lemma probFailure_bind_le_of_le_of_neverFails {oa : OracleComp spec α}
    (h' : oa.neverFails) {ob : α → OracleComp spec β} {r : ℝ≥0∞}
    (hr : ∀ x ∈ oa.support, [⊥ | ob x] ≤ r) : [⊥ | oa >>= ob] ≤ r

@[simp]
lemma probFailure_list_mapM {α β : Type*} [spec.FiniteRange] (xs : List α)
    (f : α → OracleComp spec β) : [⊥ | xs.mapM f] = 1 - (xs.map (1 - [⊥ | f ·])).prod

theorem get_get {α : Type u} {a : σ → σ → StateT σ m α} :
    (do let s₁ ← StateT.get; let s₂ ← StateT.get; a s₁ s₂) = (do let s ← StateT.get; a s s)

@[simp] lemma finSupportWhen_failure [DecidableEq α] :
    (failure : OracleComp spec α).finSupportWhen fin_poss = ∅

@[simp]
lemma bind_roll (x : f α) (r : α → FreeMonad f β) (g : β → FreeMonad f γ) :
    FreeMonad.bind (FreeMonad.roll x r) g = FreeMonad.roll x (λ u ↦ FreeMonad.bind (r u) g)

@[simp]
lemma FreeMonad.toFreeMonad_toFreeContM (x : FreeMonad f α) :
    FreeContM.toFreeMonad (FreeMonad.toFreeContM x) = x

theorem monadLift_optional [AlternativeMonad m] [AlternativeMonad n]
    [LawfulMonad m] [LawfulMonad n] [MonadLift m n] [LawfulAlternativeLift m n]
    [LawfulMonadLift m n]
    (x : m α) : monadLift (optional x) = optional (monadLift x : n α)

@[simp]
lemma mapM_roll (x : f α) (r : α → FreeMonad f β) :
    (FreeMonad.roll x r).mapM s = s x >>= λ u ↦ (r u).mapM s

theorem PMF.heq_iff {α β : Type u} {pa : PMF α} {pb : PMF β} (h : α = β) :
    HEq pa pb ↔ ∀ x, pa x = pb (cast h x)

@[simp]
lemma probOutput_bitVec_toFin_map {n : ℕ} (oa : OracleComp spec (BitVec n))
    (x : Fin (2 ^ n)) : [= x | toFin <$> oa] = [= ofFin x | oa]

@[simp]
lemma probFailure_failure : [⊥ | (failure : OracleComp spec α)] = 1

@[simp]
lemma support_seq_map_vector_cons : ((· ::ᵥ ·) <$> oa <*> ob).support =
    {xs | xs.head ∈ oa.support ∧ xs.tail ∈ ob.support}

@[simp]
lemma probOutput_bind_bind_prod_mk_eq_mul' [spec.FiniteRange] (oa : OracleComp spec α)
    (ob : OracleComp spec β) (f : α → γ) (g : β → δ) (x : γ) (y : δ) :
    [= (x, y) | do let x ← oa; let y ← ob; return (f x, g y)] =
      [= x | f <$> oa] * [= y | g <$> ob]

@[simp]
lemma liftM_append_right_eq (q : OracleQuery spec₂ α) :
    (liftM q : OracleQuery (spec₁ ++ₒ spec₂) α) =
      match q with

@[simp]
lemma simulate_coe_append_left [AlternativeMonad m₁] [LawfulMonad m₁] [LawfulAlternative m₁]
    [LawfulMonadLift m₁ n] [LawfulAlternativeLift m₁ n] (oa : OracleComp spec₁ α) :
    simulateQ (so ++ₛₒ so') (liftM oa) = (liftM (simulateQ so oa) : n α)

lemma probOutput_seq_map_eq_tsum [spec.FiniteRange]
    (z : γ) : [= z | f <$> oa <*> ob] = ∑' (x : α) (y : β),
      [= x | oa] * [= y | ob] * [= z | (pure (f x y) : OracleComp spec γ)]

@[simp]
theorem sumMap_comp_inr (l₁ : Lens P R) (l₂ : Lens Q W) :
    ((l₁ ⊎ₗ l₂) ∘ₗ Lens.inr) = (Lens.inr ∘ₗ l₂)

@[simp]
theorem map_mk [Functor f] [Functor g] {α : Type u₁} {β : Type u₂} {a b : Type u₃} (k : a → b) (map' : α → β → a) (fa : f α) (gb : g β) :
  k <$> (⟨map', fa, gb⟩ : Day f g a) = ⟨fun x y => k (map' x y), fa, gb⟩

theorem bind_comm_quad_swap_23 {m} [Monad m] [LawfulMonad m] [Commutative m] {α β γ δ ε}
    (ma : m α) (mb : m β) (mc : m γ) (md : m δ) (f : α × β × γ × δ → m ε) :
    (ma >>= fun a => mb >>= fun b => mc >>= fun c => md >>= fun d => f (a, b, c, d)) =
    (ma >>= fun a => mc >>= fun c => mb >>= fun b => md >>= fun d => f (a, b, c, d))

@[simp]
lemma evalDist_seq (oa : OracleComp spec α) (og : OracleComp spec (α → β)) :
    evalDist (og <*> oa) = evalDist og <*> evalDist oa

@[simp]
lemma probOutput_seq_map_swap [spec.FiniteRange] (z : γ) :
    [= z | Function.swap f <$> ob <*> oa] = [= z | f <$> oa <*> ob]

@[simp] lemma monoid_mul_def (qc qc' : QueryCount spec) :
  (@HMul.hMul _ _ _ (@instHMul _ (Monoid.toMulOneClass.toMul)) qc qc')
     = (qc : ι → ℕ) + (qc' : ι → ℕ)

@[simp] lemma evalDist_ite (p : Prop) [Decidable p] (mx mx' : m α) :
    evalDist (if p then mx else mx') = if p then evalDist mx else evalDist mx'

lemma abs_mul_of_nonneg (h : 0 ≤ b) : |a

lemma probEvent_fst_eq_snd [spec.FiniteRange] [DecidableEq α] (oa : OracleComp spec (α × α)) :
    [λ z ↦ z.1 = z.2 | oa] = ∑' x : α, [= (x, x) | oa]

lemma List.countP_eq_sum_fin_ite {α : Type*} (xs : List α) (p : α → Bool) :
    (∑ i : Fin xs.length, if p xs[i] then 1 else 0) = xs.countP p

@[simp]
lemma liftComp_map (oa : OracleComp spec α) (f : α → β) :
    liftComp (f <$> oa) superSpec = f <$> liftComp oa superSpec

@[simp] lemma neverFails_list_mapM {f : α → OracleComp spec β} {as : List α}
    (h : ∀ x ∈ as, neverFails (f x)) : neverFails (mapM f as)

@[simp]
lemma Fin_bound_castLE {n m : ℕ} {x : Fin (n + 1)} {h : n < m} :
  Fin_Bound (Fin.castLE h x) n

@[simp] lemma probOutput_ne_top : Pr[= x | mx] ≠ ∞

@[simp] lemma tsum_run_some_ne_top (p : SPMF α) :
    ∑' x, p.run (some x) ≠ ⊤

@[simp]
lemma probFailure_orElse {ι : Type u} {spec : OracleSpec ι} {α : Type u} [h : spec.FiniteRange]
    (oa oa' : OracleComp spec α) : [⊥ | oa <|> oa'] = [⊥ | oa] * [⊥ | oa']

lemma tsum_option {α β : Type*} [AddCommMonoid α] [TopologicalSpace α]
    [ContinuousAdd α] [T2Space α]
    (f : Option β → α) (hf : Summable (Function.update f none 0)) :
    ∑' x : Option β, f x = f none + ∑' x : β, f (some x)

@[simp]
theorem comp_id {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} (f : Lens P Q) :
    f ∘ₗ (Lens.id P) = f

lemma probEvent_seq_eq_tsum_ite [spec.FiniteRange] (p : β → Prop) [DecidablePred p] :
    [p | og <*> oa] = ∑' (g : α → β) (x : α),
      if p (g x) then [= g | og] * [= x | oa] else 0

lemma probOutput_ne_zero (h : x ∈ oa.support) : [= x | oa] ≠ 0

@[simp]
lemma neverFails_pure (x : α) : neverFails (pure x : OracleComp spec α)

@[simp]
lemma probEvent_failure (p : α → Prop) :
    [p | (failure : OracleComp spec α)] = 0

@[simp]
theorem ulift_B {a : P.A} : (P.ulift).B (ULift.up a) = ULift (P.B a)

@[simp] lemma probEvent_eq_eq_probOutput (oa : OracleComp spec α) (x : α) :
    [(· = x) | oa] = [= x | oa]

lemma probOutput_bind_congr_div_const {oa : OracleComp spec α}
    {ob₁ ob₂ : α → OracleComp spec β} {y : β} {r : ℝ≥0∞}
    (h : ∀ x ∈ oa.support, [= y | ob₁ x] = [= y | ob₂ x] / r) :
    [= y | oa >>= ob₁] = [= y | oa >>= ob₂] / r

@[simp] lemma PerfectlyCorrect_iff (encAlg : AsymmEncAlg m M PK SK C) :
    PerfectlyCorrect encAlg ↔ ∀ (msg : M),
      [⊥ | CorrectExp encAlg msg] = 0

@[simp] lemma withCaching_apply {α} (so : QueryImpl spec m) (q : OracleQuery spec α) :
    so.withCaching.impl q = match q with

lemma ProbComp.advantage_eq_half_of_sub (p : ProbComp Unit) :
    p.advantage = 2⁻¹ * |([⊥ | p]).toReal - ([= () | p]).toReal

lemma probOutput_prod_mk_apply_seq_map_eq_mul' [spec.FiniteRange] (oa : OracleComp spec α)
    (ob : OracleComp spec β)
    (f : α → γ) (g : β → δ) (x : γ) (y : δ) :
    [= (x, y) | (f ·, g ·) <$> oa <*> ob] = [= x | f <$> oa] * [= y | g <$> ob]

lemma mem_finSupport_iff_of_evalDist_eq [spec.DecidableEq] [spec'.DecidableEq]
    [DecidableEq α] {oa : OracleComp spec α} {oa' : OracleComp spec' α}
    (h : evalDist oa = evalDist oa') (x : α) : x ∈ oa.finSupport ↔ x ∈ oa'.finSupport

@[simp] lemma toExecutionMethod_eq (n : ℕ) :
    (oneTimePad n).toExecutionMethod = ExecutionMethod.default

lemma list_mapM_loop_eq {m : Type u → Type v} [Monad m] [LawfulMonad m]
    {α : Type w} {β : Type u} (xs : List α) (f : α → m β) (ys : List β) :
    List.mapM.loop f xs ys = (ys.reverse ++ ·) <$> List.mapM.loop f xs []

@[simp] lemma probFailure_uniformSelectList (xs : List α) :
    [⊥ | $ xs] = if xs.isEmpty then 1 else 0

@[simp]
lemma fst_map_prod_mk_of_subsingleton [Subsingleton β]
    (oa : OracleComp spec α) (y : β) : fst <$> (·, y) <$> oa = oa

@[simp] lemma X_A : X.A = PUnit

lemma simulateQ_eq [spec.FiniteRange] (oa : OracleComp spec α) :
    simulateQ defaultOracle oa = oa.defaultResult.getM

@[simp]
lemma liftM_query_writerT {ω : Type v} [Monoid ω] {α : Type v} (q : OracleQuery spec α) :
  (liftM q : WriterT ω (OracleComp spec) α) = liftM (liftM q : OracleComp spec α)

lemma probOutput_bind_eq_tsum (y : β) :
    Pr[= y | mx >>= my] = ∑' x : α, Pr[= x | mx] * Pr[= y | my x]

@[simp] lemma finSupport_query_bind [spec.FiniteRange] [Fintype α] [DecidableEq β]
    (q : OracleQuery spec α) (ob : α → OracleComp spec β) :
    (liftM q >>= ob).finSupport = Finset.univ.biUnion fun x => (ob x).finSupport

@[simp]
lemma mmap_seq [LawfulMonad m] [LawfulMonad n]
    (F : m →ᵐ n) (x : m (α → β)) (y : m α) : F (x <*> y) = F x <*> F y

@[simp] lemma finSupportWhen_bind (oa : OracleComp spec α) (ob : α → OracleComp spec β)
    [DecidableEq α] [DecidableEq β] :
    (oa >>= ob).finSupportWhen fin_poss =
      (oa.finSupportWhen fin_poss).biUnion fun x => (ob x).finSupportWhen fin_poss

lemma depth_bind_eq {x : FreeMonad f α} {g : α → FreeMonad f β} :
    depth (x >>= g) = depthBindAux x g

@[simp] lemma simulateQ_eq_getM_defaultResult [spec.FiniteRange] :
    @simulateQ ι spec _ α _ defaultOracle = Option.getM ∘ defaultResult

@[simp]
lemma range_index : (q : OracleQuery spec α) → spec.range q.index = α

lemma bind_def (x : WriterT ω m α) (f : α → WriterT ω m β) :
    x >>= f = WriterT.mk (x.run >>= fun (a, w₁) ↦
      (Prod.map id (w₁ * ·)) <$> (f a))

@[simp]
lemma Vector.getElem_eq_get {α n} (xs : List.Vector α n) (i : ℕ) (h : i < n) :
  xs[i]'h = xs.get ⟨i, h⟩

@[simp]
theorem prodComm_symm : (prodComm P Q).symm = prodComm Q P

@[simp]
lemma liftComp_bind (oa : OracleComp spec α) (ob : α → OracleComp spec β) :
    liftComp (oa >>= ob) superSpec =
      liftComp oa superSpec >>= λ x ↦ liftComp (ob x) superSpec

theorem map_eq_pure_bindᵣ [RelativeMonad j m] [LawfulRelativeMonad j m]
    (f : j α → j β) (x : m α) : f <$>ᵣ x = x >>=ᵣ fun a => pureᵣ (f a)

@[simp]
lemma probFailure_pos_iff (oa : OracleComp spec α) : 0 < [⊥ | oa] ↔ ¬ oa.neverFails

lemma probEvent_coin_eq_sum_subtype (p : Bool → Prop) :
    [p | coin] = ∑' _ : {x | p x}, 2⁻¹

@[simp]
lemma mapM_roll (x : P.A) (r : P.B x → FreeM P α) :
    (FreeM.roll x r).mapM s = s x >>= λ u ↦ (r u).mapM s

@[ext] lemma ext {p q : SPMF α} (h : ∀ x : α, p.run (some x) = q.run (some x)) : p = q :=
  PMF.ext fun

@[simp low]
lemma probEvent_eq_zero_iff : [p | oa] = 0 ↔ ∀ x ∈ oa.support, ¬ p x

@[simp]
lemma probFailure_run_simulateQ [spec.FiniteRange] (oa : OracleComp spec α) :
    [⊥ | (simulateQ countingOracle oa).run] = [⊥ | oa]

@[simp] lemma apply_eq [spec.FiniteRange] (q : OracleQuery spec α) :
    defaultOracle.impl q = return q.defaultOutput

@[simp]
lemma liftM_left_append_left_append_eq [h : spec₁ ⊂ₒ spec₃]
    (q : OracleQuery (spec₁ ++ₒ spec₂) α) : (liftM q : OracleQuery (spec₃ ++ₒ spec₂) α) =
    match q with

lemma probOutput_seq_eq_tsum [spec.FiniteRange] (y : β) : [= y | og <*> oa] =
    ∑' g, ∑' x, [= g | og] * [= x | oa] * [= y | (pure (g x) : OracleComp spec β)]

lemma mem_finSupport_bind_iff [spec.FiniteRange]
    (oa : OracleComp spec α) (ob : α → OracleComp spec β)
    [hoa : DecidableEq α] [hob : DecidableEq β] (y : β) : y ∈ (oa >>= ob).finSupport ↔
      ∃ x ∈ oa.finSupport, y ∈ (ob x).finSupport

lemma uniformSelectFinset_def {α : Type} [DecidableEq α] (s : Finset α) :
    ($ s) = ($ s.toList)

theorem pure_eq_pmf_pure {a : α} : (pure a : SPMF α) = PMF.pure a

@[simp]
lemma isQueryBound_query_iff_pos [Nonempty α] (q : OracleQuery spec α) (qb : ι → ℕ) :
    IsQueryBound (q : OracleComp spec α) qb ↔ 0 < qb q.index

@[simp]
theorem ulift_A : (P.ulift).A = ULift P.A

lemma probFailure_bind_congr' (oa : OracleComp spec α)
    {ob : α → OracleComp spec β} {oc : α → OracleComp spec γ}
    (h : ∀ x, [⊥ | ob x] = [⊥ | oc x]) : [⊥ | oa >>= ob] = [⊥ | oa >>= oc]

@[simp]
lemma takeAtIndex_addValues (seed : QuerySeed spec) {i : ι} (n : ℕ) (xs : List (spec.range i)) :
    (seed.addValues xs).takeAtIndex i n = if n ≤ (seed i).length
      then seed.takeAtIndex i n else seed.addValues (xs.take (n - (seed i).length))

@[simp]
lemma liftM_eq_liftComp (oa : OracleComp spec α) :
    (liftM oa : OracleComp superSpec α) = liftComp oa superSpec

@[simp]
lemma probOutput_pure_subsingleton [Subsingleton α] (x y : α) :
    [= x | (pure y : OracleComp spec α)] = 1

lemma probOutput_seq_map_vec_push_eq_mul {n : ℕ} {ova : OracleComp spec (Vector α n)} {va : Vector α n} :
    [= (va.push x) | Vector.push <$> ova <*> oa] = [= va | ova] * [= x | oa]

@[simp] theorem liftM_optional [AlternativeMonad m] [AlternativeMonad n]
    [LawfulMonad m] [LawfulMonad n] [MonadLift m n] [LawfulAlternativeLift m n]
    [LawfulMonadLift m n]
    (x : m α) : liftM (optional x) = optional (liftM x : n α)

lemma probFailure_writerT_run_simulateQ [spec.FiniteRange]
    {so : QueryImpl spec (WriterT ω (OracleComp spec))}
    (hso : ∀ {α}, ∀ q : OracleQuery spec α, fst <$> (so.impl q).run = q)
    (hso' : ∀ {α}, ∀ q : OracleQuery spec α, [⊥ | (so.impl q).run] = 0)
    (oa : OracleComp spec α) : [⊥ | (simulateQ so oa).run] = [⊥ | oa]

lemma probEvent_seq_map_eq_probEvent [spec.FiniteRange] (p : γ → Prop) :
    [p | f <$> oa <*> ob] = [λ z ↦ p (f z.1 z.2) | Prod.mk <$> oa <*> ob]

@[simp] lemma tsum_probOutput_le_one : ∑' x : α, Pr[= x | mx] ≤ 1

@[simp] theorem map_bindᵣ [RelativeMonad j m] [LawfulRelativeMonad j m]
    (f : j β → j γ) (x : m α) (g : j α → m β) :
      f <$>ᵣ (x >>=ᵣ g) = x >>=ᵣ fun a : j α => f <$>ᵣ g a

@[simp]
lemma BitVec.xor_xor_cancel_right {n : ℕ} (bv1 bv2 : BitVec n) :
    bv1 ^^^ bv2 ^^^ bv2 = bv1

lemma mem_support_bind_iff (oa : OracleComp spec α) (ob : α → OracleComp spec β) (y : β) :
    y ∈ (oa >>= ob).support ↔ ∃ x ∈ oa.support, y ∈ (ob x).support

@[simp] lemma probEvent_uniformSelectList (xs : List α) (p : α → Prop) [DecidablePred p] :
    [p | $ xs] = if xs.isEmpty then 0 else (xs.countP p : ℝ≥0∞) / xs.length

@[simp]
lemma replicate_pure (x : α) :
    (pure x : OracleComp spec α).replicate n = pure (List.replicate n x)

lemma probEvent_def (mx : m α) (p : α → Prop) :
    Pr[p | mx] = (evalDist mx).run.toOuterMeasure (some '' {x | p x})

@[simp]
lemma evalDist_ite (p : Prop) [Decidable p] (oa oa' : OracleComp spec α) :
    evalDist (if p then oa else oa') = if p then evalDist oa else evalDist oa'

@[simp]
lemma generateSeed_nil : generateSeed spec qc [] = return ∅

@[simp] theorem CommutativeAt.bind_comm_comp {m} [Monad m] [LawfulMonad m] {α β γ}
    (ma : m α) (mb : m β) (h : CommutativeAt m ma mb) (f : α × β → m γ) :
      (ma >>= fun a => mb >>= fun b => f (a, b)) = (mb >>= fun b => ma >>= fun a => f (a, b))

@[simp]
theorem vectorAdd_get {α : Type} {n : ℕ} [Add α] [Zero α]
 (vx : Vector α n) (vy : Vector α n)
 : (vx + vy).get = vx.get + vy.get

@[simp] lemma probFailure_eq : probFailure p = p.run none

@[simp low + 1]
lemma support_seq_map_eq_image2 :
    (f <$> oa <*> ob).support = Set.image2 f oa.support ob.support

@[simp]
lemma simulateQ_compose [LawfulMonad m] [LawfulAlternative m] (so' : QueryImpl spec' m)
    (so : QueryImpl spec (OracleComp spec'))
    (oa : OracleComp spec α) : simulateQ (so' ∘ₛ so) oa = simulateQ so' (simulateQ so oa)

@[simp]
lemma run_simulateQ_bind_fst (oa : OracleComp spec α) (ob : α → OracleComp spec β) :
    ((simulateQ loggingOracle oa).run >>= fun x => ob x.1) = oa >>= ob

lemma Fin_bound_dotprod {p m b₁ b₂ : ℕ} {v₁ v₂ : Vector (Fin p) m}
(h1 : Fin_Bound_vec v₁ b₁) (h2 : Fin_Bound_vec v₂ b₂) (Nez : NeZero p) :
  Fin_Bound (dotProduct v₁.get v₂.get) (b₁ * b₂ * m)

@[simp] lemma someWhen_pure (x : α) :
    (pure x : OracleComp spec α).someWhen Q F possible_outputs

@[simp] lemma supportWhen_bind (oa : OracleComp spec α) (ob : α → OracleComp spec β) :
    (oa >>= ob).supportWhen poss = ⋃ x ∈ oa.supportWhen poss, (ob x).supportWhen poss

theorem pure_rule_forward {P : PreCondition σ} (x : α) :
    HoareTriple P (pure x) (fun s a s' => s = s' ∧ a = x ∧ P s)

@[simp] lemma simulateQ_query (q : OracleQuery spec α) : simulateQ so q = so.impl q

@[simp] lemma apply_eq_run_some (p : SPMF α) (x : α) : p x = p.run (some x)

@[simp] theorem toMonadState_set_eq_monadStateOf_set {m : Type u → Type v} {σ : Type u}
    [MonadStateOf σ m] : (MonadState.set : σ → m PUnit) = MonadStateOf.set

@[simp]
lemma probFailure_list_mapM_loop {α β : Type*} [spec.FiniteRange]
    (xs : List α) (f : α → OracleComp spec β) (ys : List β) :
    [⊥ | List.mapM.loop f xs ys] = 1 - (xs.map (1 - [⊥ | f ·])).prod

lemma probOutput_map_eq_sum_fintype_ite [Fintype α] [DecidableEq β] (y : β) :
    [= y | f <$> oa] = ∑ x : α, if y = f x then [= x | oa] else 0

@[simp] theorem liftM_guard [AlternativeMonad m] [AlternativeMonad n] [MonadLift m n]
    [LawfulAlternativeLift m n] [LawfulMonadLift m n] (p : Prop) [Decidable p] :
    liftM (guard p : m Unit) = (guard p : n Unit)

@[simp] lemma apply_eq (q : OracleQuery spec α) : idOracle.impl q = q

lemma mem_finSupport_seq_map_cons_iff [spec.FiniteRange] [spec.DecidableEq] [DecidableEq α]
    (xs : List α) (h : xs ≠ []) : xs ∈ (cons <$> oa <*> ob).finSupport ↔
      xs.head h ∈ oa.finSupport ∧ xs.tail ∈ ob.finSupport

theorem strengthen_rule {P : PreCondition σ} {Q : PostCondition σ α}
    {comp : StateM σ α} (h : HoareTriple P comp Q) (Q' : PostCondition σ α)
    (h_imp : ∀ s x s', Q s x s' → Q' s x s') :
      HoareTriple P comp Q'

@[simp] theorem monadLift_mono' {m n} [OrderedMonad m] [OrderedMonad n] [OrderedMonadLiftT m n]
    {α} {a b : m α} (h : a ≤ₘ b) : monadLift a ≤ₘ (monadLift b : n α)

@[simp] lemma linear_A (A : Type u) : (linear A).A = A

@[simp]
lemma probFailure_replicate [spec.FiniteRange] :
    [⊥ | oa.replicate n] = 1 - (1 - [⊥ | oa]) ^ n

theorem isCorrect_of_uniformErrSamp [hm : NeZero m] (χ : ℕ) (he: p > 4*(χ*m + 1)) :
    (regevAsymmEnc n m p (uniformErrSamp χ (relax_p_bound he))).PerfectlyCorrect

lemma probOutput_map_eq_tsum (y : β) :
    [= y | f <$> oa] = ∑' x, [= x | oa] * [= y | (pure (f x) : OracleComp spec β)]

@[simp]
lemma finSupport_liftComp [spec.DecidableEq] [superSpec.DecidableEq] [DecidableEq α]
    [spec.FiniteRange] [superSpec.FiniteRange]
    (oa : OracleComp spec α) : (liftComp oa superSpec).finSupport = oa.finSupport

theorem modifyGet_eq_monadState {α : Type u} (f : σ → α × σ) :
    StateT.modifyGet (m := m) f = (do let (a, s) := f (← StateT.get); StateT.set s; pure a)

@[simp] lemma support_map_prod_map_fork : (Prod.map cf cf <$> main.fork qb js i cf).support =
    (fun s => (s, s)) '' (cf <$> main).support

lemma cons_mem_finSupport_seq_map_cons_iff [spec.FiniteRange] [spec.DecidableEq] [DecidableEq α]
    (x : α) (xs : List α) : x :: xs ∈ (cons <$> oa <*> ob).finSupport ↔
      x ∈ oa.finSupport ∧ xs ∈ ob.finSupport

@[simp]
lemma probFailure_guard {p : Prop} [Decidable p] :
    [⊥ | (guard p : OracleComp spec _)] = if p then 0 else 1

@[simp] lemma not_one_lt_probEvent : ¬ 1 < [p | oa]

@[simp] lemma probFailure_le_one : Pr[⊥ | mx] ≤ 1

@[simp]
lemma finSupport_seq_map_swap [spec.FiniteRange] [spec.DecidableEq] [DecidableEq γ] :
    (Function.swap f <$> ob <*> oa).finSupport = (f <$> oa <*> ob).finSupport

@[simp]
lemma neverFails_query (q : OracleQuery spec α) : neverFails (q : OracleComp spec α)

theorem RelativeFunctor.map_unitᵣ [RelativeMonad j m] [LawfulRelativeMonad j m] {a : m PUnit} :
    (fun y : j PUnit => y) <$>ᵣ a = a

@[simp] lemma probFailure_eq : probFailure p = 0

@[simp] lemma support_query (q : OracleQuery spec α) :
    (q : OracleComp spec α).support = Set.univ
</all_available_lemmas>

<local_ctx>
import ToMathlib.Control.Monad.Free

import ToMathlib.Control.WriterT

import ToMathlib.Control.AlternativeMonad

import ToMathlib.Control.OptionT

import Mathlib.Control.Lawful

import VCVio.OracleComp.OracleSpec

namespace OracleSpec

inductive OracleQuery {ι : Type u} (spec : OracleSpec.{u,v} ι) : Type v → Type (max u v)
  | query (i : ι) (t : spec.domain i) : OracleQuery spec (spec.range i)

namespace OracleQuery

variable {ι : Type u} {spec : OracleSpec ι} {α β : Type v}

end OracleQuery

end OracleSpec

open OracleSpec

def OracleComp {ι : Type u} (spec : OracleSpec.{u,v} ι) :
    Type w → Type (max u (v + 1) w) :=
  OptionT (FreeMonad (OracleQuery.{u,v} spec))

namespace OracleComp

variable {ι : Type u} {spec : OracleSpec ι} {α β : Type v}

section lift
</local_ctx>

<target_theorem>
lemma query_bind_eq_roll (q : OracleQuery spec α) (ob : α → OracleComp spec β) :
    (q : OracleComp spec α) >>= ob = OptionT.mk (FreeMonad.roll q ob) :=
</target_theorem>

