The data-type (× / Option / List) parametricity rules

A Lean port of Trocq's container relational lift (https://github.com/rocq-community/trocq, generic/Param_prod.v, generic/Param_option.v, generic/Param_list.v): the combinators that build a Param annotated relation on a container type (A × B, Option A, List A) from Param relations on its element type(s).

These are the data-type rules of the parametricity translation, extending the engine's reach from the type formers → (ParamArrow.lean) and ∀ (ParamForall.lean) to the standard inductive containers.

What is ported

For each container F the Coq files define an inductive relation (prodR, optionR, listR) and the forward map builders (F_map, F_map_in_R, F_R_in_map) at the levels map1–map4. The relations are pointwise lifts of the element relation; the math is ported directly (the relation + the map builders), exactly as ParamArrow/ParamForall ported the arrow/forall math — not the Elpi that generates these container files in Coq. Trocq's Elpi produces one such file per inductive type mechanically; the present three are the representative shapes (binary product, nullary/unary sum, recursive list) all further inductive types follow.

Relations

• R_prod PA PB p p' := PA.R p.1 p'.1 ∧ PB.R p.2 p'.2 (Coq prodR).
• R_option PA : none ~ none, some a ~ some a' := PA.R a a', else False (Coq optionR).
• R_list PA := List.Forall₂ PA.R (Coq listR is exactly Mathlib's List.Forall₂, which is reused directly).

Levels achieved

The container forward map (Map1_*) lifts the element forward map through the constructor, and its graph-inclusion (Map2a_*) lifts the element map_in_R; both are univalence-free in Lean, as in Coq's std. The Param-level combinator is delivered at forward-map1, backward-map0 — param{Prod,Option,List} : Param .map1 .map0 (F A) (F A') — from element inputs Param .map2a .map0 (map2a is what the graph-inclusion consumes), mirroring paramForall. The full map2a/map3 forward records are provided as Map2a_* for prod/option/list. Higher levels (map3/map4 backward, and the R_in_mapK coherence at map4) are the residual, exactly as for the arrow and forall rules. Dependent containers (e.g. Σ, vectors indexed by length) follow the same pattern with an indexed family in place of the constant element Param, as in ParamForall.

Product: the relation R_prod (Coq prodR)

def Transfer.Param.R_prod {A A' B B' : Type u} {mA nA mB nB : MapClass} (PA : Param mA nA A A') (PB : Param mB nB B B') : A × B → A' × B' → Prop

Trocq prodR: two pairs are related when their components are related by PA and PB respectively. The (logically equivalent) conjunction form is used, the convenient shape for the crypto transfer. The level parameters stay polymorphic — the relation touches only the R fields.

Equations

• Transfer.Param.R_prod PA PB p p' = (PA.R p.fst p'.fst ∧ PB.R p.snd p'.snd)

def Transfer.Param.Map0_prod {A A' B B' : Type u} {mA nA mB nB : MapClass} (PA : Param mA nA A A') (PB : Param mB nB B B') : Map0Has (R_prod PA PB)

Trocq Map0_prod: no structure.

Equations

• Transfer.Param.Map0_prod PA PB = { }

def Transfer.Param.Map1_prod {A A' B B' : Type u} (PA : Param MapClass.map1 MapClass.map0 A A') (PB : Param MapClass.map1 MapClass.map0 B B') : Map1Has (R_prod PA PB)

Trocq prod_map as a map1 record: lift each component forward map through the pair constructor. Needs PA, PB forward-map1.

Equations

• Transfer.Param.Map1_prod PA PB = { map := fun (p : A × B) => (PA.fwd.map p.fst, PB.fwd.map p.snd) }

def Transfer.Param.Map2a_prod {A A' B B' : Type u} (PA : Param MapClass.map2a MapClass.map0 A A') (PB : Param MapClass.map2a MapClass.map0 B B') : Map2aHas (R_prod PA PB)

Trocq prod_map_in_R as a map2a record: the lifted map's graph is included in R_prod (componentwise via each PA.map_in_R/PB.map_in_R). Needs PA, PB forward-map2a.

Equations

• Transfer.Param.Map2a_prod PA PB = { map := fun (p : A × B) => (PA.fwd.map p.fst, PB.fwd.map p.snd), map_in_R := ⋯ }

def Transfer.Param.paramProd {A A' B B' : Type u} (PA : Param MapClass.map2a MapClass.map0 A A') (PB : Param MapClass.map2a MapClass.map0 B B') : Param MapClass.map1 MapClass.map0 (A × B) (A' × B')

paramProd: from element relations at forward-map2a, backward-map0, the annotated relation on the product, forward-map1, backward-map0. The forward map is the componentwise lift prod_map.

Equations

• Transfer.Param.paramProd PA PB = { R := Transfer.Param.R_prod PA PB, fwd := { map := fun (p : A × B) => (PA.fwd.map p.fst, PB.fwd.map p.snd) }, bwd := { } }

Option: the relation R_option (Coq optionR)

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

Trocq optionR: none ~ none; some a ~ some a' iff PA.R a a'; mixed constructors are unrelated.

Equations

• Transfer.Param.R_option PA none none = True
• Transfer.Param.R_option PA (some a) (some a') = PA.R a a'
• Transfer.Param.R_option PA x✝¹ x✝ = False

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

Trocq Map0_option: no structure.

Equations

• Transfer.Param.Map0_option PA = { }

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

Trocq option_map as a map1 record: lift the element forward map through Option.map. Needs PA forward-map1.

Equations

• Transfer.Param.Map1_option PA = { map := Option.map PA.fwd.map }

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

Trocq option_map_in_R as a map2a record: the lifted map's graph is included in R_option. Needs PA forward-map2a.

Equations

• Transfer.Param.Map2a_option PA = { map := Option.map PA.fwd.map, map_in_R := ⋯ }

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

paramOption: from an element relation at forward-map2a, backward-map0, the annotated relation on Option, forward-map1, backward-map0.

Equations

• Transfer.Param.paramOption PA = { R := Transfer.Param.R_option PA, fwd := { map := Option.map PA.fwd.map }, bwd := { } }

List: the relation R_list (Coq listR = Mathlib List.Forall₂)

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

Trocq listR: the pointwise lift of the element relation to lists — [] ~ [], and a :: as ~ a' :: as' iff PA.R a a' ∧ R_list as as'. This is exactly Mathlib's List.Forall₂ PA.R, which is reused (the nilR/consR constructors are List.Forall₂.nil/List.Forall₂.cons).

Equations

• Transfer.Param.R_list PA = List.Forall₂ PA.R

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

Trocq Map0_list: no structure.

Equations

• Transfer.Param.Map0_list PA = { }

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

Trocq map_list as a map1 record: lift the element forward map through List.map. Needs PA forward-map1.

Equations

• Transfer.Param.Map1_list PA = { map := List.map PA.fwd.map }

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

Trocq map_in_R_list as a map2a record: the lifted map's graph is included in R_list, by induction on the list (the recursive consR builder). Needs PA forward-map2a.

Equations

• Transfer.Param.Map2a_list PA = { map := List.map PA.fwd.map, map_in_R := ⋯ }

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

paramList: from an element relation at forward-map2a, backward-map0, the annotated relation on List, forward-map1, backward-map0. The forward map is List.map PA.map.

Equations

• Transfer.Param.paramList PA = { R := Transfer.Param.R_list PA, fwd := { map := List.map PA.fwd.map }, bwd := { } }

R_in_map (the relation-inclusion half), recovering the graph

The element-side R_in_map (forward-map2b) lifts to the container, giving the map2b and hence map3 forward records. The list version (the recursive case) is the representative; prod/option follow by the same componentwise/cases argument.

theorem Transfer.Param.R_in_map_list {A A' : Type u} (PA : Param MapClass.map2b MapClass.map0 A A') (l : List A) (l' : List A') (h : R_list PA l l') : List.map PA.fwd.map l = l'

Trocq R_in_map_list: R_list-relatedness implies the lifted map sends l to l', by induction on the List.Forall₂ derivation. Combined with Map2a_list.map_in_R this gives the full map3 graph (omitted as a record here; this is the funext-free relation-inclusion half). Needs the element R_in_map, i.e. PA forward-map2b.

Demos

Each container relation lifts the diagonal (equality) to the expected pointwise relation, the forward map computes through the constructor, and the data rules compose with the arrow rule of ParamArrow.lean.

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

The diagonal as an element input for the data rules: forward-map2a (a map plus the graph-inclusion map_in_R), backward-map0. This is the shape paramProd/paramOption/paramList consume.

Equations

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

Cross-rule composition: the data rules feed the arrow rule

paramProd/paramList produce a Param .map1 .map0 on the container, the same output shape the leaf rules produce; weakened to the Param .map1 .map1 input paramArrow consumes (here directly at the diagonal level), the function space List T → S gets a Param whose relation is R_arrow (paramList …) ….

def Transfer.Param.paramListEq1 (T : Type u) : Param MapClass.map1 MapClass.map1 (List T) (List T)

The list-container relation at the forward-map1, backward-map1 level, the input shape paramArrow consumes (diagonal element).

Equations

• Transfer.Param.paramListEq1 T = { R := Transfer.Param.R_list (Transfer.Param.paramEqElt T), fwd := { map := List.map id }, bwd := { map := List.map id } }

def Transfer.Param.paramEq1' (S : Type u) : Param MapClass.map1 MapClass.map1 S S

The diagonal at forward/backward-map1, for the codomain of the arrow.

Equations

• Transfer.Param.paramEq1' S = { R := Eq, fwd := { map := id }, bwd := { map := id } }