RComp/RCompOk as instances of Param, and their composition

This module connects the Kleisli-level logical relations RComp/RCompOk (Integrations/ParamTripleTransfer.lean, Integrations/ParamRCompOk.lean) to the Param annotated-relation hierarchy (Hierarchy/ParamHierarchy.lean).

RComp is a Param at (map2a, map2a)

Given p : Param .map2a .map2a A A' and a WPMonad M ps, Param.rcomp p packages RComp p.R with forward/backward Map2aHas records whose maps are Functor.map of p's forward/backward maps. The content is each record's map_in_R field: a value relatedness ∀ a, p.R a (f a) (p.fwd.map_in_R, resp. p.bwd.map_in_R) lifts through WPMonad.wp_map and (wp c).mono to RComp p.R c (f <$> c) (resp. the backward RComp p.R (g <$> c') c').

(map2a, map2a) is the largest class this construction reaches, for both directions, and the ceiling is real:

• Map1Has (RComp p.R) is available from p.fwd : Map1Has p.R alone (no proof obligation), but carries no relational content — Map1Has requires nothing beyond a function.
• Map2bHas/Map3Has forward would additionally require RComp p.R c c' → f <$> c = c': that RComp-relatedness (a one-directional wp-refinement order, reflexive by RComp.refl but not an equivalence) determines c' as literally f <$> c. This needs wp to be injective on M's carrier (so that wp-refinement in both directions forces term equality) — a property WPMonad does not assume and no instance in WP/Monad.lean (Id, StateT, ExceptT, Except, Option, EStateM, …) needs. This module does not construct a formal counterexample instance; the obstruction is the missing law wp-injectivity, stated here as the boundary of what Map2aHas.map_in_R's one-directional argument reaches.

RCompOk is not generically a Param

RCompOk Rα : M A → N A' → Prop relates computations in two monads, one possibly failing (WP M ps), one total (WP N .pure). A Param m n (M A) (N A') instance needs a forward map M A → N A' (Map1Has, free) and, for any relational content (Map2aHas), a proof that RCompOk Rα c (map c) holds for every c : M A — including a c that never succeeds, where RCompOk's partial-correctness ⇓? on the M side imposes no constraint, so any map value there is fine, but including also a c for whose success value map must recover the p.fwd.map-related partner. Recovering a value from an arbitrary c : M A (to feed p.fwd.map) is exactly a monad morphism M ⟶ N compatible with wp (an "extraction"): Id, Option, Except ε, EStateM ε σ admit one concretely (Option.getD, Except.getD-style, run-and-default), but a fully abstract M with only [Monad M] [WPMonad M ps] does not — WPMonad gives no way to turn a computation into a value. So the only level Param reaches for generic M, N is the content-free Map1Has; Map2aHas (in either direction) needs the extraction morphism as extra data, which is a hypothesis outside RCompOk's own signature. Param.rcompOkTrivial below records the free map0 instance; no map2a instance is stated, since it would need that extra hypothesis and is out of the scope of RCompOk's two-monad signature.

Composition and identity

RComp.trans composes two RComps in the same monad along relation composition (∃ b, Rα a b ∧ Rβ b c), using only WP (no Monad/WPMonad needed — it is pure wp-entailment chaining through SPred.exists/SPred.and).

RCompOk.trans composes RCompOk Rα : M → N with RCompOk Rβ : N → P when both N and P are total (WP N .pure, WP P .pure): at a .pure shape the partial-correctness postcondition ⇓? and the total-correctness postcondition ⇓ coincide (ExceptConds .pure = PUnit has one element, so ExceptConds.false = ExceptConds.true by rfl), so the total-side result of the first step feeds directly as the total-side hypothesis of the second.

RCompOk.reflEq is the identity-at-Eq fact for RCompOk, available exactly when the "failing" side is itself total (WP M .pure) — the degenerate case where RCompOk and RComp coincide up to the same ⇓?/⇓ collapse.

RComp as a Param

