Documentation

VCVio.OracleComp.DistSemantics.List

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.

source
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
source
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
source
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
source
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
source
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
source
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
source
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]
source
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]
source
@[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]
source
@[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
source
@[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
source
@[simp]
theorem OracleComp.probFailure_list_mapM {ι : Type u} {spec : OracleSpec ι} {α : Type u_1} {β : Type u_2} [spec.FiniteRange] (xs : List α) (f : α → OracleComp spec β) :
[⊥|List.mapM f xs] = 1 - (List.map (fun (x : α) => 1 - [⊥|f x]) xs).prod
source
@[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
source
@[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|List.mapM f xs] = if ys.length = xs.length then (List.zipWith (fun (x : α) (y : β) => [=y|f x]) xs ys).prod else 0
source
@[simp]
theorem OracleComp.neverFails_list_mapM {ι : Type u} {spec : OracleSpec ι} {α β : Type v} {f : α → OracleComp spec β} {as : List α} (h : ∀ x ∈ as, (f x).neverFails) :
(List.mapM f as).neverFails

If each element of a list is mapped to a computation that never fails, then the computation obtained by monadic mapping over the list also never fails.

source
@[simp]
theorem OracleComp.neverFails_list_mapM' {ι : Type u} {spec : OracleSpec ι} {α β : Type v} {f : α → OracleComp spec β} {as : List α} (h : ∀ x ∈ as, (f x).neverFails) :
(List.mapM' f as).neverFails
source
@[simp]
theorem OracleComp.neverFails_list_flatMapM {ι : Type u} {spec : OracleSpec ι} {α β : Type v} {f : α → OracleComp spec (List β)} {as : List α} (h : ∀ x ∈ as, (f x).neverFails) :
(List.flatMapM f as).neverFails
source
@[simp]
theorem OracleComp.neverFails_list_filterMapM {ι : Type u} {spec : OracleSpec ι} {α β : Type v} {f : α → OracleComp spec (Option β)} {as : List α} (h : ∀ x ∈ as, (f x).neverFails) :
(List.filterMapM f as).neverFails
source
@[simp]
theorem OracleComp.neverFails_list_foldlM {ι : Type u} {spec : OracleSpec ι} {α s : Type v} {f : s → α → OracleComp spec s} {init : s} {as : List α} (h : ∀ (i : s), ∀ x ∈ as, (f i x).neverFails) :
(List.foldlM f init as).neverFails
source
@[simp]
theorem OracleComp.neverFails_list_foldrM {ι : Type u} {spec : OracleSpec ι} {α s : Type v} {f : α → s → OracleComp spec s} {init : s} {as : List α} (h : ∀ (i : s), ∀ x ∈ as, (f x i).neverFails) :
(List.foldrM f init as).neverFails
source
@[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}
source
@[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]
source
@[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]
source
@[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
source
@[simp]
theorem OracleComp.neverFails_list_vector_mmap {ι : Type u} {spec : OracleSpec ι} {α β : Type v} {n : ℕ} {f : α → OracleComp spec β} {as : List.Vector α n} (h : ∀ x ∈ as.toList, (f x).neverFails) :
(List.Vector.mmap f as).neverFails
source
@[simp]
theorem OracleComp.neverFails_array_mapM {ι : Type u} {spec : OracleSpec ι} {α β : Type v} {f : α → OracleComp spec β} {as : Array α} (h : ∀ x ∈ as, (f x).neverFails) :
(Array.mapM f as).neverFails
source
theorem OracleComp.mem_support_vector_mapM {ι : Type u} {spec : OracleSpec ι} {α β : Type v} {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
source
@[simp]
theorem OracleComp.neverFails_vector_mapM {ι : Type u} {spec : OracleSpec ι} {α β : Type v} {n : ℕ} {f : α → OracleComp spec β} {as : Vector α n} (h : ∀ x ∈ as.toList, (f x).neverFails) :
(Vector.mapM f as).neverFails