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 α

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

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

class HasEvalDist (m : Type u → Type v) [Monad m] where
  evalDist {α : Type u} (mx : m α) : SPMF α
  evalDist_pure {α : Type u} (x : α) : evalDist (pure x : m α) = pure x
  evalDist_bind {α β : Type u} (mx : m α) (my : α → m β) :
    evalDist (mx >>= my) = evalDist mx >>= fun x => evalDist (my x)

noncomputable def probOutput (oa : OracleComp spec α) (x : α) : ℝ≥0∞ :=
  (evalDist oa).run (some x)

noncomputable def probEvent (oa : OracleComp spec α) (p : α → Prop) : ℝ≥0∞ :=
  (evalDist oa).run.toOuterMeasure (Option.some '' {x | p x})

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

def support (oa : OracleComp spec α) : Set α :=
  oa.supportWhen fun _ => Set.univ

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)

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

@[elab_as_elim]
protected def inductionOn {C : OracleComp spec α → Prop}
    (pure : (a : α) → C (pure a))
    (query_bind : (i : ι) → (t : spec.domain i) →
      (oa : spec.range i → OracleComp spec α) → (∀ u, C (oa u)) → C (query i t >>= oa))
    (failure : C failure) (oa : OracleComp spec α) : C oa :=
  FreeMonad.inductionOn (Option.rec failure pure) (λ (query i t) ↦ query_bind i t) oa

@[elab_as_elim]
protected def induction {C : OracleComp spec α → Prop}
    (oa : OracleComp spec α) (pure : (a : α) → C (pure a))
    (query_bind : (i : ι) → (t : spec.domain i) →
      (oa : spec.range i → OracleComp spec α) → (∀ u, C (oa u)) → C (query i t >>= oa))
    (failure : C failure) : C oa :=
  FreeMonad.inductionOn (Option.rec failure pure) (λ (query i t) ↦ query_bind i t) oa

@[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 cases {α} {motive : {n : ℕ} → Vector α n → Sort*} (v_empty : motive #v[])
  (v_insert : {n : ℕ} → (hd : α) → (tl : Vector α n) → motive (tl.insertIdx 0 hd)) {m : ℕ} :
    (v : Vector α m) → motive v := match hm : m with
  | 0 => fun v => match v with | ⟨⟨[]⟩, rfl⟩ => v_empty
  | n + 1 => fun v => match hv : v with
    | ⟨⟨hd :: tl⟩, hSize⟩ => by admit /- proof elided -/

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

class FiniteRange (spec : OracleSpec ι) where
    range_inhabited' (i : ι) : Inhabited (spec.range i)
    range_fintype' (i : ι) : Fintype (spec.range i)

@[simp]
def extract (z : Zipper α) : α := z.focus

instance : CoeFun (NatHom m n) (λ _ ↦ {α : Type u} → m α → n α) where
  coe f {_} x := f.toFun x

structure PureHom (m : Type u → Type v) [Pure m] (n : Type u → Type w) [Pure n]
    extends NatHom m n where
  toFun_pure' {α : Type u} (x : α) : toFun (pure x) = (pure x : n α)

Array.flatMapM in Init.Data.Array.Basic

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

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 withCounting (so : QueryImpl spec m) : QueryImpl spec (WriterT spec.QueryCount m) where
  impl | q => tell (QueryCount.single q.index) *> ↑(so.impl q)

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 trans {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}}
    (E : P ≃ₚ Q) (F : Q ≃ₚ R) : P ≃ₚ R where
  equivA := E.equivA.trans F.equivA
  equivB := fun a => (E.equivB a).trans (F.equivB (E.equivA a))

Nat.succ in Init.Prelude

instance : Coapplicative Zipper where
  coseq := coseq

def Fin_Bound {n : ℕ} (x : Fin n) (b : ℕ) : Prop :=
  x.val ≤ b ∨ x.val + b ≥ n

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 : Coapplicative NonEmptyList where

List.cons in Init.Prelude

Monotone in Mathlib.Order.Monotone.Defs

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)

DFunLike in Mathlib.Data.FunLike.Basic

Finset.univ in Mathlib.Data.Fintype.Defs

instance : Commutative Option where
  bind_comm := fun ma mb => by admit /- proof elided -/

class RelativeMonadMorphism (r₁ : Type u → Type v₁) (m₁ : Type u → Type v₁)
    (r₂ : Type u → Type v₂) (m₂ : Type u → Type v₂)
    [RelativeMonad r₁ m₁] [RelativeMonad r₂ m₂] where
  r₁₂ : Type v₁ → Type v₂
  [instFunctor : Functor r₁₂]
  φ : MonadIso r₂ (r₁₂ ∘ r₁)
  mmapᵣ {α : Type u} : r₁₂ (m₁ α) → m₂ α
  mmapᵣ_pureᵣ {α} :
    mmapᵣ ∘ (Functor.map (f := r₁₂) (@pureᵣ r₁ m₁ _ α)) = pureᵣ ∘ φ.invLift.monadLift
  mmapᵣ_bindᵣ {α β : Type u} (f : r₁ α → m₁ β) :
    mmapᵣ ∘ (Functor.map (f := r₁₂) (bindᵣ · f)) =
      (· >>=ᵣ mmapᵣ ∘ Functor.map (f := r₁₂) f ∘ φ.toLift.monadLift) ∘ mmapᵣ

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 (α := α))

