The Array container rule and relational foldl transfer

ParamData.lean lifts Param through ×/Option/List. This module adds the Array container — the carrier leanprover/hex's computational cores use for O(1) dense access — and the relational foldl transfer that makes Array- (or List-) carried folds transfer generically.

Why this is the recursion story

ParamTransfer's term-level ⟦·⟧ stops at recursors, so a recursive algorithm is not translated inline. CoqEAL's answer — and this module's — is that recursion is factored through a small set of combinators, each transferred once. foldlR is that lemma for the fold combinator: given a step that respects the element and accumulator relations, a fold over related containers yields related results, at heterogeneous element and accumulator types (the general parametricity of foldl, not the encoding-only HigherOrderTransfer.foldl_transfer). Every structural/bounded algorithm expressed as a fold — HexBareiss, HexRowReduce, HexGramSchmidt, HexDeterminant — inherits transfer from this one lemma, without touching the recursor frontier. forIn/do-loops desugar to a fold and ride it too; the monadic case is Integrations/ParamTripleTransfer's RComp.

What is ported

• R_array PA — the pointwise lift to arrays, List.Forall₂ PA.R on toList (reusing the R_list machinery), with the map0/map1/map2a forward records and paramArray : Param .map1 .map0 (Array A) (Array A'), mirroring paramList.
• foldlR_list / foldlR_array — the relational fold transfer. The Array version reduces to the List version through Array.foldl_toList.

The Array relation R_array (via R_list on toList)

def Transfer.Param.R_array {A A' : Type u} {mA nA : MapClass} (PA : Param mA nA A A') : Array A → Array A' → Prop

R_array: two arrays are related when their underlying lists are pointwise related by the element relation. Reuses List.Forall₂, exactly as R_list does — the Array rule is the List rule read through Array.toList.

Equations

• Transfer.Param.R_array PA a a' = List.Forall₂ PA.R a.toList a'.toList

def Transfer.Param.Map0_array {A A' : Type u} {mA nA : MapClass} (PA : Param mA nA A A') : Map0Has (R_array PA)

Map0_array: no structure.

Equations

• Transfer.Param.Map0_array PA = { }

def Transfer.Param.Map1_array {A A' : Type u} (PA : Param MapClass.map1 MapClass.map0 A A') : Map1Has (R_array PA)

Map1_array: lift the element forward map through Array.map.

Equations

• Transfer.Param.Map1_array PA = { map := Array.map PA.fwd.map }

def Transfer.Param.Map2a_array {A A' : Type u} (PA : Param MapClass.map2a MapClass.map0 A A') : Map2aHas (R_array PA)

Map2a_array: the lifted map's graph is included in R_array, reducing to the List graph-inclusion (Map2a_list) through Array.toList_map.

Equations

• Transfer.Param.Map2a_array PA = { map := Array.map PA.fwd.map, map_in_R := ⋯ }

def Transfer.Param.paramArray {A A' : Type u} (PA : Param MapClass.map2a MapClass.map0 A A') : Param MapClass.map1 MapClass.map0 (Array A) (Array A')

paramArray: from an element relation at forward-map2a, backward-map0, the annotated relation on Array, forward-map1, backward-map0. The Array analogue of paramList.

Equations

• Transfer.Param.paramArray PA = { R := Transfer.Param.R_array PA, fwd := { map := Array.map PA.fwd.map }, bwd := { } }

Relational foldl transfer — the combinator lemma

The parametricity of foldl at heterogeneous element (A/A') and accumulator (β/β') types: a step respecting both relations sends related seeds and related containers to related results. This is the atom every fold-shaped algorithm transfers through.

theorem Transfer.Param.foldlR_list {A A' : Type u} {β β' : Type v} (PA : A → A' → Prop) (Rβ : β → β' → Prop) (f : β → A → β) (f' : β' → A' → β') (hf : ∀ (s : β) (s' : β') (x : A) (x' : A'), Rβ s s' → PA x x' → Rβ (f s x) (f' s' x')) {s : β} {s' : β'} (hs : Rβ s s') {l : List A} {l' : List A'} (hl : List.Forall₂ PA l l') : Rβ (List.foldl f s l) (List.foldl f' s' l')

Relational List.foldl transfer. If the step f/f' maps Rβ-related accumulators and PA-related elements to Rβ-related accumulators, then folding over List.Forall₂ PA-related lists from Rβ-related seeds yields Rβ-related results. The general parametricity of foldl (heterogeneous carriers), by induction on the Forall₂ derivation with the accumulators generalized.

theorem Transfer.Param.foldlR_array {A A' : Type u} {β β' : Type v} {mA nA : MapClass} (PA : Param mA nA A A') (Rβ : β → β' → Prop) (f : β → A → β) (f' : β' → A' → β') (hf : ∀ (s : β) (s' : β') (x : A) (x' : A'), Rβ s s' → PA.R x x' → Rβ (f s x) (f' s' x')) {s : β} {s' : β'} (hs : Rβ s s') {a : Array A} {a' : Array A'} (ha : R_array PA a a') : Rβ (Array.foldl f s a) (Array.foldl f' s' a')

Relational Array.foldl transfer. The Array combinator lemma, reduced to foldlR_list through Array.foldl_toList. A fold over R_array-related arrays from related seeds yields related results — so any Array-carried fold of a step that respects the refinement transfers, no recursion translation needed.

Demos

def Transfer.Param.paramEqEltArray (T : Type u) : Param MapClass.map2a MapClass.map0 T T

The diagonal element input for the Array rule (forward-map2a, backward-map0), the shape paramArray consumes.

Equations

• Transfer.Param.paramEqEltArray T = { R := Eq, fwd := { map := id, map_in_R := ⋯ }, bwd := { } }

Axiom audit