The set monad under the state and reader transformers

Membership in the computations of StateT σ Set and ReaderT σ Set, with Set.monad as the monad: a computation run at an input is a set of results, and pure, <$>, >>= and <*> act on it as singleton, image, indexed union and pointwise application. The statements are about the local instance Set.monad, so they apply wherever a file enables it.

Main results

• Set.mem_stateT_bind, Set.mem_stateT_map, Set.mem_stateT_pure, Set.mem_stateT_seq: results of StateT σ Set computations.
• Set.mk_mem_stateT_map, Set.mk_mem_stateT_map_seq: the same for a value–state pair, with f <$> m <*> n running m and then n from its output state.
• Set.mem_readerT_bind, Set.mem_readerT_map, Set.mem_readerT_pure: results of ReaderT σ Set computations.
• StateT.relEquiv: a StateT σ Set α computation is the family of relations on σ it induces at each value, and StateT.rel_bind, StateT.rel_map_seq compose these relations.
• StateT.rel_bind_subset, StateT.rel_map_seq_subset: a reflexive and transitive relation containing every step of the parts contains every step of the whole.

StateT σ Set

@[simp]

theorem Set.mem_stateT_bind {σ α β : Type u} (m : StateT σ Set α) (f : α → StateT σ Set β) (s : σ) (r : β × σ) : r ∈ (m >>= f) s ↔ ∃ q ∈ m s, r ∈ f q.1 q.2

@[simp]

theorem Set.mem_stateT_map {σ α β : Type u} (f : α → β) (m : StateT σ Set α) (s : σ) (r : β × σ) : r ∈ (f <$> m) s ↔ ∃ q ∈ m s, r = (f q.1, q.2)

@[simp]

theorem Set.mem_stateT_pure {σ α : Type u} (a : α) (s : σ) (r : α × σ) : r ∈ pure a s ↔ r = (a, s)

@[simp]

theorem Set.mem_stateT_seq {σ α β : Type u} (m : StateT σ Set (α → β)) (n : StateT σ Set α) (s : σ) (r : β × σ) : r ∈ (m <*> n) s ↔ ∃ q ∈ m s, ∃ q' ∈ n q.2, r = (q.1 q'.1, q'.2)

theorem Set.mk_mem_stateT_map {σ α β : Type u} {f : α → β} {m : StateT σ Set α} {s s' : σ} {b : β} : (b, s') ∈ (f <$> m) s ↔ ∃ (a : α), (a, s') ∈ m s ∧ b = f a

theorem Set.mk_mem_stateT_map_seq {σ α β γ : Type u} {f : α → β → γ} {m : StateT σ Set α} {n : StateT σ Set β} {s s'' : σ} {c : γ} : (c, s'') ∈ (f <$> m <*> n) s ↔ ∃ (a : α) (s' : σ), (a, s') ∈ m s ∧ ∃ (b : β), (b, s'') ∈ n s' ∧ c = f a b

ReaderT σ Set

@[simp]

theorem Set.mem_readerT_bind {σ α β : Type u} (m : ReaderT σ Set α) (f : α → ReaderT σ Set β) (s : σ) (r : β) : r ∈ (m >>= f) s ↔ ∃ x ∈ m s, r ∈ f x s

@[simp]

theorem Set.mem_readerT_map {σ α β : Type u} (f : α → β) (m : ReaderT σ Set α) (s : σ) (r : β) : r ∈ (f <$> m) s ↔ ∃ x ∈ m s, r = f x

@[simp]

theorem Set.mem_readerT_pure {σ α : Type u} (a : α) (s : σ) (r : α) : r ∈ pure a s ↔ r = a

Graded relations

def StateT.rel {σ α : Type u} (m : StateT σ Set α) (a : α) : SetRel σ σ

The relation m induces at the value a, from each state to the states m reaches from it with the value a.

Equations

• m.rel a = {p : σ × σ | (a, p.2) ∈ m p.1}

@[simp]

theorem StateT.mem_rel {σ α : Type u} {m : StateT σ Set α} {a : α} {s s' : σ} : (s, s') ∈ m.rel a ↔ (a, s') ∈ m s

def StateT.relEquiv {σ α : Type u} : StateT σ Set α ≃ (α → SetRel σ σ)

A StateT σ Set α computation is the family of relations it induces at its values.

Equations

• StateT.relEquiv = { toFun := StateT.rel, invFun := fun (R : α → SetRel σ σ) (s : σ) => {q : α × σ | (s, q.2) ∈ R q.1}, left_inv := ⋯, right_inv := ⋯ }

theorem StateT.rel_pure_self {σ α : Type u} (a : α) : (pure a).rel a = SetRel.id

theorem StateT.rel_pure_of_ne {σ α : Type u} {a b : α} (h : a ≠ b) : (pure a).rel b = ∅

theorem StateT.rel_bind {σ α β : Type u} (m : StateT σ Set α) (f : α → StateT σ Set β) (b : β) : (m >>= f).rel b = ⋃ (a : α), (m.rel a).comp ((f a).rel b)

theorem StateT.rel_map {σ α β : Type u} (f : α → β) (m : StateT σ Set α) (b : β) : (f <$> m).rel b = ⋃ (a : α), ⋃ (_ : f a = b), m.rel a

theorem StateT.rel_map_seq {σ α β γ : Type u} (f : α → β → γ) (m : StateT σ Set α) (n : StateT σ Set β) (c : γ) : (f <$> m <*> n).rel c = ⋃ (a : α), ⋃ (b : β), ⋃ (_ : f a b = c), (m.rel a).comp (n.rel b)

theorem StateT.rel_pure_subset {σ α : Type u} {R : SetRel σ σ} [R.IsRefl] (a b : α) : (pure a).rel b ⊆ R

theorem StateT.rel_bind_subset {σ α β : Type u} {R : SetRel σ σ} [R.IsTrans] {m : StateT σ Set α} {f : α → StateT σ Set β} (hm : ∀ (a : α), m.rel a ⊆ R) (hf : ∀ (a : α) (b : β), (f a).rel b ⊆ R) (b : β) : (m >>= f).rel b ⊆ R

theorem StateT.rel_map_subset {σ α β : Type u} {R : SetRel σ σ} {m : StateT σ Set α} (hm : ∀ (a : α), m.rel a ⊆ R) (f : α → β) (b : β) : (f <$> m).rel b ⊆ R

theorem StateT.rel_map_seq_subset {σ α β γ : Type u} {R : SetRel σ σ} [R.IsTrans] {m : StateT σ Set α} {n : StateT σ Set β} (hm : ∀ (a : α), m.rel a ⊆ R) (hn : ∀ (b : β), n.rel b ⊆ R) (f : α → β → γ) (c : γ) : (f <$> m <*> n).rel c ⊆ R