Transferring a Hoare/wp triple through a Param relation

This module lifts the abstraction-theorem ∀-rule (ParamTransfer.forallTransfer) from propositions to monadic computations: it builds a triple-transfer principle. Given a value-level Param-style relation between two computations and a Hoare triple for the source, it derives the triple for the transferred computation, using only the wp_pure/wp_bind algebra of Std.Do.WPMonad.

The Kleisli-level logical relation RComp

ParamForall/ParamTransfer give the abstraction theorem at R_arrow/R_forall — the pure function level. Talking about effectful programs requires the same logical relation lifted to the Kleisli category of a monad M. RComp Rα c c' is exactly that lift, phrased as wp-refinement modulo the value relation:

RComp Rα c c' := ∀ Q Q' E, (∀ a a', Rα a a' → Q a ⊢ₛ Q' a') → wp⟦c⟧ (Q, E) ⊢ₛ wp⟦c'⟧ (Q', E)

i.e. any success-postcondition pair related pointwise by Rα (sharing the failure barrel E) is refined from c to c' at the level of weakest preconditions. This is the canonical Reynolds/Kleisli lift: the relation on computations induced by the relation on values, read through the wp observation.

The two pure/bind rules below are the compositional core — the content of the abstraction theorem at the monad level:

• RComp.pure — Rα a a' gives RComp Rα (pure a) (pure a') (via wp_pure);
• RComp.bind — RComp Rα c c' and a pointwise RComp Rβ (f a) (f' a') give RComp Rβ (c >>= f) (c' >>= f') (via wp_bind).

RComp.refl records the diagonal instance (Rα = Eq, c = c'): every computation is wp-refinement-related to itself, the paramDiag analogue.

The triple-transfer lemma

triple_transfer follows: since Triple x P Q is defined as P ⊢ₛ wp⟦x⟧ Q, an RComp-witness composes on the left with the source triple to yield the transferred triple. The pure/bind closure means an RComp-witness for a whole do-block can be assembled structurally from witnesses for its leaves — exactly the abstraction-theorem discipline ParamTransfer runs for ∀-statements, here for stateful/partial SPComp programs.

Worked examples

Two self-contained examples exercise the principle end-to-end over Id:

• Examples/HexEffectful.lean — a Bareiss-style elimination step: the source triple is proved by mvcgen, then triple_transfer moves it across a storage change (dense list ↦ Mathlib vector) at the same value type;
• Examples/EffectfulTransfer.lean — a do-block whose value type changes (ℕ ↦ ℤ along the cast relation), again mvcgen for the source and triple_transfer for the target.

RComp.forIn_list (Integrations/ParamForIn.lean) extends both to for / do loops with early exit.

Scope

Proved (univalence-free, Prop-predicate triples only):

• the Kleisli logical-relation lift RComp and its pure/bind/refl closure — the compositional core of the abstraction theorem at the monad level;
• triple_transfer, transferring Triple c P (Q, E) to Triple c' P (Q', E) along any RComp-witness;
• two worked Id examples (HexEffectful, EffectfulTransfer), each with an mvcgen-proved source triple transferred across a change of representation.

The rcomp tactic (Integrations/ParamRComp.lean) assembles the RComp witness by structural descent for the common case — two structurally parallel programs (shared pure / bind / forIn skeleton, one uniform value relation) — and is folded into param_transfer, so the hand RComp.pure / RComp.bind spelling below is the explicit form of what the tactic does.

Not implemented here:

• synthesis for a non-structurally-parallel do-block (a skeleton mismatch stays a residual RComp goal rather than being forced);
• full mvcgen integration (generating RComp-witnesses from @[spec] lemmas);
• the quantitative / advantage route is explicitly out of scope: expectation transformers are monotone but not conjunctive, so they do not inhabit PredTrans.conjunctiveRaw (see StdDoBridge); quantitative transfer belongs to the Advantage/sdist layer, not to this Prop-predicate wp principle.

The Kleisli-level logical relation RComp

The relation on computations induced by a value relation Rα, read through the wp observation: a wp-refinement that holds for every Rα-related postcondition pair (sharing the failure barrel). This is the monad-level analogue of R_arrow/R_forall from ParamForall/ParamTransfer.

def Transfer.Param.RComp {M : Type u → Type v} {ps : Std.Do.PostShape} [Std.Do.WP M ps] {α α' : Type u} (Rα : α → α' → Prop) (c : M α) (c' : M α') : Prop

