search

coq-community / trocq

A modular parametricity plugin for proof transfer in Coq [maintainers=@CohenCyril,@ecranceMERCE,@amahboubi]
http://coq-community.org/trocq/
GNU Lesser General Public License v3.0
18 stars 3 forks source link

Combinator creating full parametricity witnesses from individual record fields #24

Open ecranceMERCE opened 9 months ago

ecranceMERCE commented 9 months ago

This repository contains a few files giving parametricity proofs for inductive types like nat, bool, option, but also equality and vectors for example. It looks like we first define the individual fields (i.e., map from nat to nat, then map_in_R, etc.), then a proof of equivalence between the relation and its symmetrisation:

R_sym : forall x x', sym_rel R x' x <~> R x x'

before actually building the full record at level $(m, n)$ by taking $m$ fields for R and $n$ fields for sym_rel R, then glueing both subrecords using R_sym so that the second one typechecks as the contravariant field of the Param record.

Can this symmetry proof be made automatically just from the definition of R, even when R is non-trivial and provided by the user? Can the whole process be automated so that the user just has to input the individual fields and Trocq generates all the possible records (possibly on the fly during the translation)?

CohenCyril commented 9 months ago

There are two ways to go about that:

  1. Modify and use HB (cf #28)
  2. Implement some of the features of HB in Trocq