Relational parametricity for the gwp.list list combinators

report_noisy_max_generic.v (and the idiomatic report-noisy-max) builds its lists with the combinators of gen_prob_lang.gwp.list (imported there as gwp.list): list_init (OCaml-faithful — forward, 0-indexed: list_init len f = [f 0; …; f (len-1)]), list_map, and list_max_index. These combinators have polymorphic, syntactically-typeable counterparts (list_map_poly / list_init_poly / the typed list_max_index, all typed in typing/list_typed.v), so their relational congruences (refines_list_map, refines_list_init, refines_list_max_index) come *for free* from the fundamental theorem: each is fundamental_val on the typed value, with its lrel_forall/lrel_arr structure eliminated and its list argument / result bridged through interp_TList below (interp (TList τ) ≡ lrel_list). We still define the semantic list relation lrel_list explicitly (via lrel_rec — value encoding NONE = InjLV #(), SOME x = InjRV x, a::l = SOME(a,l)), since it is the element/output relation those free theorems are read against, at *arbitrary* element relations.

The least relation R such that:

• R nilv nilv' when both are InjLV #() (the NONEV nil encoding);
• R consv consv' when both are InjRV (a, rest) / InjRV (a', rest') with A a a' and R rest rest' (the SOMEV (a, rest) cons encoding).

Bridge between the syntactic list type TList and the semantic list relation lrel_list: the relational interpretation of TList τ is exactly lrel_list over the interpretation of τ. This is what lets the fundamental theorem's free theorems (stated over interp (TList _)) be read as congruences over lrel_list at *arbitrary* element relations. The τ.[ren (+1)] shift in TList cancels the μ-bound variable via interp_ren_up.

The relational congruence for list_map over arbitrary related expressions, derived "for free" from the fundamental theorem applied to the syntactically typed polymorphic combinator list_map_poly.

Relational congruence for list_init, derived "for free" from the fundamental theorem applied to the typed list_init_poly. The index relation is lrel_int, matching the TInt index of the OCaml-faithful forward list_init.

Relational congruence for list_max_index, derived "for free" from the fundamental theorem applied to the syntactically typed list_max_index (see list_max_index_typed). list_max_index is a *monomorphic* value typed at TList TInt → TInt, so its interpretation is directly the arrow interp (TList TInt) [] → interp TInt []; we only bridge the domain interp (TList TInt) [] ≡ lrel_list (interp TInt []) via interp_TList. The output relation is interp TInt [] = lrel_int (not lrel_nat): the argmax index is built with integer +, so the syntactic type is TList TInt → TInt. This is sound — the index is in fact always a nat — and nothing downstream depends on its nat-ness (the consumers only need ∃ k, v = #k ∧ v' = #k, which lrel_int provides).