The Kleisli lift of a value relation. RComp Rα c c' holds when, for every pair of success-postconditions related pointwise by Rα (sharing one failure barrel E), the weakest precondition of c entails that of c'. This is the canonical logical-relation lift of Rα to M-computations, observed via wp.

Equations

• One or more equations did not get rendered due to their size.

theorem Transfer.Param.RComp.pure {M : Type u → Type v} {ps : Std.Do.PostShape} [Monad M] [Std.Do.WPMonad M ps] {α α' : Type u} (Rα : α → α' → Prop) {a : α} {a' : α'} (h : Rα a a') : RComp Rα (Pure.pure a) (Pure.pure a')

pure rule of the abstraction theorem at the monad level. A value relatedness Rα a a' lifts to computation relatedness of the point distributions pure a, pure a'. Proved through WPMonad.wp_pure.

theorem Transfer.Param.RComp.bind {M : Type u → Type v} {ps : Std.Do.PostShape} [Monad M] [Std.Do.WPMonad M ps] {α α' β β' : Type u} {Rα : α → α' → Prop} {Rβ : β → β' → Prop} {c : M α} {c' : M α'} {f : α → M β} {f' : α' → M β'} (hc : RComp Rα c c') (hf : ∀ (a : α) (a' : α'), Rα a a' → RComp Rβ (f a) (f' a')) : RComp Rβ (c >>= f) (c' >>= f')

bind rule of the abstraction theorem at the monad level. Sequencing two related computations with two pointwise-related continuations yields related computations. Proved through WPMonad.wp_bind: the bound wp factors as wp⟦c⟧ (fun a => wp⟦f a⟧ ·), so the head refinement RComp Rα c c' applies with the per-result continuation refinements as its postcondition relatedness.

theorem Transfer.Param.RComp.refl {M : Type u → Type v} {ps : Std.Do.PostShape} [Std.Do.WP M ps] {α : Type u} (c : M α) : RComp (fun (a a' : α) => a = a') c c

The diagonal instance (paramDiag analogue): every computation is wp-refinement-related to itself under the equality value relation. The monad-level counterpart of ParamTransfer.paramDiag.

The triple-transfer principle

Triple x P Q is defined as P ⊢ₛ wp⟦x⟧ Q (Std.Do.Triple), so an RComp-witness — a wp-refinement — composes on the left of a source triple to give the transferred triple.

theorem Transfer.Param.triple_transfer {M : Type u → Type v} {ps : Std.Do.PostShape} [Std.Do.WP M ps] {α α' : Type u} {Rα : α → α' → Prop} {c : M α} {c' : M α'} (hcc : RComp Rα c c') {P : Std.Do.Assertion ps} {Q : α → Std.Do.Assertion ps} {Q' : α' → Std.Do.Assertion ps} {E : Std.Do.ExceptConds ps} (hQ : ∀ (a : α) (a' : α'), Rα a a' → Q a ⊢ₛ Q' a') (ht : ⦃P⦄ c ⦃(Q, E)⦄) : ⦃P⦄ c' ⦃(Q', E)⦄

Triple transfer along an RComp-witness. Given relatedness RComp Rα c c', a postcondition relatedness ∀ a a', Rα a a' → Q a ⊢ₛ Q' a', and a source triple ⦃P⦄ c ⦃Q, E⦄, derive the transferred triple ⦃P⦄ c' ⦃Q', E⦄ (same precondition, same failure barrel). This is the monad-level abstraction theorem: the conclusion is read off Triple = (· ⊢ₛ wp⟦·⟧ ·) by transitivity through the refinement.

A worked pure ≫= pure assembly

A two-leaf do-block witness assembled from RComp.pure and RComp.bind, showing the compositional core composes (the param-tactic would synthesize this automatically).

theorem Transfer.Param.RComp.pure_bind_pure {M : Type u → Type v} {ps : Std.Do.PostShape} [Monad M] [Std.Do.WPMonad M ps] {α α' β β' : Type u} {Rα : α → α' → Prop} {Rβ : β → β' → Prop} {a : α} {a' : α'} {g : α → β} {g' : α' → β'} (ha : Rα a a') (hg : ∀ (x : α) (x' : α'), Rα x x' → Rβ (g x) (g' x')) : RComp Rβ (do let x ← Pure.pure a Pure.pure (g x)) do let x ← Pure.pure a' Pure.pure (g' x)

RComp for do let x ← pure a; pure (g x) vs its primed twin, assembled structurally from the pure/bind rules. The continuation relatedness Rβ (g a) (g' a') is supplied pointwise.