Distribution Semantics for Computations with Lists and Vectors

This file contains lemmas for probEvent and probOutput of computations involving List. We also include Vector as a related case.

theorem OracleComp.mem_support_seq_map_cons_iff' {ι : Type u} {spec : OracleSpec ι} {α : Type v} (oa : OracleComp spec α) (ob : OracleComp spec (List α)) (xs : List α) : xs ∈ (List.cons <$> oa <*> ob).support ↔ List.recOn xs False fun (x : α) (xs : List α) (x_1 : Prop) => x ∈ oa.support ∧ xs ∈ ob.support

theorem OracleComp.mem_support_seq_map_cons_iff {ι : Type u} {spec : OracleSpec ι} {α : Type v} (oa : OracleComp spec α) (ob : OracleComp spec (List α)) (xs : List α) (h : xs ≠ []) : xs ∈ (List.cons <$> oa <*> ob).support ↔ xs.head h ∈ oa.support ∧ xs.tail ∈ ob.support

theorem OracleComp.cons_mem_support_seq_map_cons_iff {ι : Type u} {spec : OracleSpec ι} {α : Type v} (oa : OracleComp spec α) (ob : OracleComp spec (List α)) (x : α) (xs : List α) : x :: xs ∈ (List.cons <$> oa <*> ob).support ↔ x ∈ oa.support ∧ xs ∈ ob.support

theorem OracleComp.mem_finSupport_seq_map_cons_iff' {ι : Type u} {spec : OracleSpec ι} {α : Type v} (oa : OracleComp spec α) (ob : OracleComp spec (List α)) [spec.FiniteRange] [spec.DecidableEq] [DecidableEq α] (xs : List α) : xs ∈ (List.cons <$> oa <*> ob).finSupport ↔ List.recOn xs False fun (x : α) (xs : List α) (x_1 : Prop) => x ∈ oa.finSupport ∧ xs ∈ ob.finSupport

theorem OracleComp.mem_finSupport_seq_map_cons_iff {ι : Type u} {spec : OracleSpec ι} {α : Type v} (oa : OracleComp spec α) (ob : OracleComp spec (List α)) [spec.FiniteRange] [spec.DecidableEq] [DecidableEq α] (xs : List α) (h : xs ≠ []) : xs ∈ (List.cons <$> oa <*> ob).finSupport ↔ xs.head h ∈ oa.finSupport ∧ xs.tail ∈ ob.finSupport

theorem OracleComp.cons_mem_finSupport_seq_map_cons_iff {ι : Type u} {spec : OracleSpec ι} {α : Type v} (oa : OracleComp spec α) (ob : OracleComp spec (List α)) [spec.FiniteRange] [spec.DecidableEq] [DecidableEq α] (x : α) (xs : List α) : x :: xs ∈ (List.cons <$> oa <*> ob).finSupport ↔ x ∈ oa.finSupport ∧ xs ∈ ob.finSupport

theorem OracleComp.probOutput_cons_seq_map_cons_eq_mul {ι : Type u} {spec : OracleSpec ι} {α : Type v} (oa : OracleComp spec α) (ob : OracleComp spec (List α)) [spec.FiniteRange] [spec.DecidableEq] (x : α) (xs : List α) : [=x :: xs|List.cons <$> oa <*> ob] = [=x|oa] * [=xs|ob]

theorem OracleComp.probOutput_cons_seq_map_cons_eq_mul' {ι : Type u} {spec : OracleSpec ι} {α : Type v} (oa : OracleComp spec α) (ob : OracleComp spec (List α)) [spec.FiniteRange] [spec.DecidableEq] (x : α) (xs : List α) : [=x :: xs|(fun (xs : List α) (x : α) => x :: xs) <$> ob <*> oa] = [=x|oa] * [=xs|ob]

@[simp]

theorem OracleComp.probOutput_seq_map_cons_eq_mul {ι : Type u} {spec : OracleSpec ι} {α : Type v} (oa : OracleComp spec α) (ob : OracleComp spec (List α)) [spec.FiniteRange] [spec.DecidableEq] (xs : List α) : [=xs|List.cons <$> oa <*> ob] = if h : xs.isEmpty = true then 0 else [=xs.head ⋯|oa] * [=xs.tail|ob]