Group in Mathlib.Algebra.Group.Defs

class OrderedMonad (m : Type u → Type v) extends Monad m where
  [monadOrder {α : Type u} : Preorder (m α)]
  bind_mono {α β : Type u} {ma ma' : m α} {f f' : α → m β} (ha : ma ≤ ma') (hf : ∀ a, f a ≤ f' a) :
    ma >>= f ≤ ma' >>= f'

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

structure Day (f : Type u₁ → Type v₁) (g : Type u₂ → Type v₂) (a : Type u₃) where
   
  {α : Type u₁}
   
  {β : Type u₂}
   
  map' : α → β → a
   
  fa : f α
   
  gb : g β

Computation in Mathlib.Data.Seq.Computation

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

Nonempty in Init.Prelude

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

instance : Add PFunctor.{uA, uB} where
  add := sum

Prod.map in Init.Core

class IsCoupling (c : PMF (α × β)) (p : PMF α) (q : PMF β) where
  map_fst : c.map Prod.fst = p
  map_snd : c.map Prod.snd = q

ReaderT.adapt in Init.Prelude

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

OfNat.ofNat in Init.Prelude

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

MonadControl in Init.Control.Basic

def sumTensorDistrib :
    (Q + R : PFunctor.{max uA₂ uA₃, uB₂}) ⊗ P
      ≃ₗ ((Q ⊗ P) + (R ⊗ P) : PFunctor.{max uA₁ uA₂ uA₃, max uB₁ uB₂}) where
  toLens := (fun ⟨qr, p⟩ => match qr with
              | Sum.inl q => Sum.inl (q, p)
              | Sum.inr r => Sum.inr (r, p)) ⇆
            (fun ⟨qr, _⟩ b => match qr with
              | Sum.inl _ => b
              | Sum.inr _ => b)
  invLens := (fun qprp => match qprp with
              | Sum.inl (q, p) => (Sum.inl q, p)
              | Sum.inr (r, p) => (Sum.inr r, p)) ⇆
             (fun qprp b => match qprp with
              | Sum.inl _ => b
              | Sum.inr _ => b)
  left_inv := by admit /- proof elided -/

StateT.bind in Init.Control.State

instance : unifSpec.DecidableEq where
  domain_decidableEq' := inferInstance
  range_decidableEq' := inferInstance

structure NonEmptyList (α : Type u) where
  head : α
  tail : List α

def idOracle : QueryImpl spec (OracleComp spec) where impl q := OracleComp.lift q

structure RelativeMonadHom (M N : RelativeMonad C D J) where

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

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

def terminal {P : PFunctor.{uA, uB}} : Lens P 1 :=
  (fun _ => PUnit.unit) ⇆ (fun _ => PEmpty.elim)

instance : Coe (MonadEquiv m n) (MonadHom n m) where
  coe f := ⟨f.invNatHom, f.map_pure_inv, f.map_bind_inv⟩

List.mapM in Init.Data.List.Control

Pure in Init.Prelude

Matrix in Mathlib.LinearAlgebra.Matrix.Defs

Function.RightInverse in Init.Data.Function

Subsingleton in Init.Core

@[always_inline, inline]
def lift (x : P.Obj α) : FreeM P α := FreeM.roll x.1 (fun y ↦ FreeM.pure (x.2 y))

def sumMap {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₂, uB₁, max uA₃ uA₄, uB₃} (P + Q) (R + W) :=
  (Sum.map l₁.toFunA l₂.toFunA) ⇆
    (fun psum => match psum with
      | Sum.inl pa => l₁.toFunB pa
      | Sum.inr qa => l₂.toFunB qa)

List.all in Init.Data.List.Basic

@[elab_as_elim]
protected def inductionOn {C : FreeM P α → Prop}
    (pure : ∀ x, C (pure x))
    (roll : (x : P.A) → (r : P.B x → FreeM P α) → (∀ y, C (r y)) → C (FreeM.roll x r)) :
    (oa : FreeM P α) → C oa
  | FreeM.pure x => pure x
  | FreeM.roll x r => roll x _ (λ u ↦ FreeM.inductionOn pure roll (r u))

def relabelM : (t : Tree' α) → StateM ℕ (Tree' ℕ)
  | .leaf _ => do
    let n ← get
    set (n + 1)
    return .leaf n
  | .node l r => do
    let l' ← relabelM l
    let r' ← relabelM r
    return .node l' r'

Seq in Init.Prelude

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

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

@[always_inline, inline]
protected def failure {α : Type u} : WriterT ω m α := WriterT.mk failure

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

instance : Commutative PMF where
  bind_comm := fun ma mb => by admit /- proof elided -/

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⟩

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

instance : Extract Stream' where
  extract := Stream'.head

instance : MonadTransformer (ExceptT ε) where
  mapMonad _ := inferInstance
  transform _ := inferInstance

structure IND_CPA_Adv (encAlg : AsymmEncAlg m M PK SK C) where
  State : Type
  chooseMessages : PK → m (M × M × State)
  distinguish : State → C → m Bool

def ofLift (m : Type u → Type v) (n : Type u → Type v) [Monad m] [Monad n]
    [MonadLift m n] [LawfulMonadLift m n] : m →ᵐ n where
  toFun := liftM
  toFun_pure' := liftM_pure
  toFun_bind' := liftM_bind

