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 α

@[always_inline, inline]
def lift (x : f α) : FreeMonad f α := FreeMonad.roll x FreeMonad.pure

@[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)

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

@[simp]
def map (f : α → β) (z : Zipper α) : Zipper β :=
  ⟨ List.map f z.left, f z.focus, List.map f z.right ⟩

structure FrankingTag where
  tag : mock_hmac_sha256_out_type 
  deriving Repr

LawfulFunctor in Init.Control.Lawful.Basic

Stream'.get in Mathlib.Data.Stream.Defs

PFunctor.comp in Mathlib.Data.PFunctor.Univariate.Basic

List.Vector.toList in Mathlib.Data.Vector.Defs

Fintype in Mathlib.Data.Fintype.Defs

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)

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

Vector.push in Init.Data.Vector.Basic

local instance instPreorderId {r} [h : Preorder r] : Preorder (id r) := h

CoeFun in Init.Coe

Num in Mathlib.Data.Num.Basic

instHMul in Init.Prelude

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 effectObserve (m : Type u → Type v) (α : Type u) := m α → (m α → Prop) → Prop

def probSpec : OracleSpec.{0,0} ℕ :=
  fun n => (ℕ, Fin (n + 1))

instance : LawfulMonad (FreeM P) :=
  LawfulMonad.mk' (FreeM P)
    (λ x ↦ by admit /- proof elided -/
      )
    (λ x f ↦ rfl)
    (λ x f g ↦ by admit /- proof elided -/
      )

def LWE_Distr : ProbComp (Matrix (Fin n) (Fin m) (Fin p) × Vector (Fin p) m) := do
  let A ←$ᵗ Matrix (Fin n) (Fin m) (Fin p)
  let s ←$ᵗ Vector (Fin p) n
  
  let e ← (Vector.range m).mapM (fun _ ↦ errSamp)
  let u := A.vecMul s.get + e.get
  return (A, Vector.ofFn u)

instance : Unique (A 1) := inferInstanceAs (Unique PUnit)

def mock_encrypt (msg : BitVec 256) : BitVec 256 :=
  msg ^^^ (BitVec.ofNat 256 0xABCDEF)

@[elab_as_elim]
protected def construct {C : FreeMonad f α → Type*}
    (pure : (x : α) → C (pure x))
    (roll : {β : Type u} → (x : f β) → (r : β → FreeMonad f α) →
      ((y : β) → C (r y)) → C (x >>= r)) :
    (oa : FreeMonad f α) → C oa
  | .pure x => pure x
  | .roll x r => roll x _ (λ u ↦ FreeMonad.construct pure roll (r u))

instance {Q : PostCondition σ σ} {x : σ} : WeakestPrecondition (pure x : StateM σ σ) Q := default

instance instLawfulComonad [Comonad w] [LawfulComonad w] : LawfulComonad (StoreT s w) where
  map_eq_extend_extract := sorry 
  extend_extract := sorry 
  extract_extend := by admit /- proof elided -/

Stream'.head in Mathlib.Data.Stream.Defs

def unzipCommits (x₀ pk : P) (zs : Vector G n)
    (hash : Vector Bool n) : Vector P n :=
  Vector.zipWith (λ z b ↦ if b then z +ᵥ pk else z +ᵥ x₀) zs hash

Filter.atTop in Mathlib.Order.Filter.AtTopBot.Defs

def speedup {S : Type u} {P : PFunctor.{uA, uB}} (l : Lens (selfMonomial S) P) :
    Lens (selfMonomial S) (P ◃ P) :=
  (l ◃ₗ l) ∘ₗ fixState

instance : Functor Stream' where
  map := Stream'.map

def tensorZero : P ⊗ 0 ≃ₗ 0 where
  toLens := (fun a => PEmpty.elim a.2) ⇆ (fun _ b => PEmpty.elim b)
  invLens := PEmpty.elim ⇆ (fun a _ => PEmpty.elim a)
  left_inv := by admit /- proof elided -/

CategoryTheory.aesop_cat in Mathlib.CategoryTheory.Category.Basic

instance : Inhabited (OracleComp spec α) := ⟨failure⟩

List.filterMap in Init.Data.List.Basic

StateM in Init.Control.State

BitVec.ofNat in Init.Prelude

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

dite in Init.Prelude

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

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

instance : Coseq NonEmptyList where
  coseq := NonEmptyList.zip

bind_assocᵣ {α β γ : Type u} (x : m α) (f : j α → m β) (g : j β → m γ) :
    x >>=ᵣ f >>=ᵣ g = x >>=ᵣ fun x ↦ f x >>=ᵣ g

instance subSpec_right_append_right_append_of_subSpec [h : spec₂ ⊂ₒ spec₃] :
    spec₁ ++ₒ spec₂ ⊂ₒ spec₁ ++ₒ spec₃ where
  monadLift
    | query (inl i) t => query (inl i) t
    | query (inr i) t => liftM (query i t)

NatPow in Init.Prelude

T2Space in Mathlib.Topology.Separation.Hausdorff

Set.indicator in Mathlib.Algebra.Notation.Indicator

def totalQueries [FiniteRange spec] {α : Type v} (oa : OracleComp spec α) : ℕ :=

instance {Q : PostCondition σ α} {x : α} :
    Inhabited (WeakestPrecondition (pure x : StateM σ α) Q) where
  default := ⟨fun s => Q s x s, HoareTriple.pure_rule_backward x, fun _ hP' => hP'⟩

instance : Extend Zipper where
  extend z f := map f (duplicate z)

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

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)

Finite in Mathlib.Data.Finite.Defs

instance [RelativePure Id f] : Pure f where
  pure := @pureᵣ Id f _

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)

def deserialize_message_data (data : BitVec 256 × BitVec 256) : String × BitVec 256 :=
  let (msg_bv, nonce) := data
  (bitvec_to_string msg_bv, nonce)

