forIn / do-loop transfer: foldlR meets RComp

ParamArray.foldlR transfers a pure fold across related containers. Real hex loops (HexBareiss, HexLLL) are do/for loops — effectful, with early exit. Lean desugars for x in xs do … to forIn, so this module lifts the fold transfer to forIn, combining ParamArray's container relation with Integrations/ParamTripleTransfer's Kleisli relation RComp.

The result RComp.forIn_list is exactly foldlR extended along two axes:

• effects — the body runs in an arbitrary WPMonad, so the transfer is at the wp-refinement level (RComp), not plain equality;
• early exit — the body returns a ForInStep, and RForInStep relates yield/done constructor-wise (a done on one side must meet a done on the other), so the loop transfers even when it breaks early.

A pure, yield-only forIn is a foldl, so foldlR is the special case of this lemma at M = Id with no done. Together with ParamArray.foldlR (structural folds) and RComp.pure/RComp.bind (straight-line effects), this closes the combinator set a fold-or-loop-shaped hex algorithm needs to transfer without any recursor translation.

The relation on ForInStep

def Transfer.Param.RForInStep {β β' : Type u} (Rβ : β → β' → Prop) : ForInStep β → ForInStep β' → Prop

The constructor-wise lift of a value relation to ForInStep: yield/done are related only to the same constructor, carrying the value relation (the ForInStep analogue of R_option). A done on one side cannot be related to a yield on the other, so an early exit must be matched.

Equations

• Transfer.Param.RForInStep Rβ (ForInStep.yield b) (ForInStep.yield b') = Rβ b b'
• Transfer.Param.RForInStep Rβ (ForInStep.done b) (ForInStep.done b') = Rβ b b'
• Transfer.Param.RForInStep Rβ x✝¹ x✝ = False

forIn transfer over a List

theorem Transfer.Param.RComp.forIn_list {M : Type u → Type v} {ps : Std.Do.PostShape} [Monad M] [Std.Do.WPMonad M ps] {A A' β β' : Type u} (RA : A → A' → Prop) (Rβ : β → β' → Prop) (body : A → β → M (ForInStep β)) (body' : A' → β' → M (ForInStep β')) (hbody : ∀ (a : A) (a' : A') (b : β) (b' : β'), RA a a' → Rβ b b' → RComp (RForInStep Rβ) (body a b) (body' a' b')) {l : List A} {l' : List A'} (hl : List.Forall₂ RA l l') {init : β} {init' : β'} (hinit : Rβ init init') : RComp Rβ (forIn l init body) (forIn l' init' body')

forIn transfer. For a loop body that maps related elements and related accumulators to RForInStep-related steps (in the wp-refinement sense), folding it with forIn over List.Forall₂-related lists from related initial accumulators yields RComp-related computations. Proved by induction on the Forall₂ derivation, RComp.bind-ing the body step against the continuation, which the RForInStep relation splits into the yield (recurse) and done (pure) cases.

Demo: a do-loop transfers in Id

A for-loop summation over related lists, transferred by the engine. The body is yield-only, so this is the effectful/early-exit generalisation of foldlR specialised back to a pure accumulation.

Axiom audit