@[simp]

theorem OracleComp.probOutput_map_append_left {ι : Type u} {spec : OracleSpec ι} {α : Type v} [DecidableEq α] [spec.FiniteRange] (xs : List α) (oa : OracleComp spec (List α)) (ys : List α) : [=ys|(fun (x : List α) => xs ++ x) <$> oa] = if List.take xs.length ys = xs then [=List.drop xs.length ys|oa] else 0

@[simp]

theorem OracleComp.probFailure_list_mapM_loop {ι : Type u} {spec : OracleSpec ι} {α : Type u_1} {β : Type u_2} [spec.FiniteRange] (xs : List α) (f : α → OracleComp spec β) (ys : List β) : [⊥|List.mapM.loop f xs ys] = 1 - (List.map (fun (x : α) => 1 - [⊥|f x]) xs).prod

@[simp]

theorem OracleComp.probFailure_list_mapM {ι : Type u} {spec : OracleSpec ι} {α : Type u_1} {β : Type u_2} [spec.FiniteRange] (xs : List α) (f : α → OracleComp spec β) : [⊥|mapM f xs] = 1 - (List.map (fun (x : α) => 1 - [⊥|f x]) xs).prod

@[simp]

theorem OracleComp.probOutput_list_mapM_loop {ι : Type u} {spec : OracleSpec ι} {α : Type u_1} {β : Type u_2} [DecidableEq β] [spec.FiniteRange] (xs : List α) (f : α → OracleComp spec β) (ys zs : List β) : [=zs|List.mapM.loop f xs ys] = if zs.length = xs.length + ys.length ∧ List.take ys.length zs = ys.reverse then (List.zipWith (fun (x : α) (z : β) => [=z|f x]) xs (List.drop ys.length zs)).prod else 0

@[simp]

theorem OracleComp.probOutput_list_mapM {ι : Type u} {spec : OracleSpec ι} {α : Type u_1} {β : Type u_2} [spec.FiniteRange] (xs : List α) (f : α → OracleComp spec β) (ys : List β) : [=ys|mapM f xs] = if ys.length = xs.length then (List.zipWith (fun (x : α) (y : β) => [=y|f x]) xs ys).prod else 0

@[simp]

theorem OracleComp.support_seq_map_vector_cons {ι : Type u} {spec : OracleSpec ι} {α : Type v} {n : ℕ} (oa : OracleComp spec α) (ob : OracleComp spec (List.Vector α n)) : ((fun (x1 : α) (x2 : List.Vector α n) => x1 ::ᵥ x2) <$> oa <*> ob).support = {xs : List.Vector α n.succ | xs.head ∈ oa.support ∧ xs.tail ∈ ob.support}

@[simp]

theorem OracleComp.probOutput_seq_map_vector_cons_eq_mul {ι : Type u} {spec : OracleSpec ι} {α : Type v} {n : ℕ} (oa : OracleComp spec α) (ob : OracleComp spec (List.Vector α n)) [spec.FiniteRange] [spec.DecidableEq] (xs : List.Vector α (n + 1)) : [=xs|(fun (x1 : α) (x2 : List.Vector α n) => x1 ::ᵥ x2) <$> oa <*> ob] = [=xs.head|oa] * [=xs.tail|ob]

@[simp]

theorem OracleComp.probOutput_seq_map_vector_cons_eq_mul' {ι : Type u} {spec : OracleSpec ι} {α : Type v} {n : ℕ} (oa : OracleComp spec α) (ob : OracleComp spec (List.Vector α n)) [spec.FiniteRange] [spec.DecidableEq] (xs : List.Vector α (n + 1)) : [=xs|(fun (xs : List.Vector α n) (x : α) => x ::ᵥ xs) <$> ob <*> oa] = [=xs.head|oa] * [=xs.tail|ob]

@[simp]

theorem OracleComp.probOutput_vector_toList {ι : Type u} {spec : OracleSpec ι} {α : Type v} [spec.FiniteRange] [spec.DecidableEq] {n : ℕ} (oa : OracleComp spec (List.Vector α n)) (xs : List α) : [=xs|List.Vector.toList <$> oa] = if h : xs.length = n then [=⟨xs, h⟩|oa] else 0