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

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

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)

def countingOracle : QueryImpl spec (WriterT (QueryCount spec) (OracleComp spec)) :=
  idOracle.withCounting

noncomputable def probFailure (oa : OracleComp spec α) : ℝ≥0∞ :=
  (evalDist oa).run none

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

@[reducible] def QueryCount (_spec : OracleSpec ι) : Type u := ι → ℕ

instance QueryImpl.Inhabited [∀ i, Inhabited (spec.range i)] [Pure m] :
  Inhabited (QueryImpl spec m) := ⟨{impl q := pure q.defaultOutput}⟩

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

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

def coseq (za : Zipper α) (zb : Zipper β) : Zipper (α × β) :=
  sorry

Functor.map in Init.Prelude

def unifOracle [∀ i, SelectableType (spec.range i)] :
    QueryImpl spec ProbComp where
  impl | query i _ => $ᵗ spec.range i

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

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

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

CategoryTheory.MonoidalCategory in Mathlib.CategoryTheory.Monoidal.Category

AddGroup in Mathlib.Algebra.Group.Defs

List.replicate in Init.Data.List.Basic

PMF.instMonad in Mathlib.Probability.ProbabilityMassFunction.Monad

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

MonadStateOf.modifyGet in Init.Prelude

instance (n : ℕ) : Fintype (BitVec n) :=

LawfulMonad in Init.Control.Lawful.Basic

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

protected def mapM [Pure m] [Bind m] (s : (a : P.A) → m (P.B a)) : FreeM P α → m α
  | .pure a => Pure.pure a
  | .roll a r => (s a) >>= (λ u ↦ (r u).mapM s)

Vector.get in Init.Data.Vector.Basic

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

instance : Coe (BindEquiv m n) (BindHom n m) where
  coe f := ⟨f.toNatEquiv, f.map_bind_inv⟩

def Hybrid_0 : ProbComp Bool :=
  IND_CPA_OneTime_Game (encAlg := uniformRegevAsymmEnc n m p χ he) adv

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

protected def id (P : PFunctor.{uA, uB}) : Lens P P where
  toFunA := id
  toFunB := fun _ => id

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

List.replicateTR in Init.Data.List.Basic

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

def extract [Extract f] [Extract g] {a : Type u₃} (day : Day f g a) : a :=
  
  day.map' (Extract.extract day.fa) (Extract.extract day.gb)

instance : Extract Id where
  extract := id

Finset.card in Mathlib.Data.Finset.Card

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

instance instMonadLift [Bind m] : MonadLift m (FreeContT f m) where
  monadLift := lift

Bind in Init.Prelude

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

def defaultResult [spec.FiniteRange] (oa : OracleComp spec α) : Option α :=
  oa.mapM (fail := none) (query_map := some ∘ OracleQuery.defaultOutput)

@[simps]
def tensorX : P ⊗ X ≃ₚ P where
  equivA := _root_.Equiv.prodPUnit P.A
  equivB := fun a => _root_.Equiv.prodPUnit (P.B a.1)

OptionT.fail in Init.Control.Option

NeZero in Init.Data.NeZero

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

require "leanprover-community" / "mathlib" @ git "v4.24.0-rc1"

IsEmpty in Mathlib.Logic.IsEmpty

instMonadFunctorTOfMonadFunctor in Init.Prelude