def perfectSecrecy (encAlg : SymmEncAlg m M K C) : Prop :=
  ∀ mgen : ProbComp M, ∀ msg : M, ∀ σ : C,
    [= (msg, σ) | encAlg.exec do
      let msg' ← encAlg.lift_probComp mgen
      (msg', ·) <$> encAlg.encrypt (← encAlg.keygen) msg'] =
    [= msg | mgen]

instance : LawfulComonad (Prod ε) where
  
  map_eq_extend_extract := by admit /- proof elided -/

def sumCompDistrib (Q : PFunctor.{uA₂, uB₁}) :
    (P + Q : PFunctor.{max uA₁ uA₂, uB₁}) ◃ R ≃ₚ
    ((P ◃ R) + (Q ◃ R) : PFunctor.{max uA₁ uA₂ uA₃ uB₁, max uB₁ uB₃}) where
  equivA := sorry
  equivB := sorry

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

def tails : NonEmptyList α → NonEmptyList (NonEmptyList α)
  | nel@⟨_, t⟩ =>
    
    let head_tail : NonEmptyList α := nel
    
    let rest_tails_list : List (NonEmptyList α) :=
      List.filterMap NonEmptyList.fromList? (List.tails t)
    ⟨head_tail, rest_tails_list⟩

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

def withCaching (so : QueryImpl spec m) : QueryImpl spec (StateT spec.QueryCache m) where
  impl | query i t => do match (← get) i t with
    | Option.some u => return u
    | Option.none =>
        let u ← so.impl (query i t)
        modifyGet fun cache => (u, cache.cacheQuery i t u)

instance : Monoid (QueryCount spec) where
  mul qc qc' := qc + qc'
  mul_assoc := add_assoc
  one := 0
  one_mul := zero_add
  mul_one := add_zero

guard in Init.Control.Basic

@[always_inline, inline]
def liftPos (a : P.A) : FreeM P (P.B a) := FreeM.roll a FreeM.pure

Functor in Init.Prelude

PEmpty.elim in Init.Core

def decrypt_message (encrypted_msg : EncryptedMessage) (nonce : BitVec 256) : String :=
  let decrypted_bv := mock_decrypt encrypted_msg.ciphertext
  let (msg, _) := deserialize_message_data (decrypted_bv, nonce)
  msg

def sumSumSumComm :
    ((P + Q) + (R + S) : PFunctor.{max uA₁ uA₂ uA₃ uA₄, uB}) ≃ₚ
    ((P + R) + (Q + S) : PFunctor.{max uA₁ uA₂ uA₃ uA₄, uB}) where
  equivA := _root_.Equiv.sumSumSumComm P.A Q.A R.A S.A
  equivB := (Sum.casesOn ·
    (Sum.casesOn · (fun _ => _root_.Equiv.refl _) (fun _ => _root_.Equiv.refl _))
    (Sum.casesOn · (fun _ => _root_.Equiv.refl _) (fun _ => _root_.Equiv.refl _)))

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 uniformErrSamp {p : ℕ} (χ : ℕ) (hχ : p > 2*χ) : ProbComp (Fin p) := do
  let e ←$ᵗ Fin (2*χ + 1)
  haveI : NeZero p := ⟨by admit /- proof elided -/
  ⟩
  return (Fin.castLE hχ e) - ⟨χ, by admit /- proof elided -/
  ⟩

PMF.toOuterMeasure in Mathlib.Probability.ProbabilityMassFunction.Basic

CategoryTheory.EnrichedFunctor.obj in Mathlib.CategoryTheory.Enriched.Basic

liftWith_restoreM {α : Type u} (t : n α) :
    liftWith (m := m) (fun run => run t) >>= restoreM = t

instance {β} : Unique (A (purePower β)) := inferInstanceAs (Unique PUnit)

AddGroup in Mathlib.Algebra.Group.Defs

class OrderedDijkstraMonad (w : Type u → Type v) (d : {α : Type u} → w α → Type z)
    [OrderedMonad w] extends DijkstraMonad w d where
  dWeaken {α} {wa wa' : w α} : d wa → (wa ≤ₘ wa') → d wa'
  dWeaken_refl {α} {wa : w α} (x : d wa) : dWeaken x (le_refl _) = x
  dWeaken_trans {α} {wa wa' wa'' : w α} (x : d wa) (h1 : wa ≤ₘ wa') (h2 : wa' ≤ₘ wa'') :
    dWeaken (dWeaken x h1) h2 = dWeaken x (le_trans h1 h2)
  dWeaken_dBind {α β} {wa wa' : w α} {f f' : α → w β} (x : d wa) (g : (a : α) → d (f a))
    (ha : wa ≤ₘ wa') (hf : ∀ a, f a ≤ₘ f' a) :
      (dWeaken x ha) >>=ᵈ (fun a => dWeaken (g a) (hf a)) = dWeaken (x >>=ᵈ g) (bind_mono ha hf)

@[inline, reducible] def coinSpec : OracleSpec.{0,0} Unit := Unit →ₒ Bool

instance : FiniteRange []ₒ where
  range_inhabited' := inferInstance
  range_fintype' := inferInstance

LawfulMonad in Init.Control.Lawful.Basic

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

def Hybrid_2 : ProbComp Bool := do
  let b ←$ᵗ Bool
  let A ←$ᵗ Matrix (Fin n) (Fin m) (Fin p)
  let u ←$ᵗ Vector (Fin p) m
  let ⟨_, _, st⟩ ← adv.chooseMessages (A, u)
  
  let c₁ ←$ᵗ Vector (Fin p) n
  let c₂ ←$ᵗ Fin p
  let b' ← adv.distinguish st (c₁, c₂)
  return b = b'

@[simp]
noncomputable def depthBindAux {f : Type u → Type v} {α β : Type u} :
    FreeMonad f α → (α → FreeMonad f β) → ℕ∞
  | .pure x, g => depth (g x)
  | .roll _ r, g => 1 + iSup (λ u ↦ depthBindAux (r u) g)

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

ULift in Init.Prelude

def tensorOne : P ⊗ 1 ≃ₚ C P.A where
  equivA := Equiv.prodPUnit P.A
  equivB := fun _ => Equiv.equivPEmpty _

Add in Init.Prelude

def IND_CPA_experiment {encAlg : AsymmEncAlg ProbComp M PK SK C}
    (adversary : encAlg.IND_CPA_adversary) : ProbComp Unit := do
  let b ← $ᵗ Bool
  let (pk, _sk) ← encAlg.keygen
  let b' ← (simulateQ (encAlg.IND_CPA_queryImpl' pk b) (adversary pk)).run' ∅
  guard (b = b')

def sumZero :
    Lens.Equiv.{max uA uA₁, uB, uA₁, uB} (P + (0 : PFunctor.{uA, uB})) P where
  toLens := Lens.sumPair (Lens.id P) Lens.initial
  invLens := Lens.inl
  left_inv := 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

class MonadTransformer (t : (Type u → Type v) → Type u → Type w) where
  [mapMonad (m) [Monad m] : Monad (t m)]
  [transform (m) [Monad m] : MonadLift m (t m)]

Classical.decEq in Mathlib.Logic.Basic

def LHL_Consequence_Game_1 (adv : LHL_Consequence_Adv n p) : ProbComp Bool := do
  let x ←$ᵗ Vector (Fin p) n
  let y ←$ᵗ Fin p
  adv (x, y)

def replicateTR {ι : Type u} {spec : OracleSpec ι} {α : Type v}
    (n : ℕ) (oa : OracleComp spec α) : OracleComp spec (List α) :=
  (List.replicateTR n ()).mapM fun () => oa

OptionT.instMonadFunctor in Init.Control.Option

alias coprod := sum

Bool in Init.Prelude

instance : LawfulMonad (FreeMonad f) :=
  LawfulMonad.mk' (FreeMonad f)
    (λ x ↦ by admit /- proof elided -/
      )
    (λ x f ↦ rfl)
    (λ x f g ↦ by admit /- proof elided -/
      )

def exp (P Q : PFunctor.{uA, uB}) : PFunctor.{max uA uB, max uA uB} :=
  pi (fun a => P ◃ (X + C (Q.B a)))

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

def liftComp (oa : OracleComp spec α) (superSpec : OracleSpec τ)
      [h : MonadLift (OracleQuery spec) (OracleQuery superSpec)] :
      OracleComp superSpec α := simulateQ ⟨liftM⟩ oa

MonadFunctor in Init.Prelude

Sum.inr in Init.Core

class IsMonadHom (m : Type u → Type v) [Pure m] [Bind m]
    (n : Type u → Type w) [Pure n] [Bind n]
    (f : {α : Type u} → m α → n α) where
  map_pure {α} (x : α) : f (pure x) = pure x
  map_bind {α β} (x : m α) (y : α → m β) : f (x >>= y) = f x >>= f ∘ y

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)

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

