rcomp: structural assembly of an RComp witness

Integrations/ParamTripleTransfer.lean builds an RComp witness — the Kleisli logical relation observed through wp — by hand, one RComp.pure / RComp.bind leaf per pure / bind in the do-block. This module automates that assembly: rcomp is the monad-level analogue of the pure transfer / rcongr descent, a goal-shape-directed tactic that walks the two programs' structure and applies the matching RComp rule, leaving each value-relatedness as a residual goal.

What rcomp does

On a goal RComp Rα c c' it tries, in order:

• RComp.refl — the diagonal (c and c' definitionally equal, Rα reflexive);
• RComp.pure — a pure/pure (or pure-reducible) pair, leaving one leaf Rα a a';
• RComp.bind — a bind/bind pair, pinning the intermediate relation to the goal's Rα and recursing on the head and (under the introduced value binders) the continuation;
• RComp.forIn_list — a for/do loop.

The value leaves (Rα a a', the arithmetic content) are left for the caller — the same non-fabrication discipline transfer follows. A pure computation over Id collapses to a single leaf (pure reduces definitionally), discharged with norm_cast / simp_all; an effectful monad descends its bind structure leaf by leaf.

Folded into param_transfer

param_transfer gains an RComp alternative: on a ∀-transfer goal it runs the abstraction-theorem ∀-rule (ParamTransferTac), and on an RComp goal it assembles the witness with rcomp. One entry point, both the pure and the effectful abstraction theorem.

Only the structurally parallel fragment is automatic — the two programs must share a pure / bind / forIn skeleton and a uniform value relation, which is the shape every hand-assembled witness has. A structural mismatch stays a residual RComp goal rather than being forced.

partial def Transfer.Param.rcompCore : Lean.Elab.Tactic.TacticM Unit

Goal-shape-directed RComp descent. On RComp Rα c c' it applies the first matching rule — RComp.refl (diagonal), RComp.pure (a pure leaf, or a pure-reducible Id computation collapsed to one leaf), RComp.bind (a bind node, intermediate relation pinned to Rα), or RComp.forIn_list (a loop) — and recurses into the resulting RComp / continuation subgoals, introducing the continuation's value binders with fresh names. Value-relatedness leaves are left as residual goals.

def Transfer.Param.tacticRcomp : Lean.ParserDescr

Assemble an RComp witness by structural descent (see rcompCore). Fails on a goal that is not RComp _ _ _, so it composes safely as a param_transfer alternative. The value-relatedness leaves remain — discharge them with the relation's arithmetic (norm_cast / simp_all / push_cast; ring).

Equations

• Transfer.Param.tacticRcomp = Lean.ParserDescr.node `Transfer.Param.tacticRcomp 1024 (Lean.ParserDescr.nonReservedSymbol "rcomp" false)

Demonstrations

Each witness below is assembled by the tactic; the caller writes only the value leaf. Compare Examples/HexEffectful.lean / Examples/EffectfulTransfer.lean, where the same witnesses are spelled out by hand.

Axiom audit