@[simp]
def compNth (P : PFunctor.{uA, uB}) : Nat → PFunctor.{max uA uB, uB}
  | 0 => X
  | Nat.succ n => P ◃ compNth P n

instance : LawfulMonadTransformer (ExceptT ε) where
  monad_functor := inferInstance
  liftOf_pure _ := map_pure _ _
  liftOf_bind _ _ := by admit /- proof elided -/

Stream'.map in Mathlib.Data.Stream.Defs

instance : Coe (PureEquiv m n) (PureHom m n) where
  coe f := ⟨f.toNatEquiv, f.map_pure'⟩

instance [RelativeMonad Id m] : Monad m where
  pure := @pureᵣ Id m _
  bind := @bindᵣ Id m _

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

def tensorMap {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 ⟨pa, qa⟩ => (l₁.toFunA pa, l₂.toFunA qa)) ⇆
    (fun ⟨_pa, qa⟩ ⟨rb, wb⟩ => (l₁.toFunB _pa rb, l₂.toFunB qa wb))

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

BitVec.ofFin in Init.Prelude

Set.image2 in Mathlib.Data.Set.Operations

def symm {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} (E : P ≃ₚ Q) : Q ≃ₚ P where
  equivA := E.equivA.symm
  equivB := fun a =>
    (Equiv.cast (congrArg Q.B ((Equiv.symm_apply_eq E.equivA).mp rfl))).trans
      (E.equivB (E.equivA.symm a)).symm

protected class DecidableEq (spec : OracleSpec ι) where
  domain_decidableEq' (i : ι) : DecidableEq (spec.domain i)
  range_decidableEq' (i : ι) : DecidableEq (spec.range i)