def Transfer.Param.Param.rcomp {M : Type u → Type u} {ps : Std.Do.PostShape} [Monad M] [Std.Do.WPMonad M ps] {A A' : Type u} (p : Param MapClass.map2a MapClass.map2a A A') : Param MapClass.map2a MapClass.map2a (M A) (M A')

RComp is a Param at (map2a, map2a). Given an element relation at forward/backward map2a, the Kleisli lift RComp p.R is again forward/backward map2a, with maps Functor.map of p's forward/backward maps. This is the largest class the construction reaches (see the module docstring for why map2b/map3 is out of reach in general).

Equations

• p.rcomp = { R := Transfer.Param.RComp p.R, fwd := { map := fun (c : M A) => p.fwd.map <$> c, map_in_R := ⋯ }, bwd := { map := fun (c' : M A') => p.bwd.map <$> c', map_in_R := ⋯ } }

RCompOk: the free map0 instance

def Transfer.Param.Param.rcompOkTrivial {M : Type u → Type u} {ps : Std.Do.PostShape} [Std.Do.WP M ps] {N : Type u → Type u} [Std.Do.WP N Std.Do.PostShape.pure] {A A' : Type u} (Rα : A → A' → Prop) : Param MapClass.map0 MapClass.map0 (M A) (N A')

The content-free Param instance RCompOk always admits: Map0Has needs no data. No Map2aHas instance is stated (see the module docstring): it would need a wp-respecting extraction M A → A, data outside RCompOk's own two-monad signature.

Equations

• Transfer.Param.Param.rcompOkTrivial Rα = { R := Transfer.Param.RCompOk Rα, fwd := { }, bwd := { } }

Composition

theorem Transfer.Param.RComp.trans {M : Type u → Type v} {ps : Std.Do.PostShape} [Std.Do.WP M ps] {A B C : Type u} {Rα : A → B → Prop} {Rβ : B → C → Prop} {c : M A} {c' : M B} {c'' : M C} (h1 : RComp Rα c c') (h2 : RComp Rβ c' c'') : RComp (fun (a : A) (x : C) => ∃ (b : B), Rα a b ∧ Rβ b x) c c''

RComp composes along relation composition. Sequencing two RComp-witnesses in the same monad gives a witness for the composed value relation ∃ b, Rα a b ∧ Rβ b c. Needs only WP M ps — no Monad/WPMonad, since it chains wp-entailment through SPred.exists/SPred.and alone.

theorem Transfer.Param.RCompOk.trans {M : Type u → Type v} {ps : Std.Do.PostShape} {N : Type u → Type w} {P : Type u → Type x} [Std.Do.WP M ps] [Std.Do.WP N Std.Do.PostShape.pure] [Std.Do.WP P Std.Do.PostShape.pure] {A B C : Type u} {Rα : A → B → Prop} {Rβ : B → C → Prop} {c : M A} {c' : N B} {c'' : P C} (h1 : RCompOk Rα c c') (h2 : RCompOk Rβ c' c'') : RCompOk (fun (a : A) (x : C) => ∃ (b : B), Rα a b ∧ Rβ b x) c c''

RCompOk composes across two total codomains. RCompOk Rα : M → N and RCompOk Rβ : N → P compose to RCompOk (∃ b, Rα a b ∧ Rβ b c) : M → P whenever both N and P are total (WP N .pure, WP P .pure): at a .pure shape ⇓? and ⇓ coincide by rfl (ExceptConds .pure = PUnit), so the total-correctness conclusion about c' from the second witness feeds directly as the total-correctness hypothesis the first witness expects.

Identity

theorem Transfer.Param.RCompOk.reflEq {M : Type u → Type v} [Std.Do.WP M Std.Do.PostShape.pure] {A : Type u} (c : M A) : RCompOk Eq c c

RCompOk at Eq is reflexive when the M-side is itself total. The degenerate case N := M, ps := .pure, where RCompOk's partial- and total-correctness postconditions coincide (⇓? = ⇓ by rfl at .pure), so RCompOk reduces to the same wp-monotonicity argument as RComp.refl.

Axiom audit