instance {P : PreCondition σ} {s' : σ} :
    Inhabited (StrongestPostcondition P (set s' : StateM σ Unit)) where
  default := ⟨fun s _ s'' => P s ∧ s'' = s', HoareTriple.set_rule_forward P s',
    fun Q' hQ' _ => by admit /- proof elided -/
    ⟩

def MonoCont (r : Type v) [Preorder r] : Type u → Type max u v
  | α => {m : Cont r α // ∀ p p' : α → r, (∀ a, p a ≤ p' a) → m p ≤ m p'}

@[simp]
instance {P : PFunctor.{uA, uB}} [inst : P.Fintype] : ∀ a, Fintype (P.B a) :=
  fun a => inst.fintype_B a

Decidable.isFalse in Init.Prelude

IO.userError in Init.System.IOError

def regevAsymmEnc (n m p : ℕ) [hp2 : p.AtLeastTwo] (errSampKG : ProbComp (Fin p)) :
    AsymmEncAlg ProbComp (M := Bool) (PK := Matrix (Fin n) (Fin m) (Fin p) × Vector (Fin p) m)
     (SK := Vector (Fin p) n) (C := Vector (Fin p) n × Fin p) where
  keygen := do
    let A ←$ᵗ Matrix (Fin n) (Fin m) (Fin p)
    let s ←$ᵗ Vector (Fin p) n
    let e ← (Vector.range m).mapM (fun _ ↦ errSampKG)
    return ((A, Vector.ofFn (Matrix.vecMul s.get A) + e), s)
  encrypt := λ (A, y) msg ↦ do
    let r2 ←$ᵗ Vector (Fin 2) m
    let r := (r2.map (Fin.castLE hp2.one_lt)).get
    let yr := dotProduct y.get r
    let signal := if msg then 0 else p / 2
    return (Vector.ofFn (Matrix.mulVec A r), yr + (Fin.ofNat p signal))
  decrypt := λ s (a, b) ↦ do
    let sa := dotProduct s.get a.get
    let val := Fin.val (sa - b)
    return if val < p/4 then true else val > 3*p/4
  __ := ExecutionMethod.default

structure MonadEquiv (m : Type u → Type v) [Pure m] [Bind m] (n : Type u → Type w) [Pure n] [Bind n]
    extends NatEquiv m n, PureEquiv m n, BindEquiv m n

instance : LawfulFunctor Zipper where
  id_map    := sorry
  comp_map  := sorry
  map_const := sorry

def enclose (P : PFunctor.{uA, uB}) : Type max uA uA₁ uB uB₁ :=
  Lens P X.{uA₁, uB₁}

def PFunctor.FreeContM (P : PFunctor.{z, y}) (α : Type w) : Type _ :=
  FreeContT P Id.{u} α

OptionT.mk in Init.Control.Option

map_constᵣ {α β : Type u} : (mapConstᵣ : j α → f β → _) = mapᵣ ∘ (Function.const _)

abbrev PreordEnrichedCategory (C : Type u) := EnrichedCategory Preord C

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

@[simps]
def sumCongr {P Q} {R : PFunctor.{uA₃, uB₁}} {S : PFunctor.{uA₄, uB₁}} (e₁ : P ≃ₚ R) (e₂ : Q ≃ₚ S) :
    P + Q ≃ₚ (R + S : PFunctor.{max uA₃ uA₄, uB₁}) where
  equivA := _root_.Equiv.sumCongr e₁.equivA e₂.equivA
  equivB := (Sum.casesOn · (e₁.equivB ·) (e₂.equivB ·))

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

def toList (nel : NonEmptyList α) : List α := nel.head :: nel.tail

@[simps]
def tensorComm :
    (P ⊗ Q : PFunctor.{max uA₁ uA₂, max uB₁ uB₂}) ≃ₚ
    (Q ⊗ P : PFunctor.{max uA₁ uA₂, max uB₁ uB₂}) where
  equivA := _root_.Equiv.prodComm P.A Q.A
  equivB := fun a => _root_.Equiv.prodComm (P.B a.1) (Q.B a.2)

def prodPair {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}}
    (l₁ : Lens P Q) (l₂ : Lens P R) :
    Lens.{uA₁, uB₁, max uA₂ uA₃, max uB₂ uB₃} P (Q * R) :=
  (fun p => (l₁.toFunA p, l₂.toFunA p)) ⇆
    (fun p => Sum.elim (l₁.toFunB p) (l₂.toFunB p))

def Hybrid_12_Reduction : LHL_Consequence_Adv n p := fun x => 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 b' ← adv.distinguish st x
  return b = b'

instance : Extend Stream' where
  extend s f := fun n => f (Stream'.drop n s)

def zeroCoprod :
    Lens.Equiv.{max uA uA₁, uB, uA₁, uB} ((0 : PFunctor.{uA, uB}) + P) P where
  toLens := Lens.sumPair Lens.initial (Lens.id P)
  invLens := Lens.inr
  left_inv := by admit /- proof elided -/

Equiv in Mathlib.Logic.Equiv.Defs

Set.preimage in Mathlib.Data.Set.Operations

Zero in Init.Prelude

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

PEmpty.elim in Init.Core

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

List.filterMap in Init.Data.List.Basic

instance : MonadTransformer OptionT where
  mapMonad _ := inferInstance
  transform _ := inferInstance

Turing.TM2ComputableInPolyTime in Mathlib.Computability.TMComputable

Fin.ofNat in Init.Data.Fin.Basic

OptionT.lift in Init.Control.Option

structure MonadHom (m : Type u → Type v) [Pure m] [Bind m]
    (n : Type u → Type w) [Pure n] [Bind n] extends NatHom m n, PureHom m n, BindHom m n

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

ULift.down in Init.Prelude

WithTop in Mathlib.Order.TypeTags

abbrev ProbComp : Type z → Type (max z 1) := OracleComp unifSpec

MonadControlT in Init.Control.Basic

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

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

OfNat.ofNat in Init.Prelude

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

instance [Monoid ω] [LawfulMonad m] : LawfulMonadLift m (WriterT ω m) where
  monadLift_pure x := map_pure (·, 1) x
  monadLift_bind {α β} x y := by admit /- proof elided -/

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)

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

Summable in Mathlib.Topology.Algebra.InfiniteSum.Defs

@[reducible] def SPMF : Type u → Type u := OptionT PMF

Decidable in Init.Prelude

def bind {P₁ : PreCondition σ} {Q₁ : PostCondition σ α}
    {P₂ : α → PreCondition σ} {Q₂ : α → PostCondition σ β}
    (m : HoareState P₁ α Q₁) (f : ∀ x, HoareState (P₂ x) β (Q₂ x)) :
      HoareState (fun s₁ => P₁ s₁ ∧ ∀ x s₂, Q₁ s₁ x s₂ → P₂ x s₂) β
        (fun s₁ y s₃ => ∃ x s₂, Q₁ s₁ x s₂ ∧ Q₂ x s₂ y s₃)
  | ⟨s₁, h₁⟩ => match m ⟨s₁, h₁.left⟩ with
    | ⟨(x, s₂), h₂⟩ =>
      let ⟨⟨y, s₃⟩, h₃⟩ := f x ⟨s₂, h₁.right x s₂ h₂⟩
      ⟨⟨y, s₃⟩, ⟨x, s₂, h₂, h₃⟩⟩

Sum in Init.Core

def IND_CPA_parallelTesting_reduction
    (adversary : (elgamalAsymmEnc G P).IND_CPA_adversary) :
    parallelTestingAdversary G P := fun x x₁ x₂ x₃ => do
  let so : QueryImpl (P × P →ₒ P × P) ProbComp := ⟨fun (query () (m₁, _m₂)) =>
    return (x₂, m₁ * x₃)⟩
  simulateQ (idOracle ++ₛₒ so) (adversary (x, x₁))

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

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

Equiv.sigmaPUnit in Mathlib.Logic.Equiv.Prod

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

@[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 Chart (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) where
  toFunA : P.A → Q.A
  toFunB : ∀ a, P.B a → Q.B (toFunA a)

class LawfulMonadRelation (m : Type u → Type v) (n : Type u → Type w) [Monad m] [Monad n]
    [MonadRelation m n] where
  monadRel_pure {α : Type u} (a : α) : monadRel (pure a : m α) (pure a : n α)
  monadRel_bind {α β : Type u} {ma : m α} {mb : α → m β} {na : n α} {nb : α → n β}
    (ha : monadRel ma na) (hb : ∀ a, monadRel (mb a) (nb a)) : monadRel (ma >>= mb) (na >>= nb)

Option.elimM in Init.Data.Option.Basic

class Commutative (m : Type u → Type v) [Monad m] where
  bind_comm {α β} (ma : m α) (mb : m β) : CommutativeAt m ma mb

alias coprod := sum

class CoseqRight (w : Type u → Type v) where
   
  coseqRight : {α β : Type u} → w α → w β → w β

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

structure SecAdv {ι : Type u} [DecidableEq ι]
    (spec : OracleSpec ι) (α β : Type u) where
  run : α → OracleComp spec β
  qb : ι → ℕ
  qb_isQueryBound (x : α) : IsQueryBound (run x) (qb)
  activeOracles : List ι
  mem_activeOracles_iff (i : ι) : i ∈ activeOracles ↔ qb i ≠ 0

instance : LawfulMonadTransformer (ReaderT ρ) where
  monad_functor := inferInstance
  liftOf_pure _ := rfl
  liftOf_bind _ _ := rfl

def monadOfId (M : RelativeMonad C _ (𝟭 _)) : Monad C where
  toFunctor := M.inducedFunctor
  η := { app X := M.η }
  μ := NatTrans.mk (fun X => M.μ (𝟙 (M.T X)))
    (fun X Y f => by admit /- proof elided -/
    )
  right_unit _ := by admit /- proof elided -/

CategoryTheory.inv in Mathlib.CategoryTheory.Iso

@[simps]
def prodCongr {P Q} {R : PFunctor.{uA₃, uB₃}} {S : PFunctor.{uA₄, uB₄}}
    (e₁ : P ≃ₚ R) (e₂ : Q ≃ₚ S) : P * Q ≃ₚ (R * S : PFunctor.{max uA₃ uA₄, max uB₃ uB₄}) where
  equivA := _root_.Equiv.prodCongr e₁.equivA e₂.equivA
  equivB := fun a => _root_.Equiv.sumCongr (e₁.equivB a.1) (e₂.equivB a.2)

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

@[always_inline, inline, simp]
abbrev MonadTransformer.lift [MonadTransformer t] {m} [Monad m] : m α → t m α :=
  liftOf m

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

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

Fintype.subtypeEq in Mathlib.Data.Fintype.Basic

def getQ (log : QueryLog spec) (i : ι) : List (spec.domain i × spec.range i) :=
  List.foldr (fun ⟨j, t, u⟩ xs => if h : j = i then h ▸ (t, u) :: xs else xs) [] log

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

@[reducible, inline] def coin : OracleComp coinSpec Bool :=
  coinSpec.query () ()

instance [MonadTransformer t] [Monad m] : MonadLift m (t m) := MonadTransformer.transform m

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

instance instFunctor [Functor f] [Functor g] : Functor (Day f g) where
  map {a b : Type u₃} (k : a → b) (day : Day f g a) : Day f g b :=
    
    ⟨fun (x : day.α) (y : day.β) => k (day.map' x y), day.fa, day.gb⟩

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

@[ext]
structure Equiv (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) where
  toLens : Lens P Q
  invLens : Lens Q P
  left_inv : comp invLens toLens = Lens.id P := by admit /- proof elided -/

@[reducible, inline] def uniformFin (n : ℕ) : ProbComp (Fin (n + 1)) :=
  unifSpec.query n ()

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

HEq in Init.Prelude

String.mk in Init.Data.String.Bootstrap

Prod in Init.Prelude

def generateSeedT (spec : OracleSpec ι) [∀ i, SelectableType (spec.range i)]
    (qc : ι → ℕ) (activeOracles : List ι) :
    StateT (QuerySeed spec) ProbComp Unit :=
  for j in activeOracles do
    modify (QuerySeed.addValues (← ($ᵗ spec.range j).replicate (qc j)))

instance : LawfulCoapplicative Zipper where
  coseqLeft_eq  := sorry
  coseqRight_eq := sorry
  coseq_assoc   := sorry

IO.println in Init.System.IO

NatPow in Init.Prelude

Array.mapM' in Init.Data.Array.BasicAux

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

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

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

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

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

def simulation_setup (message_content : String) : OracleComp unifSpec (Option SimulationData) := do
  let facebook_key := BitVec.ofNat 256 123456789
  let context : Context := {
    sender_id := BitVec.ofNat 256 1001, recipient_id := BitVec.ofNat 256 1002,
    timestamp := 1730230302,
    message_id := 123 }
  let nonce ← generate_nonce
  let franking_tag  := generate_franking_tag nonce message_content
  let encrypted_msg := prepare_encrypted_message message_content nonce
  let reporting_tag := generate_reporting_tag franking_tag context facebook_key
  let package : MessagePackage := {
    encrypted_message := encrypted_msg,
    franking_tag := franking_tag,
    reporting_tag := reporting_tag,
    context := context,
    nonce := nonce }
  let maybeVerifiedMsg ← verify_message_package package
  match maybeVerifiedMsg with
  | none => 
    return none
  | some verified_msg =>
    return some { verified_msg := verified_msg
                  message_package := package
                  facebook_key := facebook_key }

instance : Coe (BindEquiv m n) (BindHom m n) where
  coe f := ⟨f.toNatEquiv, f.map_bind'⟩

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

Or.inl 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 -/

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

def logQuery {α} (log : QueryLog spec) (q : OracleQuery spec α) (u : α) :
    QueryLog spec := log ++ singleton q u

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

instance instLawfulMonad : LawfulMonad (FreeContT f m) := LawfulMonad.mk'
  (id_map := by admit /- proof elided -/
  )
  (pure_bind := by admit /- proof elided -/
  )
  (bind_assoc := by admit /- proof elided -/
  )

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

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

Polynomial in Mathlib.Algebra.Polynomial.Basic

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

Computation in Mathlib.Data.Seq.Computation

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

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

Group in Mathlib.Algebra.Group.Defs

instance : Mul PFunctor.{uA, uB} where
  mul := prod

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

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

instance instExtend [Comonad w] : Extend (StoreT s w) where
  extend storet k := { runStoreT := Extend.extend storet.runStoreT (fun w'sa s' => k { runStoreT := w'sa, pos := s' }), pos := storet.pos }

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

instance : Commutative Id where
  bind_comm := fun _ _ => rfl

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

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)

instance : Coapplicative Id where

AddLECancellable in Mathlib.Algebra.Order.Monoid.Unbundled.Basic

deriving Repr, DecidableEq

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

def compAssoc : (P ◃ Q) ◃ R ≃ₗ P ◃ (Q ◃ R) where
  toLens := (fun ⟨⟨pa, qf⟩, rf⟩ => ⟨pa, fun pb => ⟨qf pb, fun qb => rf ⟨pb, qb⟩⟩⟩) ⇆
            (fun _ ⟨pb, ⟨qb, rb⟩⟩ => ⟨⟨pb, qb⟩, rb⟩)
  invLens := (fun ⟨pa, g⟩ => ⟨⟨pa, fun pb => (g pb).1⟩, fun ⟨pb, qb⟩ => (g pb).2 qb⟩) ⇆
             (fun _ ⟨⟨pb, qb⟩, rb⟩ => ⟨pb, ⟨qb, rb⟩⟩)
  left_inv := rfl
  right_inv := rfl

ContT in Mathlib.Control.Monad.Cont

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

AddTorsor in Mathlib.Algebra.AddTorsor.Defs
</all_available_defs>

<all_available_lemmas>
@[simp]
lemma evalDist_orElse [h : spec.FiniteRange] (oa oa' : OracleComp spec α) :
    evalDist (oa <|> oa') = (evalDist oa <|> evalDist oa')

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

@[simp]
lemma support_orElse {ι : Type u} {spec : OracleSpec ι} {α : Type u}
    (oa oa' : OracleComp spec α) [Decidable oa.neverFails] : (oa <|> oa').support =
      if oa.neverFails then oa.support else oa.support ∪ oa'.support

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

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

lemma probFailure_def (oa : OracleComp spec α) :
    [⊥ | oa] = (evalDist oa).run none

lemma support_evalDist : (evalDist oa).run.support = if [⊥ | oa] = 0 then
    some '' oa.support else insert none (some '' oa.support)

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

@[simp] lemma evalDist_uniformSelectList (xs : List α) : evalDist ($ xs) =
    match xs with

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

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

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

@[simp] lemma not_one_lt_probOutput : ¬ 1 < Pr[= x | mx]

@[simp] lemma finSupport_uniformOfFintype [Fintype α] [DecidableEq α] :
    ($ᵗ α).finSupport = Finset.univ

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

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

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 replicateTR_zero : replicate 0 oa = return []

lemma probEvent_eqRec (q : β → Prop) :
    [q | h ▸ oa] = [λ x ↦ q (h ▸ x) | oa]

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

lemma probFailure_bind_le_of_forall {oa : OracleComp spec α} {s : ℝ≥0∞}
    -- TODO: this should be a general type of `uniformOutput` computations
    (h' : [⊥ | oa] = s) (ob : α → OracleComp spec β) {r : ℝ≥0∞}
    (hr : ∀ x ∈ oa.support, [⊥ | ob x] ≤ r) : [⊥ | oa >>= ob] ≤ s + (1 - s) * r

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

@[simp] lemma mapM_failure : (failure : OracleComp spec α).mapM fail qm = fail

lemma mul_abs_of_nonpos (h : a < 0) : a * |b

@[simp] lemma evalDist_eq : evalDist p = p

@[simp]
lemma mapM_ite (p : Prop) [Decidable p] (oa oa' : OracleComp spec α) :
    (ite p oa oa').mapM fail qm = ite p (oa.mapM fail qm) (oa'.mapM fail qm)

lemma getQ_singleton {α} (q : OracleQuery spec α) (u : α) (i : ι) :
    getQ (singleton q u) i = match q with

@[simp]
lemma probOutput_eq_one_iff' [spec.DecidableEq] [DecidableEq α] :
    [= x | oa] = 1 ↔ [⊥ | oa] = 0 ∧ oa.finSupport = {x}

lemma probEvent_pure_eq_zero {p : α → Prop} {x : α} (h : ¬ p x) :
    [p | (pure x : OracleComp spec α)] = 0

@[simp]
lemma run_map (x : WriterT ω m α) (f : α → β) : (f <$> x).run = Prod.map f id <$> x.run

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

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

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

lemma monad_failure_eq [Monad m] [Alternative m] :
    (failure : StateT σ m α) = StateT.failure

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

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

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

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

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

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

lemma evalDist_lift_query [superSpec.FiniteRange] [Fintype α] [Nonempty α]
    (q : OracleQuery spec α) :
    evalDist ((q : OracleQuery superSpec α) : OracleComp superSpec α) =
      OptionT.lift (PMF.uniformOfFintype α)

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 card_bitVec (n : ℕ) : Fintype.card (BitVec n) = 2 ^ n

@[simp] lemma support_query_bind (q : OracleQuery spec α) (ob : α → OracleComp spec β) :
    (liftM q >>= ob).support = ⋃ x, (ob x).support

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 purePower_B (B : Type u) (a : (purePower B).A) : (purePower B).B a = B

@[simp]
lemma mem_finSupport_replicate [spec.FiniteRange] [spec.DecidableEq] [DecidableEq α]
    (oa : OracleComp spec α) (n : ℕ)
    (xs : List α) : xs ∈ (oa.replicate n).finSupport ↔
      xs.length = n ∧ xs.all (· ∈ oa.finSupport)

@[simp]
lemma construct_roll (x : P.A) (r : P.B x → FreeM P α) :
    (FreeM.construct h_pure h_roll (FreeM.roll x r) : C (FreeM.roll x r)) =
      (h_roll x r (λ u ↦ FreeM.construct h_pure h_roll (r u)))

@[simp] lemma probOutput_eq : probOutput p = p

@[simp] lemma simulateQ_comp_pure_comp (f : α → β) : simulateQ so ∘ pure ∘ f = pure ∘ f

lemma LWE_Experiment_eq_LWE_Game_01 {n m p : ℕ} [NeZero p] {errSamp : ProbComp (Fin p)}
    {adv : LWE_Adversary n m p} :
    2 * (LWE_Experiment n m p errSamp adv).advantage' =
      (LWE_Game_0 n m p errSamp adv).advantage₂' (LWE_Game_1 n m p adv)

lemma Fin_bound_mul_helper {n b₁ b₂ : ℕ} {x y : Fin n} (h : b₁ * b₂ < n)
  (h₁ : x.val ≤ b₁) (h₂ : y.val + b₂ ≥ n) : Fin_Bound (x * y) (b₁ * b₂)

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

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

lemma isQueryBound_mono {oa : OracleComp spec α} (qb : ι → ℕ) {qb' : ι → ℕ}
    (h' : IsQueryBound oa qb) (h : qb ≤ qb') : IsQueryBound oa qb'

theorem prodMap_comp_prodPair (l₁ : Lens Q W) (l₂ : Lens R X) (f : Lens P Q) (g : Lens P R) :
    (l₁ ×ₗ l₂) ∘ₗ Lens.prodPair f g = Lens.prodPair (l₁ ∘ₗ f) (l₂ ∘ₗ g)

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

@[simp]
lemma run_tell (w : ω) : (tell w : WriterT ω m PUnit).run = pure (⟨⟩, w)

@[simp] lemma failure_ne_query : failure ≠ (q : OracleComp spec β)

lemma mapM_map [LawfulMonad m] (oa : OracleComp spec α) (f : α → β)
    (hfail : ∀ f : α → β, f <$> fail = fail) :
    (f <$> oa).mapM fail qm = f <$> oa.mapM fail qm

@[simp]
lemma probOutput_pos_iff' [spec.DecidableEq] [DecidableEq α] :
    0 < [= x | oa] ↔ x ∈ oa.finSupport

@[simp] lemma isFailure_failure : isFailure (failure : OracleComp spec α) = true

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

@[simp] lemma finSupport_pure [spec.FiniteRange] [DecidableEq α] (x : α) :
    (pure x : OracleComp spec α).finSupport = {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

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

lemma IntLE_imp_NatLE {a b : ℕ} (h : (a : ℤ) ≤ (b : ℤ)) : a ≤ b

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

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

@[simp] lemma probEvent_le_one : [p | oa] ≤ 1

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

@[simp] lemma isPure_query_bind : isPure ((q : OracleComp spec β) >>= oa) = false

lemma probOutput_seq_map_prod_mk_eq_mul :
    [= (x, y) | Prod.mk <$> oa <*> ob] = [= x | oa] * [= y | ob]

@[simp]
lemma liftM_query_stateT {σ : Type v} {α : Type v} (q : OracleQuery spec α) :
  (liftM q : StateT σ (OracleComp spec) α) = liftM (liftM q : OracleComp spec α)

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

lemma X_eq_linear_pUnit : X = linear PUnit

@[simp]
lemma evalDist_eqRec (h : α = β) (oa : OracleComp spec α) :
    evalDist (h ▸ oa) = h ▸ evalDist oa

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

lemma probOutput_map_eq_tsum_subtype_ite [DecidableEq β] (y : β) :
    [= y | f <$> oa] = ∑' x : oa.support, if y = f x then [= x | oa] else 0

theorem exists_log_of_mem_support_fork (x₁ x₂ : α)
    (h : (x₁, x₂) ∈ (fork main qb js i cf).support) :
      ∃ s, cf x₁ = some s ∧ cf x₂ = some s ∧
      ∃ log₁ : QueryLog spec, ∃ hcf₁ : ↑s < log₁.countQ i,
      ∃ log₂ : QueryLog spec, ∃ hcf₁ : ↑s < log₂.countQ i,
      (log₁.getQ i)[s].1 = (log₂.getQ i)[s].1 ∧
      (log₁.getQ i)[s].2 ≠ (log₂.getQ i)[s].2 ∧
      (x₁, log₁) ∈ (simulateQ loggingOracle main).run.support ∧
      (x₂, log₂) ∈ (simulateQ loggingOracle main).run.support

@[simp] lemma simulateQ_seqRight (oa : OracleComp spec α) (ob : OracleComp spec β) :
    simulateQ so (oa *> ob) = simulateQ so oa *> simulateQ so ob

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

@[simp]
lemma mmap_ofLift (m : Type u → Type v) (n : Type u → Type v) [Monad m] [Monad n]
    [MonadLift m n] [LawfulMonadLift m n] {α : Type u}
    (x : m α) : ofLift m n x = liftM x

lemma liftM_query_eq_liftM_liftM {m : Type v → Type z} [MonadLift (OracleComp spec) m] {α : Type v}
    (q : OracleQuery spec α) : (liftM q : m α) = liftM (liftM q : OracleComp spec α)

lemma probFailure_bind_of_neverFails {oa : OracleComp spec α}
    (h : neverFails oa) (ob : α → OracleComp spec β) :
    [⊥ | oa >>= ob] = ∑' x : α, [= x | oa] * [⊥ | ob x]

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

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

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

lemma probOutput_seq_map_eq_mul [spec.FiniteRange] (x : α) (y : β) (z : γ)
    (h : ∀ x' ∈ oa.support, ∀ y' ∈ ob.support, z = f x' y' ↔ x' = x ∧ y' = y) :
    [= z | f <$> oa <*> ob] = [= x | oa] * [= y | ob]

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

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

lemma probOutput_bind_congr_le_sub {γ₁ γ₂ : Type u}
    {oa : OracleComp spec α} {ob : α → OracleComp spec β}
      {oc₁ : α → OracleComp spec γ₁} {oc₂ : α → OracleComp spec γ₂}
    {y : β} {z₁ : γ₁} {z₂ : γ₂}
    (h : ∀ x ∈ oa.support, [= y | ob x] ≤ [= z₁ | oc₁ x] - [= z₂ | oc₂ x]) :
    [= y | oa >>= ob] ≤ [= z₁ | oa >>= oc₁] - [= z₂ | oa >>= oc₂]

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

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

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

@[simp]
lemma support_toFun (q : OracleQuery spec α) :
    support (h.monadLift q : OracleComp superSpec α) = Set.univ

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

lemma monadLift_def (x : m α) :
    (MonadLift.monadLift x : WriterT ω m α) = WriterT.mk ((·, 1) <$> x)

@[simp] lemma simulateQ_ite (p : Prop) [Decidable p] (oa oa' : OracleComp spec α) :
    simulateQ so (ite p oa oa') = ite p (simulateQ so oa) (simulateQ so oa')

@[simp] lemma finSupport_uniformFin (n : ℕ) : ($[0..n]).finSupport = Finset.univ :=
  finSupport_query _

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

lemma neverFailsWhen_simulate {ι' : Type*} {spec' : OracleSpec ι'}
    (oa : OracleComp spec α)
    (possible_outputs : {α : Type v} → OracleQuery spec α → Set α)
    (h : neverFailsWhen oa possible_outputs)
    -- {m : Type v → Type _} [Monad m]
    (so : QueryImpl spec (OracleComp spec'))
    (h' : ∀ {α}, ∀ q : OracleQuery spec α, (so.impl q).support ⊆ possible_outputs q)
    (hso : ∀ {α}, ∀ q : OracleQuery spec α, neverFails (so.impl q)) :
    neverFails (simulateQ so oa)

@[simp] lemma isPure_pure : isPure (pure x : OracleComp spec α) = true

@[simp]
lemma construct_pure (y : α) : FreeMonad.construct h_pure h_roll (pure y) = h_pure y

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]
theorem sumMap_comp_inr (l₁ : Lens P R) (l₂ : Lens Q W) :
    ((l₁ ⊎ₗ l₂) ∘ₗ Lens.inr) = (Lens.inr ∘ₗ l₂)

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

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

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

lemma probEvent_eq_sum_finSupport_ite [spec.DecidableEq] [DecidablePred p] [DecidableEq α] :
    [p | oa] = ∑ x ∈ oa.finSupport, if p x then [= x | oa] else 0

lemma probEvent_true (oa : OracleComp spec α) : [λ _ ↦ true | oa] = 1 - [⊥ | 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]
lemma monadLift_eq_lift (x : P.Obj α) : (x : FreeM P α) = FreeM.lift x

@[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 probEvent_eq_zero_iff' [spec.DecidableEq] [DecidableEq α] :
    [p | oa] = 0 ↔ ∀ x ∈ oa.finSupport, ¬ p x

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

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

theorem IsCoupling.none_iff {α β : Type u} {c : SPMF (α × β)} :
    IsCoupling c (failure : SPMF α) (failure : SPMF β) ↔ c = failure

@[simp] lemma support_uniformFin (n : ℕ) : ($[0..n]).support = Set.univ

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

lemma mem_support_eqRec_iff (oa : OracleComp spec α) (h : α = β) (y : β) :
    y ∈ (h ▸ oa).support ↔ h.symm ▸ y ∈ oa.support

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

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

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

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

lemma probEvent_seq_eq_tsum [spec.FiniteRange] (p : β → Prop) :
    [p | og <*> oa] = ∑' (g : α → β), [= g | og] * [p ∘ g | oa]

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

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

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

lemma probOutput_map_eq_single [spec.FiniteRange] {oa : OracleComp spec α} {f : α → β} {y : β}
    (x : α) (h : ∀ x' ∈ oa.support, y = f x' → x = x') (h' : f x = y) :
    [= y | f <$> oa] = [= x | oa]

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

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 not_one_lt_probFailure : ¬ 1 < [⊥ | oa]

lemma probEvent_seq_map_prod_mk_eq_mul' :
    [λ z ↦ p z.1 ∧ q z.2 | (λ x y ↦ (y, x) : β → α → α × β) <$> ob <*> oa] = [p | oa] * [q | ob]

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

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

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

@[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 allWhen_query_iff (q : OracleQuery spec α) :
    (q : OracleComp spec α).allWhen Q F possible_outputs ↔ Q q

@[simp] theorem bind_pureᵣ [RelativeMonad j m] [LawfulRelativeMonad j m] (x : m α) :
    x >>=ᵣ pureᵣ (j := j) = x
</all_available_lemmas>

<local_ctx>
import VCVio.OracleComp.QueryTracking.CountingOracle

import VCVio.OracleComp.DistSemantics.Alternative

open OracleSpec Prod

namespace OracleComp

section IsQueryBound

variable {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} {α β γ : Type u}

def IsQueryBound (oa : OracleComp spec α) (qb : ι → ℕ) : Prop :=
    ∀ qc ∈ (snd <$> (simulateQ countingOracle oa).run).support, qc ≤ qb
</local_ctx>

<target_theorem>
lemma isQueryBound_iff_probEvent [spec.FiniteRange] {oa : OracleComp spec α} {qb : ι → ℕ} :
    IsQueryBound oa qb ↔
      [(· ≤ qb) | snd <$> (simulateQ countingOracle oa).run <|> return 0] = 1 :=
</target_theorem>