abbrev vcvLinters : Array LeanOption := #[
  
  ⟨`linter.hashCommand, true⟩,
  ⟨`linter.oldObtain, true,⟩,
  ⟨`linter.refine, true⟩,
  ⟨`linter.style.cdot, true⟩,
  ⟨`linter.style.dollarSyntax, true⟩,
  
  ⟨`linter.style.longLine, true⟩,
  ⟨`linter.style.longFile, .ofNat 1500⟩,
  ⟨`linter.style.missingEnd, true⟩,
  ⟨`linter.style.setOption, true⟩
]

instance : Coe (PureEquiv m n) (PureHom n m) where
  coe f := ⟨f.toNatEquiv, f.map_pure_inv⟩

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

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

dite in Init.Prelude

def symm (e : NatEquiv m n) : NatEquiv n m where
  toFun := e.invFun
  invFun := e.toFun
  left_inv := e.right_inv
  right_inv := e.left_inv

structure NatHom (m : Type u → Type v) (n : Type u → Type w) where
  toFun : {α : Type u} → m α → n α

Set.image in Mathlib.Data.Set.Defs

FunLike in Mathlib.Data.FunLike.Basic

@[simps]
def inducedFunctor (M : RelativeMonad C D J) : C ⥤ D where
  obj X := M.T X
  map f := M.μ (J.map f ≫ M.η)
  map_comp f g := by admit /- proof elided -/

instance : HPow PFunctor.{uA, uB} PFunctor.{uA, uB} PFunctor.{max uA uB, max uA uB} where
  hPow := exp

def PFunctor.FreeContT (P : PFunctor.{z, y}) (m : Type u → Type v) (α : Type w) :
    Type (max (u + 1) v w y z) :=
  {r : Type u} → ((a : P.A) → ContT r m (P.B a)) → ContT r m α

AddTorsor in Mathlib.Algebra.AddTorsor.Defs

OptionT in Init.Control.Option

MonadControl.restoreM in Init.Control.Basic

def sum (P : PFunctor.{uA₁, uB}) (Q : PFunctor.{uA₂, uB}) :
    PFunctor.{max uA₁ uA₂, uB} :=
  ⟨P.A ⊕ Q.A, Sum.elim P.B Q.B⟩

Vector.ofFn in Init.Data.Vector.Basic

def test_abuse_report_validation : IO Unit := do
  let message_content := "Hello world"
  let manipulated_message := "Hell world"
  let maybeData ← OracleComp.runIO (simulation_setup message_content)
  match maybeData with
  | none =>
    IO.println "setup failed"
  | some data =>
    let valid_abuse_report := {
      message := data.verified_msg,
      franking_tag := data.message_package.franking_tag,
      reporting_tag := data.message_package.reporting_tag,
      context := data.message_package.context }
    let is_valid := validate_abuse_report valid_abuse_report data.facebook_key
    IO.println s!"valid abuse report validation result: {is_valid}"

List.mapM.loop in Init.Data.List.Control

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

@[elab_as_elim]
protected def construct' {C : OracleComp spec α → Type*}
    (pure : (a : α) → C (pure a))
    (query_bind : (i : ι) → (t : spec.domain i) →
      (oa : spec.range i → OracleComp spec α) →
      ((u : spec.range i) → C (oa u)) → C (query i t >>= oa))
    (failure : C failure) (oa : OracleComp spec α) : C oa :=
  oa.construct pure (λ (query i t) ↦ query_bind i t) failure

class MonadAlgebra (m : Type u → Type v) where
  monadAlg {α : Type u} : m α → α

MonadFunctorT in Init.Prelude

def PostCondition (σ α : Type*) := σ → α → σ → Prop

instance : Comonad Zipper where

Equiv.sumEmpty in Mathlib.Logic.Equiv.Sum

PFunctor.A in Mathlib.Data.PFunctor.Univariate.Basic

StateT.mk in Init.Control.State

def PerfectlyComplete (sigAlg : SignatureAlg m M PK SK S) : Prop :=
  ∀ msg : M, [= true | sigAlg.exec do
    let (pk, sk) ← sigAlg.keygen
    let sig ← sigAlg.sign pk sk msg
    sigAlg.verify pk msg sig] = 1

def LWE_Game_1 (adv : LWE_Adversary n m p) : ProbComp Bool := do
  let distr ← LWE_Uniform_Distr n m p
  let b ← adv distr
  return b

instance : Coe (PureEquiv m n) (NatEquiv m n) where
  coe f := f.toNatEquiv

def equivFreeM : FreeMonad f α ≃ FreeContM f α where
  toFun := FreeMonad.toFreeContM
  invFun := FreeContM.toFreeMonad
  left_inv := FreeMonad.toFreeMonad_toFreeContM
  right_inv := FreeContM.toFreeContM_toFreeMonad

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

def prod (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⟩

dotProduct in Mathlib.Data.Matrix.Mul

instance {w d} [Monad w] [DijkstraMonad w d] [h : LawfulMonad w] [LawfulDijkstraMonad w d] :
    LawfulMonad (fun α => (w : w α) × d w) :=
  LawfulMonad.mk' _
    (by admit /- proof elided -/
      )
      
      
      
      
    (by admit /- proof elided -/
        )
    (fun x f g => by admit /- proof elided -/
      )

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

Function.support in Mathlib.Algebra.Notation.Support

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)

@[simps]
def zeroSum : 0 + P ≃ₚ P where
  equivA := Equiv.emptySum PEmpty P.A
  equivB := (Sum.casesOn · (fun a => a.elim) (fun _ => _root_.Equiv.refl _))

structure SimulationData where
  verified_msg : SecretMessage
  message_package : MessagePackage
  facebook_key : BitVec 256
  deriving Repr

Fintype.ofBijective in Mathlib.Data.Fintype.OfMap

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

instance instOfMonadRelation {m n} [Monad m] [Monad n] [MonadRelation m n]
    [LawfulMonadRelation m n] : DijkstraMonad n (fun na => { ma : m _ // monadRel ma na}) where
  dPure x := ⟨pure x, monadRel_pure x⟩
  dBind x f := ⟨x.1 >>= (fun a => (f a).1), monadRel_bind x.2 (fun a => (f a).2)⟩

PartialOrder in Mathlib.Order.Defs.PartialOrder

instance : Append (QueryLog spec) := ⟨List.append⟩

@[inline, reducible] def seededOracle [DecidableEq ι] :
    QueryImpl spec (ReaderT (QuerySeed spec) (OracleComp spec)) :=
  idOracle.withPregen

instance [h₁ : spec₁.FiniteRange] [h₂ : spec₂.FiniteRange] :
    (spec₁ ++ₒ spec₂).FiniteRange where
  range_inhabited' := λ i ↦ Sum.recOn i h₁.range_inhabited' h₂.range_inhabited'
  range_fintype' := λ i ↦ Sum.recOn i h₁.range_fintype' h₂.range_fintype'

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

def CommutativeAt (m : Type u → Type v) [Monad m] {α β : Type u} (ma : m α) (mb : m β) : Prop :=
  (do let a ← ma; let b ← mb; pure (a, b)) = (do let b ← mb; let a ← ma; pure (a, b))

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

noncomputable def LHL_Consequence_Advantage (adv : LHL_Consequence_Adv n p) : ℝ :=
  (LHL_Consequence_Game_0 (m := m) adv).advantage₂' (LHL_Consequence_Game_1 adv)

instance {m n o} [Monad m] [Monad n] [Monad o] [MonadFunctor n o] [MonadFunctorT m n]
    [LawfulMonadFunctor n o] [LawfulMonadFunctorT m n] : LawfulMonadFunctorT m o where
  monadMap_id := by admit /- proof elided -/

def simulateQ [AlternativeMonad m] (so : QueryImpl spec m) (oa : OracleComp spec α) : m α :=
  do Option.getM (← FreeMonad.mapM oa.run so.impl)

class Extend (w : Type u → Type v) where
   
  extend {α β : Type u} : w α → (w α → β) → w β

Coe in Init.Coe

instance : Coapplicative Stream' where

Bool in Init.Prelude

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

class Complete (encAlg : SymmEncAlg m M K C) : Prop where
  decrypt_encrypt_eq_message (msg : M) : [= some msg | encAlg.exec
    do let k ← encAlg.keygen; return encAlg.decrypt k (← encAlg.encrypt k msg)] = 1

ExceptT.lift in Init.Control.Except

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

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

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)

instance instFunctor [Functor w] : Functor (StoreT s w) where
  map f storet := { runStoreT := Functor.map (fun g => f ∘ g) storet.runStoreT, pos := storet.pos }

instance [inst : IsEmpty I] : IsEmpty (sigma F).A where
  false := fun a => inst.elim a.1

def bind (f : FinRatPMF α) (g : α → FinRatPMF β) : FinRatPMF β :=
  ⟨f.toList >>= (fun a => (g a.1).toList), by admit /- proof elided -/
    ⟩

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 α

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

Add in Init.Prelude

StateT.run in Init.Control.State

instance : Extend Id where
  extend wx f := f wx

ULift in Init.Prelude

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

instance : LawfulComonad NonEmptyList where
  map_eq_extend_extract := sorry 
  extend_extract := sorry 
  extract_extend := sorry 
  extend_assoc := sorry

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

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

getThe in Init.Prelude

structure RelativeMonad where
  T : C → D
  η : {A : C} → (J.obj A ⟶[ Bundled c ] T A)
  μ : {A B : C} → (J.obj A ⟶[ Bundled c ] T B) ⟶ (T A ⟶[ Bundled c ] T B)

instance decidablePred_mem_support [spec.FiniteRange] [hα : DecidableEq α]
    (oa : OracleComp spec α) : DecidablePred (· ∈ oa.support) :=

@[inline] def lift [Bind m] {α : Type u} (x : m α) : FreeContT f m α :=
  fun _ handlePure => x >>= handlePure

PMF.uniformOfFinset in Mathlib.Probability.Distributions.Uniform

def compX : P ◃ X ≃ₗ P where
  toLens := invTildeR
  invLens := tildeR
  left_inv := rfl
  right_inv := rfl

structure SigmaAlg
    (S W PC SC Ω P : Type) (p : S → W → Bool) where
   
  commit (s : S) (w : W) : ProbComp (PC × SC)
   
  respond (s : S) (w : W) (sc : SC) (ω : Ω) : ProbComp P
   
  verify (s : S) (pc : PC) (ω : Ω) (p : P) : Bool
   
  sim (s : S) : ProbComp PC
   
  extract (ω₁ : Ω) (p₁ : P) (ω₂ : Ω) (p₂ : P) : ProbComp W

class OrderedMonadLiftT (m : Type u → Type v) (n : Type u → Type w)
    [OrderedMonad m] [OrderedMonad n] extends MonadLiftT m n where
  monadLift_mono {α} : Monotone (@monadLift α)

CategoryTheory.NatTrans in Mathlib.CategoryTheory.NatTrans

isEmptyElim in Mathlib.Logic.IsEmpty

ContT in Mathlib.Control.Monad.Cont

List.zip in Init.Data.List.Basic

deriving Repr, DecidableEq

def defaultOracle [spec.FiniteRange] : QueryImpl spec Option where
  impl | q => do return q.defaultOutput

Vector.range in Init.Data.Vector.Basic

Sum.inl in Init.Core

def IND_CCA_Game (encAlg : AsymmEncAlg m M PK SK C)
    (adversary : encAlg.IND_CCA_Adversary) : ProbComp Unit :=
  encAlg.exec do
    let (pk, sk) ← encAlg.keygen
    let b ← encAlg.lift_probComp ($ᵗ Bool)
    let b' ← (simulateQ (encAlg.IND_CCA_oracleImpl pk sk b) (adversary.main pk)).run' none
    guard (b = b')

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

<all_available_lemmas>
@[simp]
lemma evalDist_map (oa : OracleComp spec α) (f : α → β) :
    evalDist (f <$> oa) = f <$> (evalDist oa)

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

lemma probEvent_def (oa : OracleComp spec α) (p : α → Prop) :
    [p | oa] = (evalDist oa).run.toOuterMeasure (Option.some '' {x | p x})

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

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

@[simp low]
lemma probOutput_eq_zero_iff : [= x | oa] = 0 ↔ x ∉ oa.support

lemma mem_support_iff_probOutput_ne_zero : x ∈ oa.support ↔ [= x | oa] ≠ 0

lemma mem_support_iff_of_evalDist_eq {oa : OracleComp spec α} {oa' : OracleComp spec' α}
    (h : evalDist oa = evalDist oa') (x : α) : x ∈ oa.support ↔ x ∈ oa'.support

lemma probOutput_congr {x y : α} {oa : OracleComp spec α} {oa' : OracleComp spec' α}
    (h1 : x = y) (h2 : evalDist oa = evalDist oa') : [= x | oa] = [= y | oa']

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 probEvent_map (q : β → Prop) : [q | f <$> oa] = [q ∘ f | oa]

lemma probEvent_comp (q : β → Prop) : [q ∘ f | oa] = [q | f <$> oa]

@[simp] lemma support_pure (x : α) :
    (pure x : OracleComp spec α).support = {x}

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

@[simp] lemma support_map (oa : OracleComp spec α) (f : α → β) :
    (f <$> oa).support = f '' oa.support

@[simp]
lemma probOutput_seq_map_vector_cons_eq_mul' [spec.FiniteRange] [spec.DecidableEq]
    (xs : List.Vector α (n + 1)) :
    [= xs | (λ xs x ↦ x ::ᵥ xs) <$> ob <*> oa] = [= xs.head | oa] * [= xs.tail | ob]

lemma ProbComp.advantage₂_comm (p q : ProbComp Unit) : p.advantage₂ q = q.advantage₂ p

@[simp] lemma allWhen_failure_iff :
    (failure : OracleComp spec α).allWhen Q F possible_outputs ↔ F

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

@[simp]
lemma evalDist_comp_some (oa : OracleComp spec α) :
    (evalDist oa).run ∘ some = ([= · | oa])

@[simp low]
lemma probOutput_eq_one_iff :
    [= x | oa] = 1 ↔ [⊥ | oa] = 0 ∧ oa.support = {x}

lemma ProbComp.advantage_eq_half_sub_probFailure (p : ProbComp Unit) :
    p.advantage = |1 / 2 - ([⊥ | p]).toReal

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)

lemma probOutput_bind_eq_tsum_subtype (y : β) :
    [= y | oa >>= ob] = ∑' x : oa.support, [= x | oa] * [= y | ob x]

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

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

@[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] lemma not_one_lt_probEvent : ¬ 1 < [p | oa]

@[simp]
lemma support_replicate [spec.FiniteRange] (oa : OracleComp spec α) (n : ℕ) :
    (oa.replicate n).support = {xs | xs.length = n ∧ ∀ x ∈ xs, x ∈ oa.support}

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

example : support (do
    let b ← coin; let b' ← coin
    let x ← (if b && b' then return 0 else return 1);
    let z ← (if b && b' then return x else return 0);
    return (x * z)) = {0}

@[simp] lemma supportWhen_pure (x : α) :
    (pure x : OracleComp spec α).supportWhen poss = {x}

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

@[simp]
lemma evalDist_apply_eq_zero_iff (x : Option α) :
    (evalDist oa).run x = 0 ↔ x.rec ([⊥ | oa] = 0) (· ∉ oa.support)

lemma probOutput_seq_map_eq_tsum_ite [spec.FiniteRange] [DecidableEq γ]
    (z : γ) : [= z | f <$> oa <*> ob] =
      ∑' (x : α) (y : β), if z = f x y then [= x | oa] * [= y | ob] else 0

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

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

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

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

@[simp]
lemma not_neverFails_failure : ¬ neverFails (failure : OracleComp spec α)

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

theorem Correct [DecidableEq P] : (elgamalAsymmEnc G P).PerfectlyCorrect

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

@[simp] lemma support_coin : coin.support = {true, false}

lemma probEvent_replicate_of_probEvent_cons [spec.FiniteRange]
    (p : List α → Prop) (hp : p []) (q : α → Prop) (hq : ∀ x xs, p (x :: xs) ↔ q x ∧ p xs) :
    [p | oa.replicate n] = [q | oa] ^ n

@[simp]
lemma pure_inj (x y : α) : (pure x : OracleComp spec α) = pure y ↔ x = y

lemma probFailure_query : [⊥ | (query i t : OracleComp spec _)] = 0

lemma Function.injective2_swap_iff {α β γ : Type*} (f : α → β → γ) :
    (Function.swap f).Injective2 ↔ f.Injective2

@[simp] lemma apply_eq (q : OracleQuery spec α) : loggingOracle.impl q =
    do let u ← q; tell (QueryLog.singleton q u); return u

lemma probOutput_seq_map_prod_mk_eq_mul' :
    [= (x, y) | (λ x y ↦ (y, x) : β → α → α × β) <$> ob <*> oa] = [= x | oa] * [= y | ob]

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

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

@[simp] lemma purePower_A (B : Type u) : (purePower B).A = PUnit

@[simp]
protected lemma impl_apply_eq (q : OracleQuery spec α) :
    countingOracle.impl q = (tell (QueryCount.single q.index) *> liftM q)

@[simp]
lemma support_generateSeed : (generateSeed spec qc js).support =
    {seed | ∀ i, (seed i).length = qc i * js.count i}

@[simp]
lemma mk_pure_eq_pure [Monad m] (x : α) :
  StateT.mk (λ s ↦ pure (x, s)) = (pure x : StateT σ m α)

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

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

lemma mul_abs_of_nonneg (h : 0 ≤ a) : a * |b

lemma probEvent_liftM_eq_inv_mul [Fintype α] (q : OracleQuery spec α)
    (p : α → Prop) [DecidablePred p] : [p | (q : OracleComp spec _)] =
      (↑(Fintype.card α))⁻¹ * (Finset.univ.filter p).card

@[simp]
lemma probOutput_pure [DecidableEq α] (y : α) :
    [= y | (pure x : OracleComp spec α)] = if y = x then 1 else 0

lemma mem_support_vector_mapM {n} {f : α → OracleComp spec β} {as : Vector α n} {x : Vector β n} :
    x ∈ (Vector.mapM f as).support ↔ ∀ i : Fin n, x[i] ∈ (f as[i]).support

lemma probOutput_true_eq_probEvent {α} {m : Type → Type u} [Monad m] [HasEvalDist m]
    (mx : m α) (p : α → Prop) : Pr{let x ← mx}[p x] = Pr[p | mx]

lemma probEvent_eq_tsum_ite (mx : m α) (p : α → Prop) [DecidablePred p] :
    Pr[p | mx] = ∑' x : α, if p x then Pr[= x | mx] else 0

@[simp]
lemma run_failure [Monoid ω] {α : Type u} : (failure : WriterT ω m α).run = failure

@[simp]
lemma monad_pure_def (x : α) : (pure x : FreeM P α) = FreeM.pure x

@[simp] lemma supportWhen_query (q : OracleQuery spec α) :
    (q : OracleComp spec α).supportWhen poss = poss q

theorem Hybrid_2_advantage_zero : (Hybrid_2 adv).advantage' = 0

lemma not_mem_support_iff_probOutput_eq_zero : x ∉ oa.support ↔ [= x | oa] = 0

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

@[simp] lemma one_le_probFailure_iff : 1 ≤ Pr[⊥ | mx] ↔ Pr[⊥ | mx] = 1

lemma exists_eq_of_isPure {oa : OracleComp spec α} (h : isPure oa) : ∃ x, oa = pure x

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

theorem bind_comm_triple_swap_23 {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)) =
    (ma >>= fun a => mc >>= fun c => mb >>= fun b => f (a, b, c))

@[simp] lemma probOutput_le_one : Pr[= x | mx] ≤ 1

@[simp]
lemma construct_pure (x : α) :
    OracleComp.construct h_pure h_query_bind h_failure (pure x) = h_pure x

@[simp]
lemma probEvent_liftComp [spec.FiniteRange] [superSpec.FiniteRange]
    (oa : OracleComp spec α) (p : α → Prop) [DecidablePred p] :
    [p | liftComp oa superSpec] = [p | oa]

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

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

@[simp] -- This doesn't hold without lawful monad
lemma mmap_map [LawfulMonad m] [LawfulMonad n]
    (F : m →ᵐ n) (x : m α) (g : α → β) : F (g <$> x) = g <$> F x

@[simp] lemma selfMonomial_B (S : Type u) (a : (selfMonomial S).A) : (selfMonomial S).B a = S

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

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

@[simp]
lemma one_eq_probEvent_iff' [spec.DecidableEq] [DecidableEq α] :
    1 = [p | oa] ↔ [⊥ | oa] = 0 ∧ ∀ x ∈ oa.finSupport, p x

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

@[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]
lemma Finset.count_toList {α} [DecidableEq α] (x : α) (s : Finset α) :
    s.toList.count x = if x ∈ s then 1 else 0

@[simp]
lemma probOutput_list_mapM {α β : Type*} [spec.FiniteRange] (xs : List α)
    (f : α → OracleComp spec β) (ys : List β) : [= ys | xs.mapM f] = if ys.length = xs.length
      then (List.zipWith (fun x y => [= y | f x]) xs ys).prod else 0

lemma probOutput_uniformBool_not_decide_eq_decide {ob : ProbComp Bool} :
    [= true | do let b ←$ᵗ Bool; let b' ← ob; return !decide (b = b')] =
      [= true | do let b ←$ᵗ Bool; let b' ← ob; return decide (b = b')]

@[simp] lemma probFailure_lt_top : Pr[⊥ | mx] < ∞

@[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 probFailure_replicate [spec.FiniteRange] :
    [⊥ | oa.replicate n] = 1 - (1 - [⊥ | oa]) ^ n

@[simp]
lemma tsum_probOutput_add_probFailure (oa : OracleComp spec α) :
    ∑' x, [= x | oa] + [⊥ | oa] = 1

lemma probFailure_bind_eq_sub_mul {oa : OracleComp spec α} {ob : α → OracleComp spec β}
    (r : ℝ≥0∞) (h : ∀ x, [⊥ | ob x] = r) :
    [⊥ | oa >>= ob] = 1 - (1 - [⊥ | oa]) * (1 - r)

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

@[simp]
lemma map_bind (f : BindEquiv m n) {α β : Type u} (x : m α) (y : α → m β) :
    f.toFun (x >>= y) = f.toFun x >>= (fun a => f.toFun (y a))

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

@[simp]
lemma probEvent_liftM_eq_mul_inv [Fintype α] (q : OracleQuery spec α)
    (p : α → Prop) [DecidablePred p] : [p | (q : OracleComp spec _)] =
      (Finset.univ.filter p).card * (↑(Fintype.card α))⁻¹

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

lemma probOutput_bind_ite_failure_eq_tsum [spec.FiniteRange] [DecidableEq β]
    (oa : OracleComp spec α) (f : α → β) (p : α → Prop) [DecidablePred p] (y : β) :
    [= y | oa >>= fun x => if p x then pure (f x) else failure] =
      ∑' x : α, if p x ∧ y = f x then [= x | oa] else 0

protected lemma bind_def (oa : OracleComp spec α) (ob : α → OracleComp spec β) :
    oa >>= ob = OptionT.bind oa ob

lemma probFailure_def (mx : m α) : Pr[⊥ | mx] = (evalDist mx).run none

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

@[simp]
lemma Fin_Bound_modulus {n : ℕ} (x : Fin n) : Fin_Bound x n

theorem frame_rule {P : PreCondition σ} {Q : PostCondition σ α}
    {comp : StateM σ α} (h : HoareTriple P comp Q) (R : PreCondition σ) :
    HoareTriple (fun s => P s ∧ R s) comp (fun s x s' => Q s x s' ∧ R s)

@[simp]
lemma countQ_append (log log' : QueryLog spec) (i : ι) :
    (log ++ log').countQ i = log.countQ i + log'.countQ i

@[simp] lemma probFailure_eq : probFailure p = 0

@[simp] lemma neverFails_uniformOfFintype : neverFails ($ᵗ α)

@[simp]
lemma probOutput_seq_map_cons_eq_mul [spec.FiniteRange] [spec.DecidableEq] (xs : List α) :
    [= xs | cons <$> oa <*> ob] = if h : xs.isEmpty then 0 else
      [= xs.head (h ∘ List.isEmpty_iff.2) | oa] * [= xs.tail | ob]

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

@[simp]
lemma probFailure_add_tsum_probOutput (oa : OracleComp spec α) :
    [⊥ | oa] + ∑' x, [= x | oa] = 1

@[simp]
theorem vectorofFn_get {α : Type} {n : ℕ} (v : Fin n → α) : (Vector.ofFn v).get = v

lemma probEvent_eq_sum_fintype_ite [DecidablePred p] [Fintype α] :
    [p | oa] = ∑ x : α, if p x then [= x | oa] else 0

@[simp]
lemma probOutput_uniformFin (x : Fin (n + 1)) : [= x | $[0..n]] = ((n : ℝ≥0∞) + 1)⁻¹

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

lemma liftComp_def (oa : OracleComp spec α) :
    liftComp oa superSpec = simulateQ (m := OracleComp superSpec) ⟨liftM⟩ oa

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

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

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

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

lemma isQueryBound_def (oa : OracleComp spec α) (qb : QueryCount spec) :
    IsQueryBound oa qb ↔ ∀ qc ∈ (snd <$> (simulateQ countingOracle oa).run).support, qc ≤ qb

@[simp] theorem extend_eq_map_duplicate {β : Type u} (f : w α → β) :
  extend wa f = Functor.map f (duplicate wa)

lemma negligible_zero : negligible 0

lemma not_noFailure_of_probFailure_pos {oa : OracleComp spec α} (h : 0 < [⊥ | oa]) :
    ¬ neverFails oa

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 evalDist_comp_pure' (f : α → β) : evalDist ∘ (pure : β → m β) ∘ f = pure ∘ f

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

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

@[simp]
lemma probOutput_coin (b : Bool) : [= b | coin] = 2⁻¹

@[simp]
lemma map_bind_inv (f : BindEquiv m n) {α β : Type u} (x : n α) (y : α → n β) :
    f.invFun (x >>= y) = f.invFun x >>= (fun a => f.invFun (y a))

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

@[simp] lemma probOutput_lt_top : Pr[= x | mx] < ∞

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

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

@[simp]
lemma evalDist_coin : evalDist coin = OptionT.lift (PMF.uniformOfFintype Bool)

lemma probOutput_map_eq_tsum_subtype (y : β) :
    [= y | f <$> oa] = ∑' x : {x ∈ oa.support | y = f x}, [= x | oa]

@[simp]
lemma takeAtIndex_length (seed : QuerySeed spec) (i : ι) :
    seed.takeAtIndex i (seed i).length = seed

lemma mem_support_of_mem_finSupport {x : α} (hx : x ∈ oa.finSupport) : x ∈ oa.support

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

lemma query_eq_pure_iff_false : (q : OracleComp spec β) = pure y ↔ False

@[simp] lemma withCounting_apply {α} (so : QueryImpl spec m) (q : OracleQuery spec α) :
    so.withCounting.impl q = tell (QueryCount.single q.index) *> ↑(so.impl q)

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

lemma Fin_bound_shift_cast_vec {p χ m : ℕ} {v : Vector (Fin (2*χ + 1)) m} [NeZero p] (h : p > 2*χ) :
    Fin_Bound_vec (v.map (fun t ↦ (Fin.castLE h t) - (Fin.ofNat p χ))) χ

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

lemma probOutput_map_eq_probEvent [spec.FiniteRange]
    (oa : OracleComp spec α) (f : α → β) (y : β) :
    [= y | f <$> oa] = [fun x => f x = y | oa]

@[simp] lemma support_uniformOfFintype : ($ᵗ α).support = Set.univ

lemma probOutput_cons_seq_map_cons_eq_mul [spec.FiniteRange] [spec.DecidableEq] (x : α)
    (xs : List α) : [= x :: xs | cons <$> oa <*> ob] = [= x | oa] * [= xs | ob]

@[simp] lemma probEvent_eq : probEvent p = p.run.toOuterMeasure ∘ Set.image some

@[simp]
lemma mapM_map' {m : Type v → Type w} [AlternativeMonad m] [LawfulAlternative m]
    [LawfulMonad m] (qm : {α : Type v} → OracleQuery spec α → m α)
    (oa : OracleComp spec α) (f : α → β) :
    (f <$> oa).mapM failure qm = f <$> oa.mapM failure qm

@[simp] lemma probFailure_lt_top : [⊥ | oa] < ∞

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

@[simp]
theorem sumComm_symm :
    (sumComm P Q).symm = sumComm Q P

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

@[simp]
theorem modifyThe_eq (f : σ → σ) :
    modifyThe σ (m := m) f = (do set (f (← MonadStateOf.get)))

lemma apply_eq_apply_of_mem_support_fork (x₁ x₂ : α)
    (h : (x₁, x₂) ∈ (fork main qb js i cf).support) : cf x₁ = cf x₂

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

lemma probOutput_false_eq_probOutput_true_not {ob : OracleComp spec Bool} :
    [= false | ob] = [= true | do let b ← ob; return !b]
</all_available_lemmas>

<local_ctx>
import VCVio.OracleComp.DistSemantics.Monad

namespace OracleComp

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

variable (oa : OracleComp spec α) (og : OracleComp spec (α → β))

section seq_map

variable (oa : OracleComp spec α) (ob : OracleComp spec β) (f : α → β → γ)
</local_ctx>

<target_theorem>
lemma probEvent_seq_map_eq_probEvent_comp_uncurry [spec.FiniteRange]
    (p : γ → Prop) : [p | f <$> oa <*> ob] =
      [p ∘ f.uncurry | Prod.mk <$> oa <*> ob] :=
</target_theorem>