class LawfulComonad (w : Type u → Type v) [Comonad w] extends LawfulCoapplicative w where
   
  map_eq_extend_extract : ∀ {α β : Type u} (f : α → β) (wa : w α),
    Functor.map f wa = extend wa (f ∘ extract)
   
  extend_extract : ∀ {α : Type u} (wa : w α), extend wa (@extract w _ α) = wa
   
  extract_extend : ∀ {α β : Type u} (wa : w α) (f : w α → β),
    extract (extend wa f) = f wa
   
  extend_assoc : ∀ {α β γ : Type u} (wa : w α) (f : w α → β) (g : w β → γ),
    extend (extend wa f) g = extend wa (fun w'a => g (extend w'a f))

instance : Comonad (CofreeC F) where
  extract := extract
  extend := sorry
  coseq := sorry

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

liftWith_restoreM {α : Type u} (t : n α) :
    MonadControl.liftWith (m := m) (fun run => run t) >>= MonadControl.restoreM ∘ pure = t

instance isEmpty : IsEmpty (OracleQuery []ₒ α) where false | query i t => i.elim

set_set : {s₁ s₂ : σ} → (do set s₁; set s₂) = set (m := m) s₂

bind_pure_compᵣ {α β : Type u} (f : j α → j β) (x : m α) :
    x >>=ᵣ (fun y => pureᵣ (f y)) = f <$>ᵣ x

DecidablePred in Init.Prelude

instance {m} [Monad m] [Commutative m] {α β} (ma : m α) (mb : m β) :
    CommutativeAt m ma mb := bind_comm ma mb

Equiv.prodPEmpty in Mathlib.Logic.Equiv.Prod

class LawfulMonadRelationHom (m₁ : Type u → Type v₁) (n₁ : Type u → Type w₁)
    (m₂ : Type u → Type v₂) (n₂ : Type u → Type w₂)
    [MonadRelation m₁ n₁] [MonadRelation m₂ n₂]
    [MonadRelationHom m₁ n₁ m₂ n₂] where
  monadRel_hom {α : Type u} {ma : m₁ α} {na : n₁ α} (h : ma ∼ₘ na) :
    (monadRelHomFst n₁ n₂ ma : m₂ α) ∼ₘ (monadRelHomSnd m₁ m₂ na : n₂ α)

instance instLawfulCoapplicative [Comonad w] [LawfulCoapplicative w] : LawfulCoapplicative (StoreT s w) where
  coseqLeft_eq := sorry 
  coseqRight_eq := sorry 
  coseq_assoc := sorry

structure IND_CCA_Adversary (encAlg : AsymmEncAlg m M PK SK C) where
    main : PK → OracleComp encAlg.IND_CCA_oracleSpec Bool

instance : One PFunctor.{uA, uB} where
  one := ⟨PUnit, fun _ => PEmpty⟩

LawfulMonadLiftT in Init.Control.Lawful.MonadLift.Basic

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

def FreeMonad.toFreeContM : FreeMonad f α → FreeContM f α :=
  fun x => match x with
    | FreeMonad.pure a => fun _ handlePure => handlePure a
    | FreeMonad.roll x k => fun handleEff handlePure =>
      handleEff x (fun a => FreeMonad.toFreeContM (k a) handleEff handlePure)

instance {a} : IsEmpty (B 1 a) := inferInstanceAs (IsEmpty PEmpty)

ContT in Mathlib.Control.Monad.Cont

ExceptT.bind in Init.Control.Except

instance : Coapplicative Zipper where
  coseq := coseq

instance : Repr mock_hmac_sha256_out_type := instReprString

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

inductive FreeM (f : Type v → Type w) (α : Type u) where
  | pure (a : α) : FreeM f α
  | roll {β : Type v} (x : f β) (k : β → FreeM f α) : FreeM f α

get_get : get *> get = get

Summable in Mathlib.Topology.Algebra.InfiniteSum.Defs

