-
Notifications
You must be signed in to change notification settings - Fork 4
/
meta.yml
157 lines (126 loc) · 5.63 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
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
---
fullname: Dblib
shortname: dblib
organization: coq-community
community: true
action: true
synopsis: Library for de Bruijn indices in Coq
description: |-
Library with facilities for working with de Bruijn indices in Coq to
reason about capture-avoiding substitution of variables in syntax with binders.
authors:
- name: François Pottier
initial: true
maintainers:
- name: Kevin Orr
nickname: KevOrr
opam-file-maintainer: [email protected]
opam-file-version: dev
license:
fullname: GNU General Public License v3.0
identifier: GPL-3.0-only
supported_coq_versions:
text: 8.7 or later
opam: '{(>= "8.7" & < "8.15~") | (= "dev")}'
tested_coq_nix_versions:
- coq_version: 'master'
tested_coq_opam_versions:
- version: dev
- version: '8.13'
- version: '8.12'
- version: '8.11'
- version: '8.10'
- version: '8.9'
- version: '8.8'
- version: '8.7'
namespace: Dblib
keywords:
- name: abstract syntax
- name: binders
- name: de Bruijn indices
- name: substitution
categories:
- name: Computer Science/Lambda Calculi
documentation: |-
## Documentation
### Workflow
The basic workflow for using the library is as follows:
1. The client manually defines the syntax of terms (or types, or whatever
syntax she is interested in) as usual, as an inductive type.
2. The client manually defines a higher-order `traverse` function, which can
be thought of as a generic, capture-avoiding substitution function. Its
job is (i) to apply a user-supplied function `f` at every variable, and
(ii) to inform `f` about the number of binders that have been entered. By
defining `traverse`, the client effectively defines the binding structure.
3. The client proves that the `traverse` function is well-behaved, i.e., it
satisfies half a dozen reasonable properties. These proofs are usually
trivial, because the library provides tailor-made tactics for this
purpose.
4. The library defines weakening (`lift`) and substitution (`subst`) in
terms of `traverse`, and proves a rather large number of properties of
these functions.
5. The functions `lift` and `subst` are opaque, so an application of these
functions cannot be reduced by Coq's builtin tactic `simpl`. The library
provides `simpl_lift_goal` and `simpl_subst_goal` for this purpose (plus
a few variants of these tactics that perform simplification within a
hypothesis, or within all hypotheses).
6. The library also provides hint databases, to be used with `eauto`, that
can prove many of the typical equalities that arise when proving
weakening or substitution lemmas.
7. The library defines a `closed` term as one that is invariant under
lifting (and substitution), and provides lemmas/tactics for reasoning
about this notion.
Everything is based on type classes: `traverse`, `lift`, `subst`, etc. are
overloaded, so the whole process can be repeated, if desired, for another
inductive type.
The library *does* support multiple *independent* namespaces: for instance, it
is possible to have terms that contain term variables and types that contain
type variables.
The library does *not* support multiple namespaces when there is interaction
between them: for instance, it is *not* possible to have terms that contain
both term variables and type variables, as in a standard presentation of
System F. A possible work-around is to define a single namespace of
"variables" and to use a separate well-kindedness judgement in order to
distinguish between "term" variables and "type" variables. This
approach has been used in a large proof, where it has turned out
to be extremely beneficial.
### Library Files
The library consists of the following files:
- [DblibTactics.v](src/DblibTactics.v)
A small number of hints and tactics that are used in the library.
The end user should not need to worry about them, but can go and
have a look.
- [DeBruijn.v](src/DeBruijn.v)
The core library. The end user is encouraged to read the first
two parts of this file, which present 1- the operations and
properties that the client is expected to provide; and 2- the
operations and properties that the library provides. These two
parts extend up to the first double dashed line, near line 432.
- [Environments.v](src/Environments.v)
This auxiliary library defines a notion of environment, which
is typically useful when defining a typing judgement. The use
of this library is optional.
### Demos
The documentation takes the form of a few demo files:
- [DemoLambda.v](src/DemoLambda.v)
Small-step operational semantics and typing judgement for the
simply-typed lambda-calculus. Proof of type preservation and
of a few other basic lemmas.
- [DemoValueTerm.v](src/DemoValueTerm.v)
Short demo of how to use the library in the case where there
are two distinct syntactic categories of things in which we
substitute (e.g., terms) and things that we substitute (e.g.,
values).
- [DemoExplicitSystemF.v](src/DemoExplicitSystemF.v)
Proof of type preservation for System F, in a version where
the presence of type abstractions and type applications is
explicit in the syntax of terms. (Still, terms do not refer
to types!)
- [DemoImplicitSystemF.v](src/DemoImplicitSystemF.v)
Proof of type preservation for System F, in a version where
type abstraction and type application are implicit, i.e.,
the syntax of terms is untyped. This proof is trickier than
the one above, in that it requires induction over the height
of type derivations. But as far as binding is concerned, no
new problems arise.
---