meta.yml

---
fullname: Paramcoq
shortname: paramcoq
organization: coq-community
community: true
action: true
plugin: true
doi: 10.4230/LIPIcs.CSL.2012.381
branch: 'master'

synopsis: Plugin for generating parametricity statements to perform refinement proofs

description: |-
  A Coq plugin providing commands for generating parametricity statements.
  Typical applications of such statements are in data refinement proofs.
  Note that the plugin is still in an experimental state - it is not very user
  friendly (lack of good error messages) and still contains bugs. But it
  is usable enough to "translate" a large chunk of the standard library.

publications:
- pub_title: Parametricity in an Impredicative Sort
  pub_url: https://hal.archives-ouvertes.fr/hal-00730913/
  pub_doi: 10.4230/LIPIcs.CSL.2012.381

authors:
- name: Chantal Keller
  initial: true
- name: Marc Lasson
  initial: true
- name: Abhishek Anand
- name: Pierre Roux
- name: Emilio Jesús Gallego Arias
- name: Cyril Cohen
- name: Matthieu Sozeau

maintainers:
- name: Pierre Roux
  nickname: proux01

license:
  fullname: MIT License
  identifier: MIT

supported_coq_versions:
  text: >-
    The master branch tracks the development version of Coq, see
    releases for compatibility with released versions of Coq
  opam: '{= "dev" }'

categories:
- name: 'Miscellaneous/Coq Extensions'

keywords:
- name: paramcoq
- name: parametricity
- name: OCaml modules

namespace: Param

opam-file-maintainer: 'Pierre Roux <pierre.roux@onera.fr>'

opam-file-version: 'dev'

tested_coq_opam_versions:
- version: 'dev'

documentation: |-
  ## Usage and Commands

  To load the plugin and make its commands available:
  ```coq
  From Param Require Import Param.
  ```

  The command scheme for named translations is:
  ```
  Parametricity <ident> as <name> [arity <n>].
  ```
  For example, the following command generates a translation named `my_param`
  of the constant or inductive `my_id` with arity 2 (the default):
  ```coq
  Parametricity my_id as my_param.
  ```

  The command scheme for automatically named translations is:
  ```coq
  Parametricity [Recursive] <ident> [arity <n>] [qualified].
  ```
  Such commands generate and name translations based on the given identifier.
  The `Recursive` option can be used to recursively translate all the constants
  and inductives which are used by the constant or inductive with the given
  identifier. The `qualified` option allows you to use a qualified default name
  for the translated constants and inductives. The default name then has the form
  `Module_o_Submodule_o_my_id` if the identifier `my_id` is declared in the
  `Module.Submodule` namespace.

  Instead of using identifiers, you can provide explicit terms to translate,
  according to the following command scheme:
  ```coq
  Parametricity Translation <term> [as <name>] [arity <n>].
  ```
  This defines a new constant containing the parametricity translation of
  the given term.

  To recursively translate everything in a module:
  ```coq
  Parametricity Module <module_path>.
  ```

  When translating terms containing section variables or axioms,
  it may be useful to declare a term to be the translation of a constant:
  ```coq
  Realizer <constant_or_variable> [as <name>] [arity <n>] := <term>.
  ```

  Note that translating a term or module may lead to proof obligations (for some
  fixpoints and opaque terms if you did not import `ProofIrrelevence`). You need to
  declare a tactic to solve such proof obligations:
  ```coq
  Parametricity Tactic := <tactic>.
  ```
  (supports global/export/local attributes like Obligation Tactic)
---