instance {w d} [Monad w] [DijkstraMonad w d] : MonadLiftT (fun α => (w : w α) × d w) w where
  monadLift x := x.1

def prepare_encrypted_message (content : String) (nonce : BitVec 256) : EncryptedMessage :=
  let (msg_bv, _) := serialize_message_data content nonce
  { ciphertext := mock_encrypt msg_bv }

@[inline] def bind (x : FreeContT f m α) (g : α → FreeContT f m β) :
    FreeContT f m β :=
  fun handleEff handlePure => x handleEff (fun a => g a handleEff handlePure)

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

List.tails in Batteries.Data.List.Basic

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

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₂ α

def isPure {α : Type v} : OracleComp spec α → Bool
  | FreeMonad.pure x => Option.isSome x
  | _ => false

Equiv.sigmaPUnit in Mathlib.Logic.Equiv.Prod

def LWE_Uniform_Distr : ProbComp (Matrix (Fin n) (Fin m) (Fin p) × Vector (Fin p) m) := do
  let A ←$ᵗ Matrix (Fin n) (Fin m) (Fin p)
  let u ←$ᵗ Vector (Fin p) m
  return (A, u)

def cacheQuery  (i : ι) (t : spec.domain i) (u : spec.range i) :
    QueryCache spec := Function.update cache i (Function.update (cache i) t u)

def FreeContT (f : Type z → Type y) (m : Type u → Type v) (α : Type w) :
    Type (max (u + 1) v w y (z + 1)) :=
  {r : Type u} → ({x : Type z} → f x → ContT r m x) → ContT r m α

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

Array.foldrM in Init.Data.Array.Basic

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

instance : CoseqRight Stream' where
  coseqRight _ s₂ := s₂

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

instMonadFunctorTOfMonadFunctor in Init.Prelude

class Extract (w : Type u → Type v) where
   
  extract {α : Type u} : w α → α

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))

TopologicalSpace in Mathlib.Topology.Defs.Basic

instance : LawfulFunctor NonEmptyList where
  id_map := by admit /- proof elided -/

structure StoreT (s : Type u₂) (w : Type u₂ → Type v₂) (a : Type u₂) where
   
  runStoreT : w (s → a)
   
  pos : s

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 -/

def toNatHom (e : NatEquiv m n) : NatHom m n where
  toFun := e.toFun

instance : OracleSpec.DecidableEq []ₒ where
  domain_decidableEq' := inferInstance
  range_decidableEq' := inferInstance

instance {ε} [Subsingleton ε] : Commutative (Except ε) where
  bind_comm := fun ma mb => by admit /- proof elided -/

def sigmaTensorDistrib {I : Type v} (F : I → PFunctor.{uA₁, uB₁}) (P : PFunctor.{uA₂, uB₂}) :
    sigma F ⊗ P ≃ₚ sigma (fun i => F i ⊗ P) where
  equivA := sorry
  equivB := sorry

class AssertAssume (α : Type u) [Preorder α] where
  assert : Prop → α → α
  assume : Prop → α → α
  assert_strengthen : ∀ p x, assert p x ≤ x
  assume_weaken : ∀ p x, x ≤ assume p x
  assert_assume_iff : ∀ p x y, assert p x ≤ y ↔ x ≤ assume p y

instance : Extract Id where
  extract := id

PMF.instMonad in Mathlib.Probability.ProbabilityMassFunction.Monad

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

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

Pure in Init.Prelude

def compose (so' : QueryImpl spec' m) (so : QueryImpl spec (OracleComp spec')) :
    QueryImpl spec m where
  impl q := simulateQ so' (so.impl q)

OfNat in Init.Prelude

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

def finSupportWhen [DecidableEq α] (oa : OracleComp spec α)
    (possible_outputs : {α : Type v} → OracleQuery spec α → Finset α) : Finset α :=

@[simps!] def elgamalAsymmEnc (G P : Type) [SelectableType G] [SelectableType P]
    [AddGroup G] [Group P] [AddTorsor G P] : AsymmEncAlg ProbComp
    (M := P) (PK := P × P) (SK := G) (C := P × P) where
  keygen := do
    let x₀ ←$ᵗ P; let sk ←$ᵗ G
    return ((x₀, sk +ᵥ x₀), sk)
  encrypt := fun (x₀, pk) msg => do
    let g ←$ᵗ G
    return (g +ᵥ x₀, msg * (g +ᵥ pk))
  decrypt := fun sk (c₁, c₂) => do
    return c₂ / (sk +ᵥ c₁)
  __ := ExecutionMethod.default

instance range_inhabited {i : ι} [h : FiniteRange spec] :
    Inhabited (spec.range i) := h.range_inhabited' i

def sumComm (P : PFunctor.{uA₁, uB}) (Q : PFunctor.{uA₂, uB}) :
    Lens.Equiv.{max uA₁ uA₂, uB, max uA₁ uA₂, uB} (P + Q) (Q + P) where
  toLens := Lens.sumPair Lens.inr Lens.inl
  invLens := Lens.sumPair Lens.inr Lens.inl
  left_inv := by admit /- proof elided -/

def Proper (A : Type u) (R : A → A → Prop) (m : A) : Prop := R m m

modifyGetThe in Init.Prelude

isEmptyElim in Mathlib.Logic.IsEmpty

Matrix in Mathlib.LinearAlgebra.Matrix.Defs

liftWith_bind {α β : Type u} (ma : m α) (f : α → m β) :
    liftWith (fun _ => ma) >>= liftWith ∘ (fun a _ => f a) = liftWith (n := n) (fun _ => ma >>= f)

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 -/

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

Preord in Mathlib.Order.Category.Preord

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

instance [MonadLift (OracleQuery spec) (OracleQuery superSpec)] :
    MonadLift (OracleComp spec) (OracleComp superSpec) where
  monadLift oa := liftComp oa superSpec

Function.LeftInverse in Init.Data.Function

instance : Monad MonoContProp := inferInstanceAs (Monad (MonoCont Prop))
</all_available_defs>

<all_available_lemmas>
@[simp]
lemma bind_pure (x : α) (r : α → FreeMonad f β) :
    FreeMonad.bind (FreeMonad.pure x) r = r x

@[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 bind_lift (x : f α) (r : α → FreeMonad f β) :
    FreeMonad.bind (FreeMonad.lift x) r = FreeMonad.roll x r

@[simp]
lemma monad_pure_def (x : α) : (pure x : FreeMonad f α) = FreeMonad.pure x

@[simp]
lemma monad_bind_def (x : FreeMonad f α) (g : α → FreeMonad f β) :
    x >>= g = FreeMonad.bind x g

lemma monad_pure_def [Monad m] (x : α) :
    (pure x : StateT σ m α) = StateT.pure x

@[simp]
lemma evalDist_query (i : ι) (t : spec.domain i) : evalDist (query i t : OracleComp spec _) =
    OptionT.lift (PMF.uniformOfFintype (spec.range i))

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

lemma mem_finSupport_iff_mem_support (x : α) : x ∈ oa.finSupport ↔ x ∈ oa.support

@[simp]
theorem fst_comp_prodPair (f : Lens P Q) (g : Lens P R) :
    Lens.fst ∘ₗ Lens.prodPair f g = f

lemma evalDist_seq_map [spec.FiniteRange] :
    evalDist (f <$> oa <*> ob) = f <$> evalDist oa <*> evalDist ob

@[simp]
lemma probOutput_liftM [Fintype α] (q : OracleQuery spec α) (u : α) :
    [= u | (q : OracleComp spec α)] = (Fintype.card α : ℝ≥0∞)⁻¹

@[simp]
theorem compMap_id :
    (Lens.id P) ◃ₗ (Lens.id Q) = Lens.id (P ◃ Q)

@[simp]
lemma liftM_query_readerT {ρ : Type v} {α : Type v} (q : OracleQuery spec α) :
  (liftM q : ReaderT ρ (OracleComp spec) α) = liftM (liftM q : OracleComp spec α)

lemma probEvent_congr' {p q : α → Prop} {oa : OracleComp spec α} {oa' : OracleComp spec' α}
    (h1 : ∀ x, x ∈ oa.support → x ∈ oa'.support → (p x ↔ q x))
    (h2 : evalDist oa = evalDist oa') : [p | oa] = [q | oa']

@[simp] lemma finSupport_ite [spec.DecidableEq] [spec.FiniteRange] [DecidableEq α]
    (p : Prop) [Decidable p] (oa oa' : OracleComp spec α) :
    (if p then oa else oa').finSupport = if p then oa.finSupport else oa'.finSupport

lemma probFailure_bind_eq_sum_fintype [Fintype α] :
    [⊥ | oa >>= ob] = [⊥ | oa] + ∑ x : α, [= x | oa] * [⊥ | ob x]

@[simp]
lemma probOutput_eq_zero_iff' [spec.DecidableEq] [DecidableEq α] :
    [= x | oa] = 0 ↔ x ∉ oa.finSupport

lemma probEvent_eq_tsum_ite (oa : OracleComp spec α) (p : α → Prop) [DecidablePred p] :
    [p | oa] = ∑' x : α, if p x then [= x | oa] else 0

lemma probFailure_bind_of_const [Nonempty α] (r : ℝ≥0∞) (h : ∀ x, [⊥ | ob x] = r) :
    [⊥ | oa >>= ob] = [⊥ | oa] + r - [⊥ | oa] * r

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

theorem bind_comm_triple_swap_12 {m} [Monad m] [LawfulMonad m] [Commutative m] {α β γ δ}
    (ma : m α) (mb : m β) (mc : m γ) (f : α × β × γ → m δ) :
    (do let a ← ma; let b ← mb; let c ← mc; f (a, b, c)) =
    (do let b ← mb; let a ← ma; let c ← mc; f (a, b, c))

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]
lemma probFailure_run_simulateQ [spec.FiniteRange] (oa : OracleComp spec α) :
    [⊥ | (simulateQ loggingOracle oa).run] = [⊥ | oa]

@[simp]
lemma equivState_equivState : (so.equivState e).equivState e.symm = so

@[simp] lemma failure_ne_query_bind : failure ≠ (q : OracleComp spec β) >>= oa

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

@[simp]
theorem symm_symm {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} (e : P ≃ₚ Q) :
    e.symm.symm = e

@[simp]
lemma mapM_pure (x : α) : (FreeM.pure x : FreeM P α).mapM s = Pure.pure x

@[simp low]
lemma probEvent_eq_one_iff : [p | oa] = 1 ↔ [⊥ | oa] = 0 ∧ ∀ x ∈ oa.support, p x

@[simp]
lemma probOutput_fst_map_eq_sum [spec.FiniteRange] [Fintype β]
    (oa : OracleComp spec (α × β)) (x : α) : [= x | fst <$> oa] = ∑ y, [= (x, y) | oa]

lemma probOutput_prod_mk_eq_probEvent [spec.FiniteRange] [DecidableEq α] [DecidableEq β]
    (oa : OracleComp spec (α × β)) (x : α) (y : β) :
    [= (x, y) | oa] = [λ z ↦ z.1 = x ∧ z.2 = y | oa]

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 mk_pure_eq_pure [Monad m] (x : α) :
  StateT.mk (λ s ↦ pure (x, s)) = (pure x : StateT σ m α)

lemma BitVec.toFin_bijective (n : ℕ) :
    Function.Bijective (BitVec.toFin : BitVec n → Fin (2 ^ n))

lemma eq_takeAtIndex_length_iff (seed seed' : QuerySeed spec) (i : ι) :
    seed = seed'.takeAtIndex i (seed i).length ↔
      seed' = seed.addValues ((seed' i).drop (seed i).length)

@[simp] lemma probFailure_uniformSelectFinset [DecidableEq α] (s : Finset α) :
    [⊥ | $ s] = if s.Nonempty then 0 else 1

@[simp] lemma finSupportWhen_query [DecidableEq α] (q : OracleQuery spec α) :
    (q : OracleComp spec α).finSupportWhen fin_poss = fin_poss q

@[simp]
lemma heq_of_toArray_eq_of_size_eq {α} {m n : ℕ} {a : Vector α m} {b : Vector α n}
    (h : a.toArray = b.toArray) (h' : m = n) : HEq a b

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

@[simp] lemma probEvent_const (oa : OracleComp spec α) (p : Prop) [Decidable p] :
    [λ _ ↦ p | oa] = if p then 1 - [⊥ | oa] else 0

@[simp] lemma neverFails_lift_comp_iff (oa : OracleComp spec α) :
    (liftComp oa superSpec).neverFails ↔ oa.neverFails

lemma probOutput_eq_sub_probFailure_of_unit {oa : OracleComp spec PUnit} :
    [= () | oa] = 1 - [⊥ | oa]

lemma support_eq_setOf_probOutput_eq_zero [spec.FiniteRange] (oa : OracleComp spec α) :
    oa.support = {x | [= x | oa] ≠ 0}

lemma probEvent_bind_eq_sum_finSupport [spec.DecidableEq] [DecidableEq α]
    (q : β → Prop) :
    [q | oa >>= ob] = ∑ x ∈ oa.finSupport, [= x | oa] * [q | ob x]

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

lemma probFailure_bind_eq_tsum :
    [⊥ | oa >>= ob] = [⊥ | oa] + ∑' x : α, [= x | oa] * [⊥ | ob x]

@[simp]
lemma evalDist_failure : evalDist (failure : OracleComp spec α) = failure

lemma probOutput_map_eq_sum_filter_finSupport [spec.DecidableEq] [DecidableEq α] [DecidableEq β]
    (y : β) : [= y | f <$> oa] = ∑ x ∈ oa.finSupport.filter (y = f ·), [= x | oa]

@[simp] lemma PMF.map_some_apply_some (p : PMF α) (x : α) : (some <$> p) (some x) = p x

theorem IsCoupling.exists_bind {α₁ α₂ β₁ β₂ : Type u}
    {p : SPMF α₁} {q : SPMF α₂} {f : α₁ → SPMF β₁} {g : α₂ → SPMF β₂}
    (c : Coupling p q)
    (h : ∀ (a₁ : α₁) (a₂ : α₂), ∃ (d : SPMF (β₁ × β₂)), IsCoupling d (f a₁) (g a₂)) :
    ∃ (d : SPMF (β₁ × β₂)), IsCoupling d (p >>= f) (q >>= g) :=
  let d : (a₁ : α₁) → (a₂ : α₂) → SPMF (β₁ × β₂)

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 List.foldlM_range {m : Type u → Type v} [Monad m] [LawfulMonad m]
    {s : Type u} (n : ℕ) (f : s → Fin n → m s) (init : s)  :
    List.foldlM f init (List.finRange n) =
      Fin.foldlM n f init

@[simp]
lemma probOutput_prod_mk_snd_map' [spec.FiniteRange] (ob : OracleComp spec β)
    (f : β → γ) (x : α) (z : α × γ) :
    [= z | (x, f ·) <$> ob] = [= z.1 | (pure x : OracleComp spec α)] * [= z.2 | f <$> ob]

lemma probEvent_query_eq_inv_mul [spec.DecidableEq] (p : spec.range i → Prop) [DecidablePred p] :
    [p | (query i t : OracleComp spec _)] =
      (↑(Fintype.card (spec.range i)))⁻¹ * (Finset.univ.filter p).card

@[simp] theorem RelativeFunctor.map_map [RelativeFunctor j f] [LawfulRelativeFunctor j f]
    (h : j α → j β) (g : j β → j γ) (x : f α) :
      g <$>ᵣ h <$>ᵣ x = (fun a => g (h a)) <$>ᵣ x

@[simp]
lemma isQueryBound_pure (a : α) (qb : ι → ℕ) : IsQueryBound (pure a : OracleComp spec α) qb

lemma probOutput_pure_eq_one {x y : α} (h : y = x) :
    [= y | (pure x : OracleComp spec α)] = 1

@[simp] lemma failure_ne_pure : failure ≠ (pure x : OracleComp spec α)

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

lemma mem_support_map {oa : OracleComp spec α} {x : α}
    (hx : x ∈ oa.support) (f : α → β) : f x ∈ (f <$> oa).support

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

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

lemma mem_finSupport_seq_map_iff_of_injective2 [spec.FiniteRange] [spec.DecidableEq]
    [DecidableEq α] [DecidableEq β] [DecidableEq γ]
    (hf : f.Injective2) (x : α) (y : β) : f x y ∈ (f <$> oa <*> ob).finSupport ↔
      x ∈ oa.finSupport ∧ y ∈ ob.finSupport

@[simp]
lemma probOutput_fst_map_eq_tsum [spec.FiniteRange] (oa : OracleComp spec (α × β)) (x : α) :
    [= x | fst <$> oa] = ∑' y, [= (x, y) | oa]

lemma probEvent_eq_tsum_indicator (mx : m α) (p : α → Prop) :
    Pr[p | mx] = ∑' x : α, {x | p x}.indicator (Pr[= · | mx]) x

lemma probOutput_map_eq_probOutput_inverse (f : α → β) (g : β → α)
    (hl : Function.LeftInverse f g) (hr : Function.RightInverse f g)
    (y : β) : [= y | f <$> oa] = [= g y | oa]

lemma abs_mul_of_nonpos (h : b < 0) : |a

@[simp]
lemma neverFails_run_simulateQ_iff (oa : OracleComp spec α) :
    neverFails (simulateQ countingOracle oa).run ↔ neverFails oa

lemma eq_addValues_iff [DecidableEq ι] (seed seed' : QuerySeed spec)
    {i : ι} (xs : List (spec.range i)) :
    seed = seed'.addValues xs ↔ seed' = seed.takeAtIndex i (seed' i).length ∧
      xs = (seed i).drop (seed' i).length

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

@[simp low]
lemma finSupport_seq [spec.DecidableEq] [spec.FiniteRange]
    [DecidableEq α] [DecidableEq β] [DecidableEq (α → β)] :
    (og <*> oa).finSupport = og.finSupport.biUnion (λ g ↦ oa.finSupport.image g)

@[simp]
lemma monadLift_eq_lift (x : P.Obj α) : (x : FreeM P α) = FreeM.lift x

@[simp] lemma probOutput_none_map_fork_right (s : Option (Fin (qb i + 1))) :
    [= (s, none) | Prod.map cf cf <$> main.fork qb js i cf] = 0

@[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 α)

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

lemma probFailure_seq [spec.FiniteRange] :
    [⊥ | og <*> oa] = [⊥ | og] + [⊥ | oa] - [⊥ | og] * [⊥ | oa]

@[simp]
lemma run_bind [LawfulMonad m] (x : WriterT ω m α) (f : α → WriterT ω m β) :
    (x >>= f).run = x.run >>= fun (a, w₁) => Prod.map id (w₁ * ·) <$> (f a).run

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

@[simp]
lemma probOutput_liftComp [spec.FiniteRange] [superSpec.FiniteRange]
    (oa : OracleComp spec α) (x : α) : [= x | liftComp oa superSpec] = [= x | oa]

@[simp]
lemma mmap_bind (F : m →ᵐ n) (x : m α) (y : α → m β) :
    F (x >>= y) = F x >>= fun x => F (y x)

lemma probOutput_seq_eq_sum_finSupport_ite [spec.FiniteRange] [spec.DecidableEq]
    [DecidableEq α] [DecidableEq (α → β)] [DecidableEq β]
    (y : β) : [= y | og <*> oa] = ∑ g ∈ og.finSupport, ∑ x ∈ oa.finSupport,
      if y = g x then [= g | og] * [= x | oa] else 0

protected lemma failure_def : (failure : OracleComp spec α) = OptionT.fail

@[simp]
lemma probFailure_liftM (q : OracleQuery spec α) :
    [⊥ | (q : OracleComp spec _)] = 0

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

@[simp]
theorem MonoContProp_def :
  MonoContProp = fun α => {m : Cont Prop α // ∀ p p', (∀ a, p a → p' a) → m p → m p'}

@[simp]
lemma probEvent_ite (q : α → Prop) : [q | if p then oa else oa'] =
    if p then [q | oa] else [q | oa']

@[simp] lemma supportWhen_query_bind (q : OracleQuery spec α) (ob : α → OracleComp spec β) :
    (liftM q >>= ob).supportWhen poss = ⋃ x ∈ poss q, (ob x).supportWhen poss

@[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 low]
lemma zero_eq_probOutput_iff : 0 = [= x | oa] ↔ x ∉ oa.support

@[simp]
lemma depth_roll {x : f α} {r : α → FreeMonad f β} :
    depth (roll x r : FreeMonad f β) = 1 + iSup (λ u ↦ depth (r u))

@[simp] lemma evalDist_uniformSelectFinset [DecidableEq α] (s : Finset α) :
    evalDist ($ s) = if hs : s.Nonempty then
      OptionT.lift (PMF.uniformOfFinset s hs) else failure

@[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)

@[simp]
lemma neverFails_query_bind_iff {q : OracleQuery spec α} {oa : α → OracleComp spec β} :
    (liftM q >>= oa).neverFails ↔ ∀ x, neverFails (oa x)

lemma probOutput_bind_congr {oa : OracleComp spec α} {ob₁ ob₂ : α → OracleComp spec β} {y : β}
    (h : ∀ x ∈ oa.support, [= y | ob₁ x] = [= y | ob₂ x]) :
    [= y | oa >>= ob₁] = [= y | oa >>= ob₂]

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

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

@[simp]
lemma mapM_bind' {m : Type v → Type w} [AlternativeMonad m] [LawfulMonad m]
    [LawfulAlternative m] (qm : {α : Type v} → OracleQuery spec α → m α)
    (oa : OracleComp spec α) (ob : α → OracleComp spec β) :
    (oa >>= ob).mapM failure qm =
      oa.mapM failure qm >>= λ x ↦ (ob x).mapM failure qm

@[simp] lemma probEvent_eq : probEvent p = p.toOuterMeasure

@[simp]
lemma evalDist_simulateQ [spec.FiniteRange] (oa : OracleComp spec α) :
    evalDist (simulateQ unifOracle oa) = evalDist oa

@[simp] lemma index_query (i : ι) (t : spec.domain i) : (query i t).index = i

@[simp]
lemma mem_support_evalDist_iff' [spec.DecidableEq] [DecidableEq α]
    (oa : OracleComp spec α) (x : α) :
    some x ∈ (evalDist oa).run.support ↔ x ∈ oa.finSupport

lemma probEvent_query_eq_div [spec.DecidableEq] (p : spec.range i → Prop) [DecidablePred p] :
    [p | (query i t : OracleComp spec _)] =
      (Finset.univ.filter p).card / (Fintype.card (spec.range i))

lemma probEvent_bind_eq_sum_fintype [Fintype α] (q : β → Prop) :
    [q | oa >>= ob] = ∑ x : α, [= x | oa] * [q | ob x]

@[simp] lemma probEvent_uniformOfFintype [Fintype α] (p : α → Prop) [DecidablePred p] :
    [p | $ᵗ α] = (Finset.univ.filter p).card / Fintype.card α

@[simp]
lemma evalDist_seq_map_swap [spec.FiniteRange] :
    evalDist (Function.swap f <$> ob <*> oa) = evalDist (f <$> oa <*> ob)

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

lemma X_eq_purePower_pUnit : X = purePower PUnit

theorem comp_assoc {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}}
    {S : PFunctor.{uA₄, uB₄}} (c : Chart R S) (c' : Chart Q R) (c'' : Chart P Q) :
    (c ∘c c') ∘c c'' = c ∘c (c' ∘c c'')

lemma finSupport_subset_iff_support_subset_coe : oa.finSupport ⊆ s ↔ oa.support ⊆ ↑s

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 BitVec.xor_xor_cancel_right {n : ℕ} (bv1 bv2 : BitVec n) :
    bv1 ^^^ bv2 ^^^ bv2 = bv1

@[simp]
lemma probOutput_vector_toList [spec.FiniteRange] [spec.DecidableEq]
    {n : ℕ} (oa : OracleComp spec (List.Vector α n))
    (xs : List α) : [= xs | List.Vector.toList <$> oa] =
      if h : xs.length = n then [= ⟨xs, h⟩ | oa] else 0

lemma probOutput_bind_eq_tsum (y : β) :
    [= y | oa >>= ob] = ∑' x : α, [= x | oa] * [= y | ob x]

lemma Fintype.sum_inv_card (α : Type*) [Fintype α] [Nonempty α] :
  Finset.sum Finset.univ (λ _ ↦ (Fintype.card α)⁻¹ : α → ℝ≥0∞) = 1

@[simp] lemma probFailure_ne_top : Pr[⊥ | mx] ≠ ∞

lemma tsum_run_some_eq_one_sub (p : SPMF α) :
    ∑' x, p.run (some x) = 1 - p.run none

lemma ProbComp.advantage₂_eq_abs_sub_probFailure (p q : ProbComp Unit) :
    p.advantage₂ q = |([⊥ | p]).toReal - ([⊥ | q]).toReal

lemma StateT_run'_simulateQ_eq_self {α} (so : QueryImpl spec (StateT σ (OracleComp spec)))
    (h : ∀ α (q : OracleQuery spec α) s, (so.impl q).run' s = q)
    (oa : OracleComp spec α) (s : σ) : (simulateQ so oa).run' s = oa

lemma pull_up_4_helper {ι : Type*} {spec : OracleSpec ι} [spec.FiniteRange]
    {α β γ δ ε : Type}
    (oa : OracleComp spec α) (ob : OracleComp spec β)
    (oc : OracleComp spec γ) (od : OracleComp spec δ)
    (oe : α → β → γ → δ → OracleComp spec ε) (z : ε) :
    [= z | do let a ← oa; let b ← ob; let c ← oc; let d ← od; oe a b c d] =
      [= z | do let d ← od; let a ← oa; let b ← ob; let c ← oc; oe a b c d]

@[simp]
lemma run_mk {ω : Type u} [LawfulMonad m] (x : m (α × ω)) :
  (WriterT.mk x).run = x

@[simp] lemma tsum_probOutput_ne_top : ∑' x : α, [= x | oa] ≠ ⊤

lemma eq_finSupport_iff_coe_eq_support : s = oa.finSupport ↔ ↑s = oa.support

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

lemma cons_mem_support_seq_map_cons_iff (x : α) (xs : List α) :
    x :: xs ∈ (cons <$> oa <*> ob).support ↔ x ∈ oa.support ∧ xs ∈ ob.support

@[simp]
lemma snd_map_prod_mk_of_subsingleton [Subsingleton α]
    (ob : OracleComp spec β) (x : α) : snd <$> (x, ·) <$> ob = ob

lemma probEvent_eq_tsum_indicator (oa : OracleComp spec α) (p : α → Prop) :
    [p | oa] = ∑' x : α, {x | p x}.indicator ([= · | oa]) x

lemma liftM_def [Monad m] (x : m α) : (liftM x : StateT σ m α) = StateT.lift x

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

lemma probOutput_def (oa : OracleComp spec α) (x : α) :
    [= x | oa] = (evalDist oa).run (some x)

@[simp] lemma probOutput_uniformSelectFinset [DecidableEq α] (s : Finset α) (x : α) :
    [= x | $ s] = if x ∈ s then (s.card : ℝ≥0∞)⁻¹ else 0

@[simp] lemma finSupportWhen_pure [DecidableEq α] (x : α) :
    (pure x : OracleComp spec α).finSupportWhen fin_poss = {x}

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

@[simp] lemma run_none_ne_top (p : SPMF α) : p.run none ≠ ⊤

lemma subset_finSupport_iff_coe_subset_support : s ⊆ oa.finSupport ↔ ↑s ⊆ oa.support

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

@[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] lemma finSupport_uniformSelectFinset [DecidableEq α] (s : Finset α) :
    ($ s).finSupport = if s.Nonempty then s else ∅

@[simp]
lemma Fin_Bound_mul {n b₁ b₂ : ℕ} {x y : Fin n} (h₁ : Fin_Bound x b₁)
 (h₂ : Fin_Bound y b₂) : Fin_Bound (x * y) (b₁ * b₂)

@[simp]
lemma mapM_query [LawfulMonad m] (q : OracleQuery spec α) :
    (q : OracleComp spec α).mapM fail qm = qm q

List.isEmpty_iff in Init.Data.List.Lemmas

@[simp] lemma probEvent_lt_top : Pr[p | mx] < ∞

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

@[simp]
lemma liftM_of_liftM_eq [MonadLift m m'] (x : StateT σ m α) :
    (liftM x : StateT σ m' α) = StateT.mk fun s => liftM (x.run s)

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 zero_eq_probOutput_iff' [spec.DecidableEq] [DecidableEq α] :
    0 = [= x | oa] ↔ x ∉ oa.finSupport

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

lemma neverFails_eq_freeMonad_construct (oa : OracleComp spec α) :
    oa.neverFails = FreeMonad.construct
      (fun t ↦ Option.rec False (fun _ ↦ True) t) (fun _ _ r ↦ ∀ x, r x) oa

@[simp]
lemma ProbComp.advantage₂_self (p : ProbComp Unit) : p.advantage₂ p = 0

@[simp] lemma probFailure_le_one : Pr[⊥ | mx] ≤ 1
</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

end lift

notation "$[0.." n "]" => uniformFin n

notation:50 "$[" n "⋯" m "]" => uniformFin' n m

example : OracleComp probSpec ℕ := do
  let x ← $[314⋯31415]; let y ← $[0⋯x]
  return x + 2 * y

section construct

variable {C : OracleComp spec α → Type w}
  (h_pure : (a : α) → C (pure a))
  (h_query_bind : {β : Type v} → (q : OracleQuery spec β) →
      (oa : β → OracleComp spec α) → ((u : β) → C (oa u)) → C (q >>= oa))
  (h_failure : C failure) (oa : OracleComp spec α)

end construct

section noConfusion

variable (x : α) (y : β) (q : OracleQuery spec β) (oa : β → OracleComp spec α)

end noConfusion

section mapM

variable {m : Type v → Type w} [Monad m]
  (fail : {α : Type v} → m α) (qm : {α : Type v} → OracleQuery spec α → m α)

end mapM

section inj
</local_ctx>

<target_theorem>
@[simp]
lemma queryBind_inj (q q' : OracleQuery spec α) (ob ob' : α → OracleComp spec β) :
    (q : OracleComp spec α) >>= ob = (q' : OracleComp spec α) >>= ob' ↔ q = q' ∧ ob = ob' :=
</target_theorem>

