Query Implementations with Reader Monads

This file gives lemmas about QueryImpl spec m when m is something like ReaderT ρ n.

TODO: should generalize things to MonadReader once laws for it exist.

def QueryImpl.addReaderT {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {m : Type (max u_3 u_4) → Type u_5} {ρ₁ ρ₂ : Type (max u_3 u_4)} (impl₁ : QueryImpl spec₁ (ReaderT ρ₁ m)) (impl₂ : QueryImpl spec₂ (ReaderT ρ₂ m)) : QueryImpl (spec₁ + spec₂) (ReaderT (ρ₁ × ρ₂) m)

Given implementations for oracles in spec₁ and spec₂ in terms of reader monads for two different contexts ρ₁ and ρ₂, implement the combined set spec₁ + spec₂ in terms of a combined ρ₁ × ρ₂ state. The binary analogue of QueryImpl.sigmaReaderT.

def QueryImpl.sigmaReaderT {τ : Type} {ι : τ → Type u_1} {spec : (t : τ) → OracleSpec (ι t)} {m : Type u_2 → Type u_3} {ρ : τ → Type u_2} (impl : (t : τ) → QueryImpl (spec t) (ReaderT (ρ t) m)) : QueryImpl (OracleSpec.sigma spec) (ReaderT ((t : τ) → ρ t) m)

Indexed version of QueryImpl.addReaderT. Each query for index t reads from the t-th component of the pi-product (t : τ) → ρ t. Note that m cannot vary with t.

def QueryImpl.flattenReaderT {ι : Type u_1} {spec : OracleSpec ι} {m : Type (max u_2 u_3) → Type u_4} {ρ₁ ρ₂ : Type (max u_2 u_3)} (impl : QueryImpl spec (ReaderT ρ₁ (ReaderT ρ₂ m))) : QueryImpl spec (ReaderT (ρ₁ × ρ₂) m)

Reassociate a nested reader transformer into one product context.

The outer context is the first component of the product; the inner/base context is the second. This is the reader-transformer analogue of flattenStateT and flattenWriterT.