-
Notifications
You must be signed in to change notification settings - Fork 3
/
Copy pathmeta.yml
132 lines (105 loc) · 3.86 KB
/
meta.yml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
---
fullname: Trocq
shortname: trocq
organization: coq-community
community: true
action: false
coqdoc: false
doi: 10.5281/zenodo.10492403
synopsis: >-
A modular parametricity plugin for proof transfer in Coq
description: |-
Trocq is a modular parametricity plugin for Coq. It can be used to
achieve proof transfer by both translating a user goal into another,
related, variant, and computing a proof that proves the corresponding implication.
The plugin features a hierarchy of structures on relations, whose
instances are computed from registered user-defined proof via
parametricity. This hierarchy ranges from structure-less relations
to an original formulation of type equivalence. The resulting
framework generalizes [raw
parametricity](https://arxiv.org/abs/1209.6336), [univalent
parametricity](https://doi.org/10.1145/3429979) and
[CoqEAL](https://github.com/coq-community/coqeal), and includes them
in a unified framework.
The plugin computes a parametricity translation "à la carte", by
performing a fine-grained analysis of the requires properties for a
given proof of relatedness. In particular, it is able to prove
implications without resorting to full-blown type equivalence,
allowing this way to perform proof transfer without necessarily
pulling in the univalence axiom.
The plugin is implemented in Coq-Elpi and the code of the
parametricity translation is fairly close to a pen-and-paper
sequent-style presentation.
publications:
- pub_url: https://hal.science/hal-04177913/document
pub_title: 'Trocq: Proof Transfer for Free, With or Without Univalence'
authors:
- name: Cyril Cohen
initial: true
- name: Enzo Crance
initial: true
- name: Assia Mahboubi
initial: true
maintainers:
- name: Cyril Cohen
nickname: CohenCyril
- name: Enzo Crance
nickname: ecranceMERCE
- name: Assia Mahboubi
nickname: amahboubi
opam-file-maintainer: Enzo Crance <[email protected]>
opam-file-version: dev
license:
fullname: GNU Lesser General Public License v3.0
identifier: LGPL-3.0-or-later
file: LICENSE
supported_coq_versions:
text: 8.17
opam: '{>= "8.17" & < "8.18"}'
tested_coq_opam_versions:
- version: '8.17'
dependencies:
- opam:
name: coq-elpi
version: '{= "dev"}'
description: |-
[Coq-Elpi custom version](https://github.com/ecranceMERCE/coq-elpi/tree/strat)
- opam:
name: coq-hott
version: '{>= "8.17" & < "8.18~"}'
description: |-
[Coq-HoTT 8.17](https://github.com/HoTT/Coq-HoTT)
namespace: Trocq
keywords:
- name: automation
- name: elpi
- name: proof transfer
- name: isomorphism
- name: univalence
- name: parametricity
categories:
- name: Computer Science/Decision Procedures and Certified Algorithms/Decision procedures
- name: Miscellaneous/Coq Extensions
build: |-
## Building and installation instructions
Trocq is a still a prototype. In particular, it depends on a [custom
version](https://github.com/ecranceMERCE/coq-elpi/tree/strat) of
Coq-Elpi. It is not yet packaged in Opam or Nix.
There are however three ways to experiment with it, all documented
in the [INSTALL.md file](INSTALL.md).
documentation: |-
## Documentation
See the [tutorial](artifact-doc/TUTORIAL.md) for concrete use cases.
In short, the plugin provides a tactic:
- `trocq` (without arguments) which attempts to run a translation on
a given goal, using the information provided by the user with the
commands described below.
And three commands:
- `Trocq Use t` to use a translation `t` during the subsequent calls
to the tactic `trocq`.
- `Trocq Register Univalence u` to declare a univalence axiom `u`.
- `Trocq Register Funext fe` to declare a function extensionality
axiom `fe`.
## ESOP 2024 artifact documentation
The ESOP 2024 artifact documentation files can be found in the `artifact-doc` directory, except for `INSTALL.md` that can be found in the current